Reductive affine groups

A finite-type affine group over a field is reductive when it is smooth and geometrically connected and, after extension to an algebraic closure, it has no nontrivial connected normal smooth unipotent closed subgroup. In coordinate-Hopf-algebra terms, a closed subgroup of the geometric fibre is 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 unipotent radical once that radical has been constructed, but it does not make the definition wait for that construction. It also avoids asserting descent of the geometric unipotent radical over an imperfect field.

Instantiating the definition at the zero Hopf ideal—the whole geometric fibre as a subgroup of itself—shows that if the geometric fibre of a reductive group is itself unipotent, its coordinate Hopf algebra is the algebraic closure of the ground field. The resulting bialgebra equivalence is the precise affine-group statement that the geometric fibre is the trivial group.

Main declarations

• TauCeti.reductiveCommHopfAlgProperty: reductivity for finite-type commutative Hopf algebras over a field.
• TauCeti.ReductiveCommHopfAlgCat: the corresponding full subcategory.
• TauCeti.reductiveCommHopfAlgProperty_of_geometricFiber_iso: establish reductivity using an isomorphic direct model of the geometric fibre.
• TauCeti.reductiveCommHopfAlgProperty.eq_augmentation: every connected normal smooth unipotent closed subgroup of a reductive group's geometric fibre is trivial.
• TauCeti.reductiveCommHopfAlgProperty.bot_eq_augmentation: the zero Hopf ideal of a reductive group with unipotent geometric fibre is its augmentation ideal.
• TauCeti.reductiveCommHopfAlgProperty.geometricFiberCounitBialgEquiv: a reductive group with geometrically unipotent geometric fibre has trivial geometric fibre.

References

• J. S. Milne, Algebraic Groups (2017), §6.46 and §19.b.
• T. A. Springer, Linear Algebraic Groups, Chapter 8.
• B. Conrad, Reductive Group Schemes, Section 3.

This is the definition target in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. The geometric formulation is the roadmap's prescribed alternative while the descended unipotent radical is unavailable.

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

The object property selecting reductive 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 unipotent closed subgroup of the geometric fibre 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

• TauCeti.reductiveCommHopfAlgProperty k = TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty k (TauCeti.smoothUnipotentCommHopfAlgProperty (AlgebraicClosure k))

@[simp]

theorem TauCeti.reductiveCommHopfAlgProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : reductiveCommHopfAlgProperty 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 → smoothUnipotentCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I) → I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

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

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatReductiveCommHopfAlgProperty (k : Type u) [Field k] : (reductiveCommHopfAlgProperty k).IsClosedUnderIsomorphisms

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

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

Establish reductivity by identifying the geometric fibre with a direct model on which normal smooth unipotent closed subgroups can be eliminated. This packages the transport of Hopf ideals, normality, the quotient property, and the augmentation ideal across the identification.

@[reducible, inline]

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

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

Equations

• TauCeti.ReductiveCommHopfAlgCat k = (TauCeti.reductiveCommHopfAlgProperty k).FullSubcategory

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

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

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

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

theorem TauCeti.reductiveCommHopfAlgProperty.eq_augmentation {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj) (hI : I.IsNormal) (hconnected : geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj) (hunipotent : smoothUnipotentCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I)) : I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

Every connected normal smooth unipotent closed subgroup of the geometric fibre of a reductive group is the identity subgroup.

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

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

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

A reductive group whose geometric fibre has only unipotent geometric points 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 hunipotent = TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot ⋯

@[simp]

theorem TauCeti.reductiveCommHopfAlgProperty.geometricFiberCounitBialgEquiv_apply {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) (x : ↑H.baseChange.obj) : (hH.geometricFiberCounitBialgEquiv hunipotent) 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.reductiveCommHopfAlgProperty.geometricFiberCounitBialgEquiv_symm_apply {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj) (r : AlgebraicClosure k) : (hH.geometricFiberCounitBialgEquiv hunipotent).symm r = (algebraMap (AlgebraicClosure k) ↑H.baseChange.obj) r

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