Semisimple affine groups

A finite-type affine group over a field is semisimple when it is smooth and geometrically connected and, after extension to an algebraic closure, it has no nontrivial connected normal smooth solvable closed subgroup. In coordinate-Hopf-algebra terms, a closed subgroup of the geometric fibre is represented contravariantly by a Hopf-ideal quotient. The subgroup is trivial exactly when its defining Hopf ideal is the augmentation ideal.

This formulation is equivalent to triviality of the geometric radical once that radical has been constructed, but makes the semisimple predicate available without choosing a maximal subgroup. Smoothness of the candidate subgroup is essential: in positive characteristic a semisimple group can have non-smooth connected central subgroup schemes.

As a basic consequence, if the geometric fibre of a semisimple group is itself solvable, then it is trivial. The resulting bialgebra equivalence identifies its coordinate algebra with the algebraic closure of the ground field via the counit.

Main declarations

• TauCeti.semisimpleCommHopfAlgProperty: semisimplicity for finite-type commutative Hopf algebras over a field.
• TauCeti.SemisimpleCommHopfAlgCat: the full subcategory of semisimple coordinate Hopf algebras.
• TauCeti.semisimpleCommHopfAlgProperty_of_geometricFiber_iso: establish semisimplicity using an isomorphic coordinate model of the geometric fibre.
• TauCeti.semisimpleCommHopfAlgProperty.eq_augmentation: every connected normal smooth solvable closed subgroup of a semisimple group's geometric fibre is trivial.
• TauCeti.semisimpleCommHopfAlgProperty.geometricFiberCounitBialgEquiv: a semisimple group with solvable geometric fibre has trivial geometric fibre.

References

• J. S. Milne, Algebraic Groups (2017), §§6.46 and 21.10.
• T. A. Springer, Linear Algebraic Groups, Chapter 8.

The formal construction and proof structure were adapted from TauCeti.Algebra.AlgebraicGroup.Reductive.Basic; their common normal-subgroup-freeness infrastructure is factored through TauCeti.Algebra.AlgebraicGroup.Radical.Basic.

This is the semisimple-group definition target in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. It states triviality of the geometric radical through its defining universal property while the radical construction is still being developed.

def TauCeti.semisimpleCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting semisimple finite-type commutative Hopf algebras over a field.

The first two conjuncts express smoothness and geometric connectedness of the ambient group. The last says that every connected normal smooth closed subgroup with solvable geometric points is the identity subgroup. A Hopf ideal I cuts out that subgroup contravariantly, so identity means I is the augmentation ideal, not the zero ideal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.semisimpleCommHopfAlgProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : semisimpleCommHopfAlgProperty k H ↔ Algebra.Smooth k ↑H.obj ∧ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ ∀ (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj), I.IsNormal → geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj → Algebra.Smooth (AlgebraicClosure k) ↑(H.baseChange.quotient I).obj → geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj → I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

Semisimplicity means smoothness, geometric connectedness, and absence of nontrivial connected normal smooth solvable closed subgroups after extension to an algebraic closure.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatSemisimpleCommHopfAlgProperty (k : Type u) [Field k] : (semisimpleCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Semisimplicity is invariant under isomorphisms of finite-type commutative Hopf algebras.

theorem TauCeti.semisimpleCommHopfAlgProperty_of_geometricFiber_iso (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (G : CommHopfAlgCat (AlgebraicClosure k)) (hsmooth : Algebra.Smooth k ↑H.obj) (hconnected : geometricallyConnectedCommHopfAlgProperty k H.obj) (e : H.baseChange.obj ≅ G) (htrivial : ∀ (I : HopfIdeal (AlgebraicClosure k) ↑G), I.IsNormal → geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (CommHopfAlgCat.quotient G I) → Algebra.Smooth (AlgebraicClosure k) ↑(CommHopfAlgCat.quotient G I) → geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) (CommHopfAlgCat.quotient G I) → I = HopfIdeal.augmentation (AlgebraicClosure k) ↑G) : semisimpleCommHopfAlgProperty k H

Establish semisimplicity by identifying the geometric fibre with a coordinate model on which connected smooth normal solvable closed subgroups can be eliminated.

@[reducible, inline]

abbrev TauCeti.SemisimpleCommHopfAlgCat (k : Type u) [Field k] : Type (u + 1)

The category of semisimple finite-type commutative Hopf algebras over a field.

Equations

• TauCeti.SemisimpleCommHopfAlgCat k = (TauCeti.semisimpleCommHopfAlgProperty k).FullSubcategory

theorem TauCeti.semisimpleCommHopfAlgProperty.smooth {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : Algebra.Smooth k ↑H.obj

A semisimple finite-type commutative Hopf algebra is smooth over its ground field.

theorem TauCeti.semisimpleCommHopfAlgProperty.geometricallyConnected {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : geometricallyConnectedCommHopfAlgProperty k H.obj

A semisimple finite-type commutative Hopf algebra is geometrically connected.

theorem TauCeti.semisimpleCommHopfAlgProperty.eq_augmentation {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj) (hI : I.IsNormal) (hconnected : geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj) (hsmooth : Algebra.Smooth (AlgebraicClosure k) ↑(H.baseChange.quotient I).obj) (hsolvable : geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj) : I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

Every connected normal smooth solvable closed subgroup of the geometric fibre of a semisimple group is the identity subgroup.

theorem TauCeti.semisimpleCommHopfAlgProperty.bot_eq_augmentation {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) (hsolvable : geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) : ⊥ = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

If the geometric fibre of a semisimple group has solvable geometric points, its zero Hopf ideal is the augmentation ideal. Equivalently, the whole geometric fibre is the identity subgroup.

noncomputable def TauCeti.semisimpleCommHopfAlgProperty.geometricFiberCounitBialgEquiv {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) (hsolvable : geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) : ↑H.baseChange.obj ≃ₐc[AlgebraicClosure k] AlgebraicClosure k

A semisimple group with solvable geometric fibre has trivial geometric fibre: its coordinate Hopf algebra is bialgebra-equivalent to the algebraic closure of the ground field via the counit.

Equations

• hH.geometricFiberCounitBialgEquiv hsolvable = TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot ⋯

@[simp]

theorem TauCeti.semisimpleCommHopfAlgProperty.geometricFiberCounitBialgEquiv_apply {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) (hsolvable : geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) (x : ↑H.baseChange.obj) : (hH.geometricFiberCounitBialgEquiv hsolvable) x = (Bialgebra.counitBialgHom (AlgebraicClosure k) ↑H.baseChange.obj) x

The equivalence from the geometric fibre to the algebraic closure is its counit.

@[simp]

theorem TauCeti.semisimpleCommHopfAlgProperty.geometricFiberCounitBialgEquiv_symm_apply {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) (hsolvable : geometricallySolvablePointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) (r : AlgebraicClosure k) : (hH.geometricFiberCounitBialgEquiv hsolvable).symm r = (algebraMap (AlgebraicClosure k) ↑H.baseChange.obj) r

The inverse equivalence from the algebraic closure is the geometric fibre's structure map.