The trace of an endomorphism of a tensor square

A tensor square carries a basis indexed by pairs of indices of a basis of the underlying module, and the two tensor squares in the library — the binary M ⊗[R] M and the Fin 2-indexed ⨂[R]^2 M — differ only in how that pair index is spelled. This file isolates the computation they share: an endomorphism of the square whose diagonal entry at the pair (i, j) is aᵢⱼ aⱼᵢ, where a is the matrix of an endomorphism f of the module, has trace tr (f ∘ f), because summing aᵢⱼ aⱼᵢ over all pairs is the trace of a * a.

The endomorphism the two callers feed in is f ⊗ f composed with the flip of the two factors, but nothing here knows that: the input is the diagonal of the matrix, so the statement is about an arbitrary finite basis whose index type is equivalent to a pair type, and the two callers supply their own basis and their own diagonal computation.

Main results

• Module.Basis.trace_eq_trace_comp_self_of_toMatrix_diag: an endomorphism with diagonal entries aᵢⱼ aⱼᵢ in a pair-indexed basis has trace tr (f ∘ f).

theorem Module.Basis.trace_eq_trace_comp_self_of_toMatrix_diag {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Finite ι] (b : Basis ι R M) (B : Basis κ R N) (e : κ ≃ ι × ι) (f : M →ₗ[R] M) (T : N →ₗ[R] N) (hdiag : ∀ (p : κ), B.toMatrix (⇑T ∘ ⇑B) p p = b.toMatrix (⇑f ∘ ⇑b) (e p).1 (e p).2 * b.toMatrix (⇑f ∘ ⇑b) (e p).2 (e p).1) : (LinearMap.trace R N) T = (LinearMap.trace R M) (f ∘ₗ f)

An endomorphism whose diagonal entries are aᵢⱼ aⱼᵢ has trace tr (f ∘ f). Here a is the matrix of f in the basis b, and the diagonal is read in a basis B whose index type is equivalent, through e, to pairs of indices of b; summing aᵢⱼ aⱼᵢ over all pairs is the trace of a * a, which is the trace of f ∘ f. Only the index type of b is assumed finite; the equivalence e ensures that the index type of B is finite too.