trace_eq_contract_of_basis' — Mathlib

English

The trace equals the contraction using the basis-induced dual isomorphism.

Русский

След равен контрактору через дуальное изоморфирование, индуцированное базисом.

LaTeX

$$$\\text{trace}_R M = \\mathrm{contractLeft}_R M \\circ (\\text{dualTensorHomEquivOfBasis } b)^{-1}$$$

Lean4

/-- The trace of a linear map corresponds to the contraction pairing under the isomorphism
`End(M) ≃ M* ⊗ M`. -/
theorem trace_eq_contract_of_basis' [Fintype ι] [DecidableEq ι] (b : Basis ι R M) :
    LinearMap.trace R M = contractLeft R M ∘ₗ (dualTensorHomEquivOfBasis b).symm.toLinearMap := by
  simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]

Похожие утверждения