Traces on spanning and complementary invariant submodules

When two invariant subspaces span a finite-dimensional vector space, the sum of the traces on them is the ambient trace plus the trace on their intersection. Over any commutative ring R, when two finite free invariant submodules are complementary, the ambient trace is the sum of the traces on the two summands; over an integral domain R, on a rank-one invariant line R ∙ v (v ≠ 0) in a torsion-free module, the trace is the eigenvalue on v.

theorem LinearMap.trace_restrict_add_trace_restrict_eq_trace_add_trace_restrict_inf {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {A B : Submodule K V} (hAB : Codisjoint A B) (f : V →ₗ[K] V) (hA : ∀ x ∈ A, f x ∈ A) (hB : ∀ x ∈ B, f x ∈ B) : (trace K ↥A) (f.restrict hA) + (trace K ↥B) (f.restrict hB) = (trace K V) f + (trace K ↥(A ⊓ B)) (f.restrict ⋯)

Inclusion-exclusion for traces. If two invariant subspaces span the whole space, the sum of their traces equals the ambient trace plus the trace on their intersection.

theorem LinearMap.trace_eq_trace_restrict_add_trace_restrict {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {A B : Submodule R M} [Module.Free R ↥A] [Module.Finite R ↥A] [Module.Free R ↥B] [Module.Finite R ↥B] (hAB : IsCompl A B) (f : M →ₗ[R] M) (hA : ∀ x ∈ A, f x ∈ A) (hB : ∀ x ∈ B, f x ∈ B) : (trace R M) f = (trace R ↥A) (f.restrict hA) + (trace R ↥B) (f.restrict hB)

Trace on complementary invariant submodules. If A and B are complementary finite free submodules preserved by f, then the trace of f is the sum of the traces of its restrictions to A and B.

theorem LinearMap.trace_restrict_span_singleton {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {v : M} (hv : v ≠ 0) {f : M →ₗ[R] M} {c : R} (hf : f v = c • v) (hspan : ∀ x ∈ R ∙ v, f x ∈ R ∙ v := by intro x hx obtain ⟨a, rfl⟩ := Submodule.mem_span_singleton.mp hx rw [map_smul, hf] exact (Submodule.span R { v }).smul_mem a ((Submodule.span R { v }).smul_mem c (Submodule.mem_span_singleton_self v))) : (trace R ↥(R ∙ v)) (f.restrict hspan) = c

Trace on a spanned invariant line. Over an integral domain R, if v ≠ 0 in a torsion-free R-module M is an eigenvector of f with eigenvalue c, then the restriction of f to R ∙ v has trace c.