Finiteness of the normal-subgroup joint-weight action

In a finite-dimensional representation, the characters of a normal subgroup with nonzero joint weight space form a finite type by MonoidHom.finite_nonzeroJointWeights. The ambient group therefore acts on a finite set of nonzero joint weights, so the kernel of this permutation action has finite index. Each element of that kernel preserves every nonzero joint weight space by map_iInf_eigenspace_unitHom_eq_self_of_mem_ker_nonzeroJointWeightAction.

This is the finite-action bridge in the Lie--Kolchin argument. The remaining connectedness step is to show that the ambient algebraic group acts trivially on this finite set.

Main declarations

• NonzeroJointWeight: the characters whose joint weight space is nonzero.
• finiteIndex_ker_nonzeroJointWeightAction: for a normal subgroup, the kernel of the ambient permutation action on its nonzero joint weights has finite index.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. E. Humphreys, Linear Algebraic Groups, §17.6.

@[reducible, inline]

abbrev TauCeti.NonzeroJointWeight {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [Field K] [AddCommGroup V] [Module K V] (N : Subgroup G) (ρ : G →* Module.End K V) : Type (max 0 u_1 u_2)

The characters of a subgroup whose joint weight space in a representation is nonzero.

Equations

• TauCeti.NonzeroJointWeight N ρ = { χ : ↥N →* Kˣ // ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥ }

instance TauCeti.instFiniteNonzeroJointWeight {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (N : Subgroup G) (ρ : G →* Module.End K V) : Finite (NonzeroJointWeight N ρ)

A finite-dimensional representation has only finitely many nonzero joint weights.

theorem TauCeti.finiteIndex_ker_nonzeroJointWeightAction {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) : (nonzeroJointWeightAction N ρ).ker.FiniteIndex

The kernel of the permutation action on nonzero normal-subgroup weights has finite index in the ambient group.