trace_eq_contract' — Mathlib

English

The trace on End_R(M) equals the contraction composed with the inverse of the standard End_R(M) ≅ M^* ⊗ M isomorphism.

Русский

След на End_R(M) равен конракции, композиции с обратным отображением изо End_R(M) ≅ M^* ⊗ M.

LaTeX

$$$ \operatorname{trace}_R(M) = \mathrm{contractLeft}_R(M) \circ (\mathrm{dualTensorHomEquiv}_R(M,M))^{-1} . $$$

Lean4

/-- When `M` is finite free, the trace of a linear map corresponds to the contraction pairing under
the isomorphism `End(M) ≃ M* ⊗ M`. -/
theorem trace_eq_contract' : LinearMap.trace R M = contractLeft R M ∘ₗ (dualTensorHomEquiv R M M).symm.toLinearMap :=
  trace_eq_contract_of_basis' (Module.Free.chooseBasis R M)

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