Solvability and the derived closed subgroup

Let H be a commutative Hopf algebra. Its derived closed subgroup has coordinate algebra H / CommHopfAlgCat.derivedDefiningIdeal H. This file proves, over any commutative base and at every commutative value algebra, that the point group of H is solvable exactly when the point group of any closed subgroup containing the derived subgroup is solvable. The derived-subgroup and geometric-points statements are immediate specializations.

One implication is closure of solvability under closed subgroups. Conversely, the derived closed subgroup contains every pointwise commutator, so the corresponding point-group quotient is commutative. Solvability of the derived subgroup and of this commutative quotient then gives solvability of the ambient point group by extension closure. No equality between the abstract pointwise commutator subgroup and the points of the derived group is needed.

Main declarations

• TauCeti.CommHopfAlgCat.isSolvable_points_iff_of_le_derivedDefiningIdeal: over any commutative base and value algebra, the point group is solvable exactly when any closed subgroup containing the derived subgroup has a solvable point group.
• TauCeti.CommHopfAlgCat.isSolvable_points_iff_derived: the derived-subgroup specialization.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_derived: geometric-point solvability is equivalent to geometric-point solvability of the derived closed subgroup.

References

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

This comparison passes solvability between a geometric group and its derived subgroup, and is used when reducing arguments by derived length.

theorem TauCeti.CommHopfAlgCat.isSolvable_points_quotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) : Group.IsSolvable ↑(HopfAlgebra.points A) → Group.IsSolvable ↑(HopfAlgebra.points A)

The point group of a closed subgroup of an affine group is solvable whenever the ambient point group is solvable. This holds over an arbitrary commutative base ring and at every commutative value algebra.

theorem TauCeti.CommHopfAlgCat.isSolvable_points_of_le_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hID : I ≤ derivedDefiningIdeal ↑H) (A : CommAlgCat R) : Group.IsSolvable ↑(HopfAlgebra.points A) → Group.IsSolvable ↑(HopfAlgebra.points A)

If a closed subgroup contains the derived subgroup and its point group is solvable, then the ambient point group is solvable. This holds over an arbitrary commutative base ring and at every commutative value algebra.

theorem TauCeti.CommHopfAlgCat.isSolvable_points_iff_of_le_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hID : I ≤ derivedDefiningIdeal ↑H) (A : CommAlgCat R) : Group.IsSolvable ↑(HopfAlgebra.points A) ↔ Group.IsSolvable ↑(HopfAlgebra.points A)

The point group of an affine group is solvable if and only if the point group of any closed subgroup containing its derived subgroup is solvable. This holds over an arbitrary commutative base ring and at every commutative value algebra.

theorem TauCeti.CommHopfAlgCat.isSolvable_points_iff_derived {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) : Group.IsSolvable ↑(HopfAlgebra.points A) ↔ Group.IsSolvable ↑(HopfAlgebra.points A)

The group of points of an affine group is solvable if and only if the group of points of its derived closed subgroup is solvable, over any commutative base and value algebra.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_of_le_derivedDefiningIdeal (k : Type u) [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) (hID : I ≤ CommHopfAlgCat.derivedDefiningIdeal ↑H) : geometricallySolvablePointsCommHopfAlgProperty k H ↔ geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)

An affine group has solvable geometric points if and only if any closed subgroup containing its derived subgroup does. This is the point-group result specialized to algebraic-closure-valued points.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_derived (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallySolvablePointsCommHopfAlgProperty k H ↔ geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H (CommHopfAlgCat.derivedDefiningIdeal ↑H))

An affine group has solvable geometric points if and only if its derived closed subgroup does. This is CommHopfAlgCat.isSolvable_points_iff_derived specialized to algebraic-closure-valued points.