English
For finite free modules M,N, the trace on End(M×N) applied to the product-map equals the combination of traces on M and N via coprod.
Русский
Для конечном свободных модулей M,N след на End(M×N), применяемый к prodMapLinear, равен сочетанию следов на M и N через coproduct.
LaTeX
$$$ \operatorname{trace}_R(M \times N) \circ \mathrm{prodMapLinear}_R(M,N,M,N,R) = (\mathrm{coprod\;id\;id}) \circ ( (\operatorname{trace}_R M) .prodMap (\operatorname{trace}_R N) ). $$$
Lean4
theorem trace_prodMap :
trace R (M × N) ∘ₗ prodMapLinear R M N M N R = (coprod id id : R × R →ₗ[R] R) ∘ₗ prodMap (trace R M) (trace R N) :=
by
let e := (dualTensorHomEquiv R M M).prodCongr (dualTensorHomEquiv R N N)
have h : Function.Surjective e.toLinearMap := e.surjective
refine (cancel_right h).1 ?_
ext
·
simp only [dualTensorHomEquiv, LinearEquiv.coe_prodCongr, dualTensorHomEquivOfBasis_toLinearMap,
AlgebraTensorModule.curry_apply, restrictScalars_comp, curry_apply, coe_comp, coe_restrictScalars, coe_inl,
Function.comp_apply, prodMap_apply, map_zero, prodMapLinear_apply, dualTensorHom_prodMap_zero,
trace_eq_contract_apply, contractLeft_apply, coe_fst, coprod_apply, id_coe, id_eq, add_zero, e]
·
simp only [dualTensorHomEquiv, LinearEquiv.coe_prodCongr, dualTensorHomEquivOfBasis_toLinearMap,
AlgebraTensorModule.curry_apply, restrictScalars_comp, curry_apply, coe_comp, coe_restrictScalars, coe_inr,
Function.comp_apply, prodMap_apply, map_zero, prodMapLinear_apply, zero_prodMap_dualTensorHom,
trace_eq_contract_apply, contractLeft_apply, coe_snd, coprod_apply, id_coe, id_eq, zero_add, e]
