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 compatibilty 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

• Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo: the simultaneous generalised eigenspaces of a compatible family of endomorphisms are independent.
• Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo: in finite dimensions, the simultaneous generalised eigenspaces of a compatible family of endomorphisms span if the same is true of each map individually.

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 : ι → Module.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) = Submodule.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 : ι → Module.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 : ι) => Module.End.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 : ι → Module.End R M) [NoZeroSMulDivisors R M] {χ₁ : ι → R} {χ₂ : ι → 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 : ι → Module.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 : ι → Module.End R M) [NoZeroSMulDivisors R M] (h : ∀ (i j : ι) (φ : R), Set.MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) : CompleteLattice.Independent 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 : ι → Module.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.