Documentation

Mathlib.LinearAlgebra.Eigenspace.Pi

Simultaneous eigenvectors and eigenvalues for families of endomorphisms #

In finite dimensions, the theory of simultaneous eigenvalues for a family of linear endomorphisms i ↦ f i enjoys similar properties to that of a single endomorphism, provided the family obeys a compatibility condition. This condition is that the maximum generalised eigenspaces of each endomorphism are invariant under the action of all members of the family. It is trivially satisfied for commuting endomorphisms but there are important more general situations where it also holds (e.g., representations of nilpotent Lie algebras).

Main definitions / results #

theorem Module.End.mem_iInf_maxGenEigenspace_iff {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιEnd R M) (χ : ιR) (m : M) :
m ⨅ (i : ι), (f i).maxGenEigenspace (χ i) ∀ (j : ι), ∃ (k : ), ((f j - χ j 1) ^ k) m = 0
theorem Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιModule.End R M) {μ : ιR} (p : Submodule R M) (hfp : ∀ (i : ι), Set.MapsTo (f i) p p) :
p ⨅ (i : ι), (f i).maxGenEigenspace (μ i) = map p.subtype (⨅ (i : ι), Module.End.maxGenEigenspace (LinearMap.restrict (f i) ) (μ i))

Given a family of endomorphisms i ↦ f i, a family of candidate eigenvalues i ↦ μ i, and a submodule p which is invariant wrt every f i, the intersection of p with the simultaneous maximal generalised eigenspace (taken over all i), is the same as the simultaneous maximal generalised eigenspace of the f i restricted to p.

theorem Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιEnd R M) {μ : ιR} (i : ι) (h : ∀ (j : ι), Set.MapsTo (f j) ((f i).maxGenEigenspace (μ i)) ((f i).maxGenEigenspace (μ i))) :
Submodule.map ((f i).maxGenEigenspace (μ i)).subtype (⨅ (j : ι), (fun (j : ι) => maxGenEigenspace (LinearMap.restrict (f j) ) (μ j)) j) = ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Given a family of endomorphisms i ↦ f i, a family of candidate eigenvalues i ↦ μ i, and a distinguished index i whose maximal generalised μ i-eigenspace is invariant wrt every f j, taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the distinguished generalised μ i-eigenspace.

theorem Module.End.disjoint_iInf_maxGenEigenspace {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιEnd R M) [NoZeroSMulDivisors R M] {χ₁ χ₂ : ιR} (h : χ₁ χ₂) :
Disjoint (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
theorem Module.End.injOn_iInf_maxGenEigenspace {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιEnd R M) [NoZeroSMulDivisors R M] :
Set.InjOn (fun (χ : ιR) => ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) {χ : ιR | ⨅ (i : ι), (f i).maxGenEigenspace (χ i) }
theorem Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo {ι : Type u_1} {R : Type u_2} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (f : ιEnd R M) [NoZeroSMulDivisors R M] (h : ∀ (i j : ι) (φ : R), Set.MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) :
iSupIndep fun (χ : ιR) => ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
theorem Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo {ι : Type u_1} {K : Type u_3} {M : Type u_4} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (f : ιEnd K M) (h : ∀ (i j : ι) (φ : K), Set.MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) (h' : ∀ (i : ι), ⨆ (μ : K), (f i).maxGenEigenspace μ = ) :
⨆ (χ : ιK), ⨅ (i : ι), (f i).maxGenEigenspace (χ i) =

Given a family of endomorphisms i ↦ f i which are compatible in the sense that every maximal generalised eigenspace of f i is invariant wrt f j, if each f i is triangularizable, the family is simultaneously triangularizable.

theorem Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute {ι : Type u_1} {K : Type u_3} {M : Type u_4} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (f : ιEnd K M) (h : Pairwise fun (i j : ι) => Commute (f i) (f j)) (h' : ∀ (i : ι), ⨆ (μ : K), (f i).maxGenEigenspace μ = ) :
⨆ (χ : ιK), ⨅ (i : ι), (f i).maxGenEigenspace (χ i) =

A commuting family of triangularizable endomorphisms is simultaneously triangularizable.