Documentation

Mathlib.Algebra.DirectSum.LinearMap

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 : ι) → Basis (κ₁ i) R (N₁ i)) (b₂ : (i : ι) → Basis (κ₂ i) R (N₂ i)) {f : M₁ →ₗ[R] M₂} (hf : ∀ (i : ι), Set.MapsTo f (N₁ i) (N₂ i)) :
(LinearMap.toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f = Matrix.blockDiagonal' fun (i : ι) => (LinearMap.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 : { x : ι // x s }) => N i) (b : (i : { x : ι // x s }) → Basis (κ i) R (N i)) (σ : ιι) (hσ : ∀ (i : ι), σ i i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N (σ i))) (hN : is, N i = ) :
((LinearMap.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 ι] (h : DirectSum.IsInternal N) [∀ (i : ι), Module.Finite R (N i)] [∀ (i : ι), Module.Free R (N i)] [Fintype ι] {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) :
(LinearMap.trace R M) f = i : ι, (LinearMap.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 ι] (h : DirectSum.IsInternal N) [∀ (i : ι), Module.Finite R (N i)] [∀ (i : ι), Module.Free R (N i)] (hN : {i : ι | N i }.Finite) {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) :
(LinearMap.trace R M) f = ihN.toFinset, (LinearMap.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 ι] (h : DirectSum.IsInternal N) [∀ (i : ι), Module.Finite R (N i)] [∀ (i : ι), Module.Free R (N i)] [IsNoetherian R M] (σ : ιι) (hσ : ∀ (i : ι), σ i i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N (σ i))) :
(LinearMap.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 : Module.End R M} {g : Module.End R M} (h_comm : Commute f g) (hf : ⨆ (μ : R), ⨆ (k : ), (f.genEigenspace μ) k = ) (hg : ∀ (μ : R), (LinearMap.trace R (⨆ (k : ), (f.genEigenspace μ) k)) (LinearMap.restrict g ) = 0) :
(LinearMap.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 {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : ιSubmodule R M} (s : Set ι) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) :
Set.MapsTo f (is, N i) (is, 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 : CompleteLattice.Independent fun (i : { x : ι // x s }) => N i) {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) (p : Submodule R M) (hp : p = is, N i) (hp' : optParam (Set.MapsTo f p p) ) :
(LinearMap.trace R p) (LinearMap.restrict f hp') = is, (LinearMap.trace R (N i)) (LinearMap.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.