Existence of joint eigenvectors for commuting endomorphisms

Every commuting family of triangularizable endomorphisms of a nonzero finite-dimensional vector space has a joint eigenvector. The proof is by induction on the dimension: either every endomorphism is scalar, or the eigenspace of a nonscalar member is a nonzero proper subspace preserved by the whole family. Over an algebraically closed field, the triangularizability hypothesis is automatic.

For a group representation with commuting, triangularizable image, such a joint eigenvector exists. The general MonoidHom.unitHomOfJointEigenvector construction from JointEigenvector/Basic.lean packages its eigenvalue function as a unit-valued character. Thus every such representation has a one-dimensional submodule on which the group acts through that character. Over an algebraically closed field, triangularizability is automatic. This is the abelian base step for the fixed-line induction in the Lie--Kolchin theorem.

Main declarations

• TauCeti.exists_jointEigenvector_of_pairwise_commute: a commuting triangularizable family has a joint eigenvector.
• TauCeti.exists_iInf_eigenspace_ne_bot_of_pairwise_commute: the same result in the joint eigenspace API.
• TauCeti.exists_fixed_submodule_finrank_eq_one_of_exists_common_fixed_vector: a common nonzero fixed vector spans a pointwise-fixed line.
• TauCeti.exists_unitHom_jointEigenvector_of_pairwise_commute: a group representation with commuting, triangularizable image has a joint eigenvector whose eigenvalues form a unit-valued character.
• TauCeti.exists_unitHom_submodule_finrank_eq_one_of_pairwise_commute: the resulting one-dimensional submodule, together with the character through which the group acts on it.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Lemma 2.4.2(i): over an algebraically closed field, a set of pairwise commuting matrices is simultaneously conjugate into the upper-triangular matrices, by the induction on an eigenspace of a non-scalar member that is used here. The results below take triangularizability as a hypothesis instead, so that they also apply over a field that is not algebraically closed.

theorem TauCeti.exists_fixed_submodule_finrank_eq_one_of_exists_common_fixed_vector {K : Type u} {V : Type v} {ι : Type w} [DivisionRing K] [AddCommGroup V] [Module K V] (f : ι → Module.End K V) (h : ∃ (v : V), v ≠ 0 ∧ ∀ (i : ι), (f i) v = v) : ∃ (p : Submodule K V), Module.finrank K ↥p = 1 ∧ ∀ (i : ι), ∀ x ∈ p, (f i) x = x

A nonzero vector fixed by a family of endomorphisms spans a one-dimensional submodule fixed pointwise by that family.

theorem TauCeti.exists_jointEigenvector_of_pairwise_commute {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (f : ι → Module.End K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) (htri : ∀ (i : ι), ⨆ (μ : K), (f i).maxGenEigenspace μ = ⊤) : ∃ (χ : ι → K) (v : V), v ≠ 0 ∧ ∀ (i : ι), v ∈ (f i).eigenspace (χ i)

A pairwise-commuting family of triangularizable endomorphisms of a nonzero finite-dimensional vector space has a joint eigenvector.

theorem TauCeti.exists_jointEigenvector_of_pairwise_commute_of_isAlgClosed {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : ι → Module.End K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) : ∃ (χ : ι → K) (v : V), v ≠ 0 ∧ ∀ (i : ι), v ∈ (f i).eigenspace (χ i)

Over an algebraically closed field, every pairwise-commuting family of endomorphisms of a nonzero finite-dimensional vector space has a joint eigenvector.

theorem TauCeti.exists_iInf_eigenspace_ne_bot_of_pairwise_commute {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (f : ι → Module.End K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) (htri : ∀ (i : ι), ⨆ (μ : K), (f i).maxGenEigenspace μ = ⊤) : ∃ (χ : ι → K), ⨅ (i : ι), (f i).eigenspace (χ i) ≠ ⊥

A pairwise-commuting family of triangularizable endomorphisms has a nonzero joint eigenspace.

theorem TauCeti.exists_iInf_eigenspace_ne_bot_of_pairwise_commute_of_isAlgClosed {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : ι → Module.End K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) : ∃ (χ : ι → K), ⨅ (i : ι), (f i).eigenspace (χ i) ≠ ⊥

Over an algebraically closed field, a pairwise-commuting family of endomorphisms has a nonzero joint eigenspace.

theorem TauCeti.exists_unitHom_jointEigenvector_of_pairwise_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) (htri : ∀ (g : G), ⨆ (μ : K), (ρ g).maxGenEigenspace μ = ⊤) : ∃ (χ : G →* Kˣ) (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = ↑(χ g) • v

Every nonzero finite-dimensional representation with pairwise-commuting triangularizable image has a joint eigenvector, and its eigenvalues form a unit-valued character.

theorem TauCeti.exists_unitHom_jointEigenvector_of_pairwise_commute_of_isAlgClosed {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) : ∃ (χ : G →* Kˣ) (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = ↑(χ g) • v

Over an algebraically closed field, every nonzero finite-dimensional representation with pairwise-commuting image has a joint eigenvector whose eigenvalues form a unit-valued character.

theorem TauCeti.exists_unitHom_iInf_eigenspace_ne_bot_of_pairwise_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) (htri : ∀ (g : G), ⨆ (μ : K), (ρ g).maxGenEigenspace μ = ⊤) : ∃ (χ : G →* Kˣ), ⨅ (g : G), (ρ g).eigenspace ↑(χ g) ≠ ⊥

A group representation with pairwise-commuting triangularizable image has a nonzero joint eigenspace indexed by a unit-valued character.

theorem TauCeti.exists_unitHom_iInf_eigenspace_ne_bot_of_pairwise_commute_of_isAlgClosed {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) : ∃ (χ : G →* Kˣ), ⨅ (g : G), (ρ g).eigenspace ↑(χ g) ≠ ⊥

Over an algebraically closed field, a group representation with pairwise-commuting image has a nonzero joint eigenspace indexed by a unit-valued character.

theorem TauCeti.exists_unitHom_submodule_finrank_eq_one_of_pairwise_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) (htri : ∀ (g : G), ⨆ (μ : K), (ρ g).maxGenEigenspace μ = ⊤) : ∃ (χ : G →* Kˣ) (p : Submodule K V), Module.finrank K ↥p = 1 ∧ ∀ (g : G), ∀ x ∈ p, (ρ g) x = ↑(χ g) • x

For a group representation with pairwise-commuting triangularizable image, there is a one-dimensional submodule and a unit-valued character through which the group acts on it.

theorem TauCeti.exists_unitHom_submodule_finrank_eq_one_of_pairwise_commute_of_isAlgClosed {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {G : Type w} [Group G] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (ρ : G →* Module.End K V) (hcomm : Pairwise fun (g h : G) => Commute (ρ g) (ρ h)) : ∃ (χ : G →* Kˣ) (p : Submodule K V), Module.finrank K ↥p = 1 ∧ ∀ (g : G), ∀ x ∈ p, (ρ g) x = ↑(χ g) • x

Over an algebraically closed field, a group representation with pairwise-commuting image has a one-dimensional submodule and a unit-valued character through which the group acts on it.