The trace of an endomorphism of a short exact sequence #
An endomorphism of a short exact sequence 0 → N → M → Q → 0 of vector spaces, M
finite-dimensional, has trace f = trace fN + trace fQ.
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
{K : Type u_1}
{M : Type u_2}
{N : Type u_3}
{Q : Type u_4}
[Field K]
[AddCommGroup M]
[Module K M]
[AddCommGroup N]
[Module K N]
[AddCommGroup Q]
[Module K Q]
[FiniteDimensional K M]
{i : N →ₗ[K] M}
{π : M →ₗ[K] Q}
(hi : Function.Injective ⇑i)
(hπ : Function.Surjective ⇑π)
(hex : Function.Exact ⇑i ⇑π)
{f : M →ₗ[K] M}
{fN : N →ₗ[K] N}
{fQ : Q →ₗ[K] Q}
(hN : f ∘ₗ i = i ∘ₗ fN)
(hQ : π ∘ₗ f = 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.