Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Smooth

Smooth affine group schemes #

This file records smoothness of affine group schemes as an object property and compares it with smoothness of their coordinate Hopf algebras. On the coordinate side, smoothness is Algebra.Smooth R H. On the scheme side, it is smoothness of the structural morphism G ⟶ Spec R.

The key comparison is TauCeti.algebraSmooth_iff_smooth_hopfSpec: a commutative Hopf algebra is smooth over its base exactly when the structural morphism of its Hopf spectrum is smooth. Smoothness remains a separate object property rather than being built into the definition of an affine group scheme, so finite-type group schemes that are non-smooth over a characteristic-p base, such as μₚ and αₚ, remain in the ambient category.

Main declarations #

References #

The comparison uses Mathlib's AlgebraicGeometry.hopfSpec, AlgebraicGeometry.HasRingHomProperty.Spec_iff, and RingHom.smooth_algebraMap. This is the explicit smoothness predicate requested in the standing hypotheses of the ReductiveGroups roadmap. Its organization follows AffineGroupScheme/FiniteType.lean, especially TauCeti.algebraFiniteType_iff_locallyOfFiniteType_hopfSpec.

source
def TauCeti.smoothAffineGroupSchemeProperty (S : CommRingCat) :
CategoryTheory.ObjectProperty (AffineGroupSchemeCat S)

The object property on affine group schemes over Spec S selecting those whose structural morphism is smooth.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.smoothAffineGroupSchemeProperty_iff (S : CommRingCat) (G : AffineGroupSchemeCat S) :
    smoothAffineGroupSchemeProperty S G ↔ AlgebraicGeometry.Smooth G.obj.X.hom

    Membership in the smooth affine-group-scheme object property.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsAffineGroupSchemeCatSmoothAffineGroupSchemeProperty (S : CommRingCat) :
    (smoothAffineGroupSchemeProperty S).IsClosedUnderIsomorphisms

    Smoothness of the structural morphism is invariant under isomorphism of affine group schemes. This lets the predicate transport through equivalences.

    source
    theorem TauCeti.algebraSmooth_iff_smooth_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) :
    smoothCommHopfAlgProperty R H ↔ smoothAffineGroupSchemeProperty ↧R { obj := (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H), property := ⋯ }

    A commutative Hopf algebra is smooth over its base exactly when the structural morphism of its Hopf spectrum is smooth.

    This is the predicate-level compatibility needed to restrict the affine Hopf/group-scheme anti-equivalence to smooth objects.

    source
    theorem TauCeti.smoothAffineGroupSchemeProperty_inverseImage (R : Type u) [CommRing R] :
    (smoothAffineGroupSchemeProperty ↧R).inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor = (smoothCommHopfAlgProperty R).op

    Under the affine Hopf/group-scheme anti-equivalence, the inverse image of the smooth scheme property is the smooth coordinate-algebra property.

    source
    theorem TauCeti.smooth_iff_algebraSmooth_coordinate (R : Type u) [CommRing R] (G : FiniteTypeAffineGroupSchemeCat ↧R) :
    AlgebraicGeometry.Smooth G.obj.obj.X.hom ↔ Algebra.Smooth R ↑(Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat R).inverse.obj G)).obj

    A finite-type affine group scheme has smooth structural morphism exactly when its coordinate algebra supplied by the affine anti-equivalence is smooth.