English
Let M be a finite free module over a commutative ring R. Under the natural identification End_R(M) ≅ M^* ⊗_R M, the trace on End_R(M) corresponds to the contraction pairing M^* ⊗_R M → R.
Русский
Пусть M — конечнозаданная свободная модуль над коммутативной кольцевой алгеброй R. Под естественным отображением End_R(M) ≅ M^* ⊗_R M след линейного отображения совпадает с конракцией на M^* ⊗_R M → R.
LaTeX
$$$ \operatorname{trace}_R(M) \circ \mathrm{dualTensorHom}_R(M,M) = \mathrm{contractLeft}_R(M). $$$
Lean4
/-- When `M` is finite free, the trace of a linear map corresponds to the contraction pairing under
the isomorphism `End(M) ≃ M* ⊗ M`. -/
@[simp]
theorem trace_eq_contract : LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M :=
trace_eq_contract_of_basis (Module.Free.chooseBasis R M)
