Linear maps between direct sums

This file contains results about linear maps which respect direct sum decompositions of their domain and codomain.

theorem LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal' {ι : Type u_1} [DecidableEq ι] {R : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {N₁ : ι → Submodule R M₁} (h₁ : DirectSum.IsInternal N₁) [AddCommMonoid M₂] [Module R M₂] {N₂ : ι → Submodule R M₂} (h₂ : DirectSum.IsInternal N₂) {κ₁ : ι → Type u_7} {κ₂ : ι → Type u_8} [(i : ι) → Fintype (κ₁ i)] [∀ (i : ι), Finite (κ₂ i)] [(i : ι) → DecidableEq (κ₁ i)] [Fintype ι] (b₁ : (i : ι) → Module.Basis (κ₁ i) R ↥(N₁ i)) (b₂ : (i : ι) → Module.Basis (κ₂ i) R ↥(N₂ i)) {f : M₁ →ₗ[R] M₂} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)) : (toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f = Matrix.blockDiagonal' fun (i : ι) => (toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)

If a linear map f : M₁ → M₂ respects direct sum decompositions of M₁ and M₂, then it has a block diagonal matrix with respect to bases compatible with the direct sum decompositions.

theorem LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ι → Submodule R M} [DecidableEq ι] {κ : ι → Type u_4} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] {s : Finset ι} (h : DirectSum.IsInternal fun (i : ↥s) => N ↑i) (b : (i : ↥s) → Module.Basis (κ ↑i) R ↥(N ↑i)) (σ : ι → ι) (hσ : ∀ (i : ι), σ i ≠ i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))) (hN : ∀ i ∉ s, N i = ⊥) : ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag = 0

theorem LinearMap.trace_eq_sum_trace_restrict {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ι → Submodule R M} [DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (h : DirectSum.IsInternal N) [Fintype ι] {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) : (trace R M) f = ∑ i : ι, (trace R ↥(N i)) (f.restrict ⋯)

The trace of an endomorphism of a direct sum is the sum of the traces on each component.

See also LinearMap.trace_restrict_eq_sum_trace_restrict.

theorem LinearMap.trace_eq_sum_trace_restrict' {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ι → Submodule R M} [DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (h : DirectSum.IsInternal N) (hN : {i : ι | N i ≠ ⊥}.Finite) {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) : (trace R M) f = ∑ i ∈ hN.toFinset, (trace R ↥(N i)) (f.restrict ⋯)

theorem LinearMap.trace_eq_zero_of_mapsTo_ne {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ι → Submodule R M} [DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (h : DirectSum.IsInternal N) [IsNoetherian R M] (σ : ι → ι) (hσ : ∀ (i : ι), σ i ≠ i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))) : (trace R M) f = 0

theorem LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] {f g : Module.End R M} (h_comm : Commute f g) (hf : ⨆ (μ : R), f.maxGenEigenspace μ = ⊤) (hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0) : (trace R M) (g ∘ₗ f) = 0

If f and g are commuting endomorphisms of a finite, free R-module M, such that f is triangularizable, then to prove that the trace of g ∘ f vanishes, it is sufficient to prove that the trace of g vanishes on each generalized eigenspace of f.

theorem LinearMap.mapsTo_biSup_of_mapsTo {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_4} {N : ι → Submodule R M} (s : Set ι) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) : Set.MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

theorem LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ι → Submodule R M} [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (s : Finset ι) (h : iSupIndep fun (i : ↥s) => N ↑i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i) (hp' : Set.MapsTo ⇑f ↑p ↑p := ⋯) : (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

The trace of an endomorphism of a direct sum is the sum of the traces on each component.

Note that it is important the statement gives the user definitional control over p since the type of the term trace R p (f.restrict hp') depends on p.