Documentation

TauCeti.RepresentationTheory.Unipotent.DerivedEigenvector

Eigenvectors modulo a unipotent normal subgroup #

Let N be a normal subgroup containing the commutator subgroup of G, and let G act on a nonzero finite-dimensional vector space over an algebraically closed field. If every element of N acts unipotently, then the representation has a common eigenvector.

Kolchin first supplies a nonzero N-fixed vector. The whole group preserves the space of N-fixed vectors, and its action there factors through the commutative quotient G/N. Commuting operators over an algebraically closed field have a common eigenvector, whose eigenvalues assemble into a unit-valued character of G.

Main declaration #

References #

This supplies the abstract reduction used in Lie--Kolchin arguments.

theorem Representation.exists_unitHom_jointEigenvector_of_commutator_le_of_isUnipotent {K : Type u} {G : Type v} {V : Type w} [Field K] [IsAlgClosed K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (rho : Representation K G V) (N : Subgroup G) (hcomm : commutator G ≤ N) (hunipotent : ∀ (n : ↥N), IsNilpotent (rho ↑n - 1)) :
∃ (χ : G →* Kˣ) (v : V), v ≠ 0 ∧ ∀ (g : G), (rho g) v = ↑(χ g) • v

A representation has a common eigenvector if some subgroup containing the commutator subgroup acts unipotently. Such a subgroup is automatically normal.

Kolchin first produces a nonzero vector fixed by the normal subgroup. Its entire fixed space is stable under the ambient group, and the induced action factors through the commutative quotient.