Documentation

TauCeti.Algebra.AlgebraicGroup.Solvable.Derived.Series

Solvability and termination of the derived series #

For an affine group with schematically dense rational points, the scheme-theoretic and abstract derived series reach the identity at the same index. Thus the scheme-theoretic series terminates exactly when the rational-point group is solvable. This applies in particular to reduced finite-type affine groups over algebraically closed fields.

References #

source
@[simp]
theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_eq_augmentation_iff_of_dense_points {k : Type u_1} [Field k] (H : CommHopfAlgCat k) (h : TauCeti.HopfIdeal.vanishingIdeal ⊤ = ⊥) (n : ℕ) :
H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.augmentation k ↑H ↔ derivedSeries (WithConv (↑H →ₐ[k] k)) n = ⊥

With schematically dense rational points, scheme-theoretic and abstract derived series reach the identity at the same index.

source
theorem CommHopfAlgCat.isSolvable_points_iff_exists_derivedSeriesDefiningIdeal_eq_augmentation_of_dense_points {k : Type u_1} [Field k] (H : CommHopfAlgCat k) (h : TauCeti.HopfIdeal.vanishingIdeal ⊤ = ⊥) :
Group.IsSolvable (WithConv (↑H →ₐ[k] k)) ↔ ∃ (n : ℕ), H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.augmentation k ↑H

With schematically dense rational points, rational-point solvability is equivalent to termination of the scheme-theoretic derived series.

source
theorem CommHopfAlgCat.derivedSeriesDefiningIdeal_eq_augmentation_iff {k : Type u_1} [Field k] (H : CommHopfAlgCat k) [IsAlgClosed k] [Algebra.FiniteType k ↑H] [IsReduced ↑H] (n : ℕ) :
H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.augmentation k ↑H ↔ derivedSeries (WithConv (↑H →ₐ[k] k)) n = ⊥

Scheme-theoretic and abstract derived series reach the identity at the same index.

source
theorem CommHopfAlgCat.isSolvable_points_iff_exists_derivedSeriesDefiningIdeal_eq_augmentation {k : Type u_1} [Field k] (H : CommHopfAlgCat k) [IsAlgClosed k] [Algebra.FiniteType k ↑H] [IsReduced ↑H] :
Group.IsSolvable (WithConv (↑H →ₐ[k] k)) ↔ ∃ (n : ℕ), H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.augmentation k ↑H

A reduced finite-type affine group over an algebraically closed field has solvable rational points exactly when its scheme-theoretic derived series reaches the identity.

source
theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.iff_exists_derivedSeriesDefiningIdeal_eq_augmentation {k : Type u_1} [Field k] (H : CommHopfAlgCat k) [IsAlgClosed k] [Algebra.FiniteType k ↑H] [IsReduced ↑H] :
geometricallySolvablePointsCommHopfAlgProperty k H ↔ ∃ (n : ℕ), H.derivedSeriesDefiningIdeal n = HopfIdeal.augmentation k ↑H

Over an algebraically closed field, the geometric-points solvability property of a reduced finite-type affine group is equivalent to termination of its derived series.