English
For linear maps f: M→N, g: N→P, h: P→M, the trace is cyclic along the cycle g∘f∘h, i.e., tr_P(g f h) = tr_N(f h g).
Русский
След по замыканию вдоль цикла f,g,h равен циклическому обходу: tr_P(g f h) = tr_N(f h g).
LaTeX
$$$ \operatorname{trace}_R P (g \circ f \circ h) = \operatorname{trace}_R N (f \circ h \circ g). $$$
Lean4
theorem trace_comp_comm : compr₂ (llcomp R M N M) (trace R M) = compr₂ (llcomp R N M N).flip (trace R N) :=
by
apply
(compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
(show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1
ext g m f n
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply,
compr₂_apply, flip_apply, llcomp_apply', comp_dualTensorHom, LinearMapClass.map_smul, trace_eq_contract_apply,
contractLeft_apply, smul_eq_mul, mul_comm]
