The trace of an endomorphism of a short exact sequence

An endomorphism of a short exact sequence 0 → N → M → Q → 0 over a commutative ring, with M finite and N, Q free, has trace f = trace fN + trace fQ. The freeness of Q splits the sequence; the splitting makes M free and the two outer modules finite. In particular this applies to every short exact sequence of finite-dimensional vector spaces.

The typical use is a filtration whose graded pieces are known: iterating the identity along M ⊇ M₁ ⊇ ⋯ expresses trace f as the sum of the traces on the successive quotients. That is how Algebra.trace_quotient_pow_mk computes the trace of B ⧸ P ^ n from the trace of B ⧸ P.

Main results

• LinearMap.trace_eq_add_of_exact: the trace of the middle endomorphism of a short exact sequence is the sum of the traces of the outer ones.

theorem LinearMap.trace_eq_add_of_exact {R : Type u_1} {M : Type u_2} {N : Type u_3} {Q : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup Q] [Module R Q] [Module.Finite R M] [Module.Free R N] [Module.Free R Q] {i : N →ₗ[R] M} {π : M →ₗ[R] Q} (hi : Function.Injective ⇑i) (hπ : Function.Surjective ⇑π) (hex : Function.Exact ⇑i ⇑π) {f : M →ₗ[R] M} {fN : N →ₗ[R] N} {fQ : Q →ₗ[R] Q} (hN : f ∘ₗ i = i ∘ₗ fN) (hQ : π ∘ₗ f = fQ ∘ₗ π) : (trace R M) f = (trace R N) fN + (trace R Q) fQ

The trace is additive along a short exact sequence. If 0 → N --i--> M --π--> Q → 0 is exact and the endomorphisms fN, f, fQ commute with i and π, then trace f = trace fN + trace fQ. The middle module is finite and the outer modules are free; the quotient's projectivity supplies a section.