Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Torus

Torus affine group schemes #

This file transports the coordinate-Hopf-algebra definition of a torus to finite-type affine group schemes over a field. A group scheme is a torus when its coordinate Hopf algebra becomes a finite-rank split-torus coordinate ring after extension to an algebraic closure.

The resulting full subcategory is anti-equivalent to torus coordinate Hopf algebras. Every object in it is of multiplicative type and reductive, synchronizing these structural theorems between the coordinate and scheme models.

Main declarations #

References #

This supplies the scheme-side torus model and its reductivity theorem for Layers 4 and 6 of the ReductiveGroups roadmap.

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

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

The property is transported through the finite-type affine Hopf/group-scheme anti-equivalence, so it retains the coordinate definition by splitting over an algebraic closure.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.torusAffineGroupSchemeProperty_iff (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) :
    torusAffineGroupSchemeProperty k G ↔ torusCommHopfAlgProperty k (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G))

    A finite-type affine group scheme is a torus exactly when its coordinate Hopf algebra, supplied by the affine anti-equivalence, is a torus.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeAffineGroupSchemeCatOfTorusAffineGroupSchemeProperty (k : Type u) [Field k] :
    (torusAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

    Being a torus is invariant under isomorphisms of finite-type affine group schemes.

    source
    @[reducible, inline]
    abbrev TauCeti.TorusAffineGroupSchemeCat (k : Type u) [Field k] :
    Type (u + 1)

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

    Equations
    Instances For
      source
      theorem TauCeti.torusAffineGroupSchemeProperty.multiplicativeType (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : torusAffineGroupSchemeProperty k G) :
      multiplicativeTypeAffineGroupSchemeProperty k G

      Every torus affine group scheme over a field is of multiplicative type.

      source
      theorem TauCeti.torusAffineGroupSchemeProperty.reductive (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : torusAffineGroupSchemeProperty k G) :
      reductiveAffineGroupSchemeProperty k G

      Every torus affine group scheme over a field is reductive.

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

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

      source
      instance TauCeti.instSmoothHomSchemeXOverSpecOfObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemePropertyFiniteTypeAffineGroupSchemeCatTorusAffineGroupSchemeProperty (k : Type u) [Field k] (G : TorusAffineGroupSchemeCat k) :
      AlgebraicGeometry.Smooth G.obj.obj.obj.X.hom

      Objects of TorusAffineGroupSchemeCat k have smooth structural morphism.

      source
      theorem TauCeti.geometricallyConnected_of_torusAffineGroupSchemeProperty (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : torusAffineGroupSchemeProperty k G) :
      AlgebraicGeometry.GeometricallyConnected G.obj.obj.X.hom

      A finite-type affine group scheme satisfying the torus property has geometrically connected structural morphism.

      source
      instance TauCeti.instGeometricallyConnectedHomSchemeXOverSpecOfObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemePropertyFiniteTypeAffineGroupSchemeCatTorusAffineGroupSchemeProperty (k : Type u) [Field k] (G : TorusAffineGroupSchemeCat k) :
      AlgebraicGeometry.GeometricallyConnected G.obj.obj.obj.X.hom

      Objects of TorusAffineGroupSchemeCat k have geometrically connected structural morphism.

      source
      theorem TauCeti.torusAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] :
      (torusAffineGroupSchemeProperty k).inverseImage (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).functor = (torusCommHopfAlgProperty k).op

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

      source
      noncomputable def TauCeti.torusCommHopfAlgCatOpEquivTorusAffineGroupSchemeCat (k : Type u) [Field k] :
      (TorusCommHopfAlgCat k)ᵒᵖ ≌ TorusAffineGroupSchemeCat k

      Spec restricts to an anti-equivalence from torus coordinate Hopf algebras to torus affine group schemes.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.torusCommHopfAlgCatOpEquivTorusAffineGroupSchemeCat.functorCompιIso (k : Type u) [Field k] :
        (torusCommHopfAlgCatOpEquivTorusAffineGroupSchemeCat k).functor.comp ((torusAffineGroupSchemeProperty k).ι.comp ((finiteTypeAffineGroupSchemeProperty ↧k).ι.comp (affineGroupSchemeProperty ↧k).ι)) ≅ (CategoryTheory.forget₂ (TorusCommHopfAlgCat k) (FiniteTypeCommHopfAlgCat k)).op.comp ((CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat k) (CommHopfAlgCat k)).op.comp (AlgebraicGeometry.hopfSpec ↧k))

        The forward torus anti-equivalence, followed by the inclusions into finite-type affine group schemes and affine group schemes, is Mathlib's hopfSpec after forgetting the torus 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.
        Instances For