Smooth unipotent affine group schemes

This file transports smooth unipotence from finite-type commutative Hopf algebras to affine group schemes of finite type over a field. The coordinate-ring predicate says that the algebra is smooth and that every point over an algebraic closure acts unipotently in every finite-dimensional comodule. Smoothness is explicit: geometric points alone do not detect the infinitesimal structure of a nonreduced group scheme.

The resulting full subcategory is anti-equivalent to smooth unipotent commutative Hopf algebras. This synchronizes the coordinate-ring and scheme models of unipotent groups and supplies the scheme-side predicate needed to formulate reductivity using normal closed subgroup schemes.

Main declarations

• TauCeti.smoothUnipotentAffineGroupSchemeProperty: smooth unipotence for finite-type affine group schemes over a field.
• TauCeti.smoothUnipotentAffineGroupSchemeProperty_iff: its coordinate-ring characterization.
• TauCeti.SmoothUnipotentAffineGroupSchemeCat: the corresponding full subcategory.
• TauCeti.smoothUnipotentCommHopfAlgCatOpEquivSmoothUnipotentAffineGroupSchemeCat: the restricted affine Hopf/group-scheme anti-equivalence.

References

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

This advances Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. It is the scheme-side form of the smooth geometric definition and a direct prerequisite for Layer 6, where reductivity is defined by excluding nontrivial connected normal unipotent closed subgroup schemes after geometric base change.

def TauCeti.smoothUnipotentAffineGroupSchemeProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (FiniteTypeAffineGroupSchemeCat ↧k)

The object property selecting smooth unipotent affine group schemes of finite type over a field.

The property is transported through the finite-type affine Hopf/group-scheme anti-equivalence. Thus it retains the representation-theoretic coordinate-ring criterion while presenting it on the scheme side, without making smoothness implicit in the ambient category.

Equations

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

@[simp]

theorem TauCeti.smoothUnipotentAffineGroupSchemeProperty_iff (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) : smoothUnipotentAffineGroupSchemeProperty k G ↔ Algebra.Smooth k ↑(Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G)).obj ∧ ∀ (g : WithConv (↑(Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G)).obj →ₐ[k] AlgebraicClosure k)), HopfAlgebra.IsUnipotentPoint g

A finite-type affine group scheme is smooth unipotent exactly when the coordinate Hopf algebra supplied by the affine anti-equivalence is smooth and every geometric point acts unipotently in every finite-dimensional comodule.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeAffineGroupSchemeCatOfSmoothUnipotentAffineGroupSchemeProperty (k : Type u) [Field k] : (smoothUnipotentAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

Smooth unipotence of finite-type affine group schemes is invariant under isomorphism.

@[reducible, inline]

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

The category of smooth unipotent affine group schemes of finite type over a field.

Equations

• TauCeti.SmoothUnipotentAffineGroupSchemeCat k = (TauCeti.smoothUnipotentAffineGroupSchemeProperty k).FullSubcategory

theorem TauCeti.smooth_of_smoothUnipotentAffineGroupSchemeProperty (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : smoothUnipotentAffineGroupSchemeProperty k G) : AlgebraicGeometry.Smooth G.obj.obj.X.hom

A finite-type affine group scheme satisfying the smooth-unipotence property has smooth structural morphism.

instance TauCeti.instSmoothHomSchemeXOverSpecOfObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemePropertyFiniteTypeAffineGroupSchemeCatSmoothUnipotentAffineGroupSchemeProperty (k : Type u) [Field k] (G : SmoothUnipotentAffineGroupSchemeCat k) : AlgebraicGeometry.Smooth G.obj.obj.obj.X.hom

Objects of SmoothUnipotentAffineGroupSchemeCat k have smooth structural morphism.

theorem TauCeti.smoothUnipotentAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] : (smoothUnipotentAffineGroupSchemeProperty k).inverseImage (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).functor = (smoothUnipotentCommHopfAlgProperty k).op

Under the finite-type affine Hopf/group-scheme anti-equivalence, the inverse image of smooth unipotence on group schemes is smooth unipotence of coordinate Hopf algebras.

noncomputable def TauCeti.smoothUnipotentCommHopfAlgCatOpEquivSmoothUnipotentAffineGroupSchemeCat (k : Type u) [Field k] : (SmoothUnipotentCommHopfAlgCat k)ᵒᵖ ≌ SmoothUnipotentAffineGroupSchemeCat k

Spec restricts to an anti-equivalence from smooth unipotent finite-type commutative Hopf algebras to smooth unipotent affine group schemes.

Equations

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

noncomputable def TauCeti.smoothUnipotentCommHopfAlgCatOpEquivSmoothUnipotentAffineGroupSchemeCat.functorCompιIso (k : Type u) [Field k] : (smoothUnipotentCommHopfAlgCatOpEquivSmoothUnipotentAffineGroupSchemeCat k).functor.comp ((smoothUnipotentAffineGroupSchemeProperty k).ι.comp ((finiteTypeAffineGroupSchemeProperty ↧k).ι.comp (affineGroupSchemeProperty ↧k).ι)) ≅ (CategoryTheory.forget₂ (SmoothUnipotentCommHopfAlgCat k) (FiniteTypeCommHopfAlgCat k)).op.comp ((CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat k) (CommHopfAlgCat k)).op.comp (AlgebraicGeometry.hopfSpec ↧k))

The forward smooth-unipotent anti-equivalence, followed by the inclusions into finite-type affine group schemes and affine group schemes, is Mathlib's hopfSpec after forgetting the smooth-unipotent and finite-type proofs. This is the computation interface for the restricted equivalence.

Equations

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