Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Basic

The category of affine group schemes over Spec S #

This file introduces the category of affine group schemes over Spec S for a commutative ring S — the full subcategory of group objects in schemes over Spec S whose underlying scheme is affine — together with the Γ-direction endpoint of the reductive-groups roadmap's Layer 0 dictionary, stated for a plain-typed base ring R and an arbitrary structure morphism rather than through Scheme.Over instance data: a commutative R-Hopf algebra structure on the global sections of an affine group scheme φ : G ⟶ Spec R (hopfAlgebraGamma).

The Spec-direction endpoint — the group-object structure on Spec A over Spec R for a commutative R-Hopf algebra A — needs no declaration here: it is Mathlib's AlgebraicGeometry.instGrpObjSpecAsOverSpec, and its Over.mk spelling is reached by inferInstanceAs (GrpObj ((Spec (CommRingCat.of A)).asOver (Spec (CommRingCat.of R)))) at any use site. Everything consumes the instances of Mathlib's AlgebraicGeometry/Group/Affine.lean. Affineness enters only as the object property cutting out the full subcategory; further refinements stay predicates rather than being baked into the category. The anti-equivalence with commutative S-Hopf algebras is in TauCeti/AlgebraicGeometry/AffineGroupScheme/Equivalence.lean.

source
def TauCeti.affineGroupSchemeProperty (S : CommRingCat) :
CategoryTheory.ObjectProperty (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec S)))

The object property on group objects in schemes over Spec S selecting those whose underlying scheme is affine. Over the affine base Spec S this is equivalent to the structure morphism being an affine morphism; over a general base scheme only the relative notion is correct, so this property must not be transplanted verbatim there.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.affineGroupSchemeProperty_iff {S : CommRingCat} (G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec S))) :
    affineGroupSchemeProperty S G ↔ AlgebraicGeometry.IsAffine G.X.left

    Membership in the affine-group-scheme object property.

    source
    @[reducible, inline]
    abbrev TauCeti.AffineGroupSchemeCat (S : CommRingCat) :
    Type (u + 1)

    The category of affine group schemes over Spec S: the full subcategory of group objects in schemes over Spec S whose underlying scheme is affine.

    Equations
    Instances For
      source
      instance TauCeti.instIsClosedUnderIsomorphismsGrpOverSchemeSpecAffineGroupSchemeProperty (S : CommRingCat) :
      (affineGroupSchemeProperty S).IsClosedUnderIsomorphisms

      Being an affine group scheme is invariant under isomorphism of group objects: an isomorphism induces an isomorphism of underlying schemes, and affineness transfers along it.

      source
      instance TauCeti.instIsAffineLeftSchemeXOverSpecObjGrpAffineGroupSchemeProperty {S : CommRingCat} (G : AffineGroupSchemeCat S) :
      AlgebraicGeometry.IsAffine G.obj.X.left

      Membership in AffineGroupSchemeCat supplies affineness of the underlying scheme automatically, so downstream instance searches need not invoke property by hand.

      source
      @[instance_reducible]
      noncomputable def TauCeti.hopfAlgebraGamma {R : Type u} [CommRing R] {G : AlgebraicGeometry.Scheme} (φ : G ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)) [CategoryTheory.GrpObj (CategoryTheory.Over.mk φ)] [AlgebraicGeometry.IsAffine G] :
      HopfAlgebra R ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op G))

      The global sections of an affine group scheme φ : G ⟶ Spec R are a commutative R-Hopf algebra. This is the Γ-direction endpoint of the Layer 0 dictionary, stated for an arbitrary structure morphism φ with the group structure carried by the object Over.mk φ of schemes over Spec R — a statement Mathlib's Scheme.Over-instance form cannot express directly. Not an instance, because φ is data that instance search cannot recover from the goal.

      Equations
      Instances For