Common fixed vectors for commuting unipotent automorphisms

A unipotent automorphism has only the eigenvalue one. Consequently, the joint eigenvector of a commuting family of unipotent automorphisms is fixed by every member of the family. We record both the resulting common fixed vector and the one-dimensional fixed submodule that it spans.

Main declarations

• TauCeti.exists_common_fixed_vector_of_pairwise_commute_of_isUnipotent: a commuting family of unipotent automorphisms of a nonzero finite-dimensional space has a common nonzero fixed vector.
• TauCeti.exists_fixed_submodule_finrank_eq_one_of_pairwise_commute_of_isUnipotent: such a family fixes a one-dimensional submodule pointwise.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Section 2.4.

theorem TauCeti.exists_common_fixed_vector_of_pairwise_commute_of_isUnipotent {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (f : ι → LinearMap.GeneralLinearGroup K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) (hunipotent : ∀ (i : ι), (f i).IsUnipotent) : ∃ (v : V), v ≠ 0 ∧ ∀ (i : ι), ↑(f i) v = v

A pairwise-commuting family of unipotent automorphisms of a nonzero finite-dimensional vector space has a common nonzero fixed vector.

theorem TauCeti.exists_fixed_submodule_finrank_eq_one_of_pairwise_commute_of_isUnipotent {K : Type u} {V : Type v} {ι : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (f : ι → LinearMap.GeneralLinearGroup K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) (hunipotent : ∀ (i : ι), (f i).IsUnipotent) : ∃ (p : Submodule K V), Module.finrank K ↥p = 1 ∧ ∀ (i : ι), ∀ x ∈ p, ↑(f i) x = x

A pairwise-commuting family of unipotent automorphisms of a nonzero finite-dimensional vector space fixes a one-dimensional submodule pointwise.