Kolchin's common fixed vector theorem

This file proves the linear-algebraic core of Kolchin's theorem: a monoid acting by unipotent automorphisms on a nonzero finite-dimensional vector space over a field has a common nonzero fixed vector. No commutativity or finiteness assumption is made on the monoid.

Over an algebraically closed field, the proof chooses a minimal nonzero invariant subspace and uses Burnside density together with the nondegenerate trace pairing to show that every monoid element is the identity there. Over an arbitrary field, extend scalars to an algebraic closure and descend a fixed tensor by applying a base-field linear functional to its scalar coefficients.

Main results

• Representation.exists_common_fixed_vector_of_isUnipotent: Kolchin's common fixed vector theorem.
• Representation.exists_fixed_submodule_finrank_eq_one_of_isUnipotent: the equivalent fixed-line form.

References

• A. Borel, Linear Algebraic Groups, §4.8, Theorem. Its proof is the one used here: pass to an irreducible submodule, span End V by Burnside, and kill g - 1 with the trace pairing.
• T. A. Springer, Linear Algebraic Groups, Proposition 2.4.12, the same statement in the conjugate-into-Uₙ form, by the same argument.

theorem Representation.exists_common_fixed_vector_of_isUnipotent {K : Type u} {G : Type w} {V : Type v} [Field K] [Monoid G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (ρ : Representation K G V) (hunipotent : ∀ (g : G), IsNilpotent (ρ g - 1)) : ∃ (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = v

Kolchin's common fixed vector theorem. If every element of a monoid acts unipotently on a nonzero finite-dimensional vector space over a field, then the monoid fixes a nonzero vector.

theorem Representation.exists_fixed_submodule_finrank_eq_one_of_isUnipotent {K : Type u} {G : Type w} {V : Type v} [Field K] [Monoid G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (ρ : Representation K G V) (hunipotent : ∀ (g : G), IsNilpotent (ρ g - 1)) : ∃ (p : Submodule K V), Module.finrank K ↥p = 1 ∧ ∀ (g : G), ∀ x ∈ p, (ρ g) x = x

Under Kolchin's hypotheses, the common fixed vectors contain a one-dimensional subspace.