Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.MultiplicativeType

Affine group schemes of multiplicative type #

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

The resulting full subcategory is anti-equivalent to multiplicative-type coordinate Hopf algebras. This synchronizes the coordinate and scheme models without requiring the group to split over the ground field; finite diagonalizable groups and non-split tori both belong to the resulting category.

Main declarations #

References #

This supplies the scheme-side model required by Layer 4, "Diagonalizable groups and groups of multiplicative type", of the ReductiveGroups roadmap. The construction follows the transport pattern of TauCeti.AlgebraicGeometry.AffineGroupScheme.Torus.

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

The object property selecting affine group schemes of multiplicative 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 diagonalizability after extension to an algebraic closure.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.multiplicativeTypeAffineGroupSchemeProperty_iff (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) :
    multiplicativeTypeAffineGroupSchemeProperty k G ↔ multiplicativeTypeCommHopfAlgProperty k (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G))

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

    source
    instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeAffineGroupSchemeCatOfMultiplicativeTypeAffineGroupSchemeProperty (k : Type u) [Field k] :
    (multiplicativeTypeAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

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

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

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

    Equations
    Instances For
      source
      theorem TauCeti.multiplicativeTypeAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] :
      (multiplicativeTypeAffineGroupSchemeProperty k).inverseImage (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).functor = (multiplicativeTypeCommHopfAlgProperty k).op

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

      source
      noncomputable def TauCeti.multiplicativeTypeCommHopfAlgCatOpEquivMultiplicativeTypeAffineGroupSchemeCat (k : Type u) [Field k] :
      (MultiplicativeTypeCommHopfAlgCat k)ᵒᵖ ≌ MultiplicativeTypeAffineGroupSchemeCat k

      Spec restricts to an anti-equivalence from multiplicative-type coordinate Hopf algebras to affine group schemes of multiplicative type.

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

        The forward multiplicative-type anti-equivalence, followed by the inclusions into finite-type affine group schemes and affine group schemes, is Mathlib's hopfSpec after forgetting the multiplicative-type and finite-type proofs.

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