English
Trace equals the contraction under the dual-tensor isomorphism with basis b.
Русский
След равен контрактору под дуал-множество изоморфизма с базисом b.
LaTeX
$$$\\text{trace}_R M = \\mathrm{contractLeft}_R M \\circ (\\text{dualTensorHomEquivOfBasis } b)^{-1}$$$
Lean4
/-- The trace of a linear map correspond to the contraction pairing under the isomorphism
`End(M) ≃ M* ⊗ M` -/
theorem trace_eq_contract_of_basis [Finite ι] (b : Basis ι R M) :
LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M := by
classical
cases nonempty_fintype ι
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
rintro ⟨i, j⟩
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
obtain rfl | hij := eq_or_ne i j
· simp
rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
simp [hij]
