The scheme-theoretic derived series

Starting with an affine group, repeatedly take the derived closed subgroup. We keep the defining ideals in the original coordinate algebra, pulling back from each quotient at the successor step. These ideals increase, since the closed subgroups decrease.

The comparison with the abstract derived series of rational points is in TauCeti.Algebra.AlgebraicGroup.Derived.Series.PointClosure. The resulting solvability characterization is in TauCeti.Algebra.AlgebraicGroup.Solvable.Derived.Series.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. S. Milne, Algebraic Groups (2017), §6d.

def CommHopfAlgCat.derivedSeriesDefiningIdeal {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) : ℕ → TauCeti.HopfIdeal R ↑H

The defining ideal of the nth scheme-theoretic derived subgroup, viewed as a closed subgroup of the original affine group.

Equations

• One or more equations did not get rendered due to their size.
• H.derivedSeriesDefiningIdeal 0 = ⊥

@[simp]

theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_zero {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) : H.derivedSeriesDefiningIdeal 0 = ⊥

The series starts at the ambient group itself, whose defining ideal is ⊥.

@[simp]

theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_succ {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) (n : ℕ) : H.derivedSeriesDefiningIdeal (n + 1) = (TauCeti.CommHopfAlgCat.derivedDefiningIdeal ↑(TauCeti.CommHopfAlgCat.quotient H (H.derivedSeriesDefiningIdeal n))).comapOfSurjective (Hom.hom (TauCeti.CommHopfAlgCat.mkQuotient H (H.derivedSeriesDefiningIdeal n))) ⋯

The next term is the derived subgroup of the current closed subgroup, included back into the original group.

@[simp]

theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_one {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) : H.derivedSeriesDefiningIdeal 1 = TauCeti.CommHopfAlgCat.derivedDefiningIdeal ↑H

The first derived-series term is the usual derived closed subgroup.

@[simp]

theorem CommHopfAlgCat.comapOfSurjective_derivedSeriesDefiningIdeal {R : Type u_1} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (n : ℕ) : (K.derivedSeriesDefiningIdeal n).comapOfSurjective (Hom.hom e.hom) ⋯ = H.derivedSeriesDefiningIdeal n

An isomorphism of coordinate Hopf algebras preserves every derived-series term.

theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_monotone {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) : Monotone H.derivedSeriesDefiningIdeal

The defining ideals increase along the derived series.

theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_eq_augmentation_of_le {R : Type u_1} [CommRing R] (H : CommHopfAlgCat R) {m n : ℕ} (hmn : m ≤ n) (hm : H.derivedSeriesDefiningIdeal m = TauCeti.HopfIdeal.augmentation R ↑H) : H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.augmentation R ↑H

Once the derived series reaches the identity, every later term is the identity.