Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Reductive.Basic

Reductive affine group schemes #

This file transports reductivity from finite-type commutative Hopf algebras to affine group schemes of finite type over a field. The coordinate-ring predicate says that the group is smooth and geometrically connected and that its geometric fibre has no nontrivial connected normal smooth unipotent closed subgroup.

The resulting full subcategory is anti-equivalent to reductive finite-type commutative Hopf algebras (ReductiveCommHopfAlgCat). This synchronizes the coordinate-ring and scheme models of reductive groups. Smoothness is part of the transported predicate, while finite type is enforced by the ambient category rather than baked into a monolithic notion of algebraic group.

Main declarations #

References #

This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. It is the scheme-side form of the geometric definition and supplies the model needed for the radical, centre, derived group, central isogenies, and simply connected and adjoint forms.

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

The object property selecting reductive 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 presents the coordinate-ring definition on the scheme side without choosing a descended unipotent radical over the ground field.

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

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

    source
    instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeAffineGroupSchemeCatOfReductiveAffineGroupSchemeProperty (k : Type u) [Field k] :
    (reductiveAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

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

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

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

    Equations
    Instances For
      source
      theorem TauCeti.smooth_of_reductiveAffineGroupSchemeProperty (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : reductiveAffineGroupSchemeProperty k G) :
      AlgebraicGeometry.Smooth G.obj.obj.X.hom

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

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

      Objects of ReductiveAffineGroupSchemeCat k have smooth structural morphism.

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

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

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

      Objects of ReductiveAffineGroupSchemeCat k have geometrically connected structural morphism.

      source
      theorem TauCeti.reductiveAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] :
      (reductiveAffineGroupSchemeProperty k).inverseImage (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).functor = (reductiveCommHopfAlgProperty k).op

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

      source
      noncomputable def TauCeti.reductiveCommHopfAlgCatOpEquivReductiveAffineGroupSchemeCat (k : Type u) [Field k] :
      (ReductiveCommHopfAlgCat k)ᵒᵖ ≌ ReductiveAffineGroupSchemeCat k

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

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

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