Block upper triangular endomorphisms of a product

An endomorphism F of A × C that preserves the first summand, acting there as fA, and covers fC on the second is block upper triangular: its only off-diagonal block is the C → A map fst ∘ F ∘ inr. This file records that normal form and the resulting trace identity.

Main results

• LinearMap.eq_prodMap_add_inl_comp_snd — the normal form, over an arbitrary semiring.
• LinearMap.trace_prodMap_add_inl_comp_snd — the trace of a block upper triangular endomorphism is the sum of the traces of its diagonal blocks.

The trace identity needs free finite modules over a commutative ring, since that is what Mathlib's LinearMap.trace_prodMap' and LinearMap.trace_comp_comm' require; the normal form itself needs neither commutativity, finiteness, nor additive inverses.

theorem LinearMap.eq_prodMap_add_inl_comp_snd {R : Type u_1} {A : Type u_2} {C : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid C] [Module R C] {fA : A →ₗ[R] A} {fC : C →ₗ[R] C} (F : A × C →ₗ[R] A × C) (hinl : F ∘ₗ inl R A C = inl R A C ∘ₗ fA) (hsnd : snd R A C ∘ₗ F = fC ∘ₗ snd R A C) : F = fA.prodMap fC + inl R A C ∘ₗ (fst R A C ∘ₗ F ∘ₗ inr R A C) ∘ₗ snd R A C

An endomorphism of A × C that preserves the first summand, acting there as fA, and covers fC on the second, is block upper triangular: its only off-diagonal block is C → A.

theorem LinearMap.trace_prodMap_add_inl_comp_snd {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommRing R] [AddCommGroup A] [Module R A] [Module.Free R A] [Module.Finite R A] [AddCommGroup C] [Module R C] [Module.Free R C] [Module.Finite R C] (fA : A →ₗ[R] A) (fC : C →ₗ[R] C) (u : C →ₗ[R] A) : (trace R (A × C)) (fA.prodMap fC + inl R A C ∘ₗ u ∘ₗ snd R A C) = (trace R A) fA + (trace R C) fC

The trace of a block upper triangular endomorphism of A × C is the sum of the traces of its diagonal blocks: the off-diagonal C → A block composes to zero the other way round, so LinearMap.trace_comp_comm' makes its contribution vanish.