Joins of normal unipotent linear groups

Let U and W be subgroups of a group acting on a finite-dimensional vector space, with W normalizing U. If every element of each subgroup acts unipotently, then every element of U ⊔ W acts unipotently. The key point is that the common fixed space of U is invariant under W. Kolchin's common fixed-vector theorem applied to W on that space therefore produces a line fixed by both subgroups. Repeating the argument on the quotient gives a simultaneous upper-unitriangular basis for their join. In particular, the result applies when U is normal in the ambient group.

This is the linear-algebraic core of closure of connected normal unipotent affine subgroups under binary products. The scheme-theoretic argument additionally has to identify the geometric points of the multiplication image with products of points of the two source subgroups.

Main declarations

• Representation.exists_common_fixed_vector_of_le_normalizer_isUnipotent: two subgroups, one normalized by the other, acting unipotently have a common nonzero fixed vector.
• Representation.exists_basis_isUpperUnitriangular_of_le_normalizer_isUnipotent: if they generate the ambient group, it is simultaneously upper unitriangular.
• Representation.isNilpotent_sub_one_of_mem_sup_of_le_normalizer_isUnipotent: the corresponding result for an arbitrary join inside a larger group.

References

• A. Borel, Linear Algebraic Groups, Theorem 4.8 and Proposition 14.4.
• T. A. Springer, Linear Algebraic Groups, Proposition 2.4.12.

This supplies the representation-theoretic product step in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

theorem Representation.exists_common_fixed_vector_of_le_normalizer_isUnipotent {K : Type u} {G : Type w} {V : Type v} [Field K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] (rho : Representation K G V) (U W : Subgroup G) (hWU : W ≤ Subgroup.normalizer ↑U) (hU : ∀ (u : ↥U), IsNilpotent (rho ↑u - 1)) (hW : ∀ (w : ↥W), IsNilpotent (rho ↑w - 1)) : ∃ (x : V), x ≠ 0 ∧ (∀ (u : ↥U), (rho ↑u) x = x) ∧ ∀ (w : ↥W), (rho ↑w) x = x

Common fixed vector for two unipotent subgroups, one normalized by the other. If W normalizes U and both subgroups act unipotently in a nonzero finite-dimensional representation, they fix a common nonzero vector.

theorem Representation.exists_basis_isUpperUnitriangular_of_le_normalizer_isUnipotent {K : Type u} {G : Type w} {V : Type v} [Field K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (rho : Representation K G V) (U W : Subgroup G) (hWU : W ≤ Subgroup.normalizer ↑U) (hUW : U ⊔ W = ⊤) (hU : ∀ (u : ↥U), IsNilpotent (rho ↑u - 1)) (hW : ∀ (w : ↥W), IsNilpotent (rho ↑w - 1)) : ∃ (n : ℕ) (b : Module.Basis (Fin n) K V), ∀ (g : G), ((LinearMap.toMatrixAlgEquiv b) (rho g)).IsUpperUnitriangular

Two unipotent subgroups, one normalized by the other, which generate the ambient group are simultaneously upper unitriangular.

The generation hypothesis is the natural form used for a product subgroup: after restricting an ambient representation to U ⊔ W, the images of U and W generate the whole restricted group.

theorem Representation.isNilpotent_sub_one_of_mem_sup_of_le_normalizer_isUnipotent {K : Type u} {G : Type w} {V : Type v} [Field K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (rho : Representation K G V) (U W : Subgroup G) (hWU : W ≤ Subgroup.normalizer ↑U) (hU : ∀ (u : ↥U), IsNilpotent (rho ↑u - 1)) (hW : ∀ (w : ↥W), IsNilpotent (rho ↑w - 1)) {g : G} (hg : g ∈ U ⊔ W) : IsNilpotent (rho g - 1)

Every element of the join of two unipotent subgroups, one normalized by the other, acts unipotently.

This is the form used for products of subgroup schemes: normalization makes the setwise product a subgroup, and that product is the join.