Geometric solvability of affine groups

For a commutative Hopf algebra H over a field k, this file records the geometric-points solvability condition: the convolution group of AlgebraicClosure k-valued points of H is a solvable abstract group. Smoothness and finite type are deliberately not built into this property; consumers must state them separately when interpreting it as the classical notion of a solvable algebraic group.

The property is invariant under coordinate-Hopf-algebra isomorphisms. It is preserved by closed subgroups, represented contravariantly by surjective coordinate morphisms, and a product has the property exactly when both factors do. These are the first subgroup-calculus operations needed for Lie--Kolchin theory and the construction of the solvable radical.

Main declarations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty: solvability of the geometric point group.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_isCocomm: commutative affine groups have solvable geometric points.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_surjective: closure under closed subgroups.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_tensorProduct_iff: solvability of a product is equivalent to solvability of both factors.

References

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

This begins the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap. The scheme-theoretic derived subgroup and its comparison with this geometric-points criterion remain to be constructed.

def TauCeti.geometricallySolvablePointsCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (CommHopfAlgCat k)

The object property asserting that the group of algebraic-closure-valued points of a commutative Hopf algebra is solvable.

This property packages only the geometric-points condition. In applications to classical algebraic groups, finite type and smoothness are separate hypotheses.

Equations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty k H = Group.IsSolvable (WithConv (↑H →ₐ[k] AlgebraicClosure k))

@[simp]

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallySolvablePointsCommHopfAlgProperty k H ↔ Group.IsSolvable (WithConv (↑H →ₐ[k] AlgebraicClosure k))

Membership in the geometric-points solvability property means that the convolution group of points over an algebraic closure is solvable.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_isCocomm (k : Type u) [Field k] (H : CommHopfAlgCat k) [Coalgebra.IsCocomm k ↑H] : geometricallySolvablePointsCommHopfAlgProperty k H

A cocommutative coordinate Hopf algebra has solvable geometric points.

Cocommutativity makes the convolution group of points commutative over every commutative value algebra, so in particular its algebraic-closure-valued point group is solvable.

instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatGeometricallySolvablePointsCommHopfAlgProperty (k : Type u) [Field k] : (geometricallySolvablePointsCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Geometric-points solvability is invariant under isomorphisms of commutative Hopf algebras.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_surjective (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (hH : geometricallySolvablePointsCommHopfAlgProperty k H) : geometricallySolvablePointsCommHopfAlgProperty k K

Geometric-points solvability descends along a surjective coordinate Hopf-algebra morphism.

Contravariantly, the target coordinate algebra represents a closed subgroup of the source affine group. Its geometric point group embeds into the solvable point group of the ambient object.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_quotient (k : Type u) [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) (hH : geometricallySolvablePointsCommHopfAlgProperty k H) : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)

The closed subgroup cut out by a Hopf ideal has solvable geometric points whenever the ambient affine group does.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_tensorProduct_iff (k : Type u) [Field k] (H K : CommHopfAlgCat k) : geometricallySolvablePointsCommHopfAlgProperty k ↧(TensorProduct k ↑H ↑K) ↔ geometricallySolvablePointsCommHopfAlgProperty k H ∧ geometricallySolvablePointsCommHopfAlgProperty k K

The tensor-product coordinate algebra has solvable geometric points exactly when both factors do. Contravariantly, this is closure and reflection of solvability by direct products of affine groups.