English
Let f ∈ End_R(M) and g ∈ End_R(N). Then the trace on End_R(M⊗_R N) of map f ⊗ g equals the product of traces: tr_{M⊗N}(TensorProduct.map f g) = tr_M(f) · tr_N(g).
Русский
Пусть f, g — концевые отображения на M и N. Тогда след на End(M⊗N) от отображения f ⊗ g равен произведению следов: tr(f)·tr(g).
LaTeX
$$$ \operatorname{trace}_R(M \otimes N) ( \mathrm{TensorProduct.map} f g ) = \operatorname{trace}_R M f \cdot \operatorname{trace}_R N g. $$$
Lean4
theorem trace_tensorProduct :
compr₂ (mapBilinear R M N M N) (trace R (M ⊗ N)) =
compl₁₂ (lsmul R R : R →ₗ[R] R →ₗ[R] R) (trace R M) (trace R N) :=
by
apply
(compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
(show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1
ext f m g n
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply,
compr₂_apply, mapBilinear_apply, trace_eq_contract_apply, contractLeft_apply, lsmul_apply, Algebra.id.smul_eq_mul,
map_dualTensorHom, dualDistrib_apply]
