Documentation

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Equivalence

The anti-equivalence for diagonalizable group schemes #

Over a field k, a group scheme over Spec k is diagonalizable when it is isomorphic to the spectrum of a finite-type commutative Hopf algebra whose group-like elements span its carrier. This file identifies that property with the essential image of DiagonalizableGroup.schemeFunctor and packages the resulting anti-equivalence from finitely generated commutative groups.

The equivalence is contravariant: its source is FGCommGrpCatᵒᵖ. Its forward functor recovers DiagonalizableGroup.schemeFunctor after inclusion into all group schemes. Bundled diagonalizable group schemes automatically expose affineness and local finite type over Spec k.

All categories and carriers lie in the universe of k, as required by the current AlgebraicGeometry.hopfSpec construction.

Main declarations #

References #

See Milne, Algebraic Groups, Definition 12.7 and Theorems 12.8--12.9.

The equivalence packaging follows TauCeti.AlgebraicGeometry.AffineGroupScheme.Equivalence, specifically commHopfAlgCatOpEquivAffineGroupSchemeCat and commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso.

source
def TauCeti.DiagonalizableGroup.diagonalizableGroupSchemeProperty (k : Type u) [Field k] :
CategoryTheory.ObjectProperty (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)))

The property of group schemes over Spec k that are spectra of finite-type commutative Hopf algebras spanned by their group-like elements.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.diagonalizableGroupSchemeProperty_iff (k : Type u) [Field k] (G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))) :
    diagonalizableGroupSchemeProperty k G ↔ ∃ (H : FiniteTypeCommHopfAlgCat k), groupLikeSpannedProperty k H ∧ Nonempty ((AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H.obj) ≅ G)

    A group scheme over Spec k is diagonalizable exactly when it is isomorphic to the spectrum of a finite-type commutative Hopf algebra spanned by its group-like elements.

    source
    theorem TauCeti.DiagonalizableGroup.essImage_schemeFunctor (k : Type u) [Field k] :
    (schemeFunctor k).essImage = diagonalizableGroupSchemeProperty k

    The diagonalizable group schemes are precisely the essential image of the existing contravariant diagonalizable group-scheme functor.

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

    The category of diagonalizable group schemes over Spec k.

    Equations
    Instances For
      source
      instance TauCeti.DiagonalizableGroup.instIsAffineLeftSchemeXOverSpecOfObjGrpDiagonalizableGroupSchemeProperty (k : Type u) [Field k] (G : DiagonalizableGroupSchemeCat k) :
      AlgebraicGeometry.IsAffine G.obj.X.left

      A bundled diagonalizable group scheme is affine.

      source
      instance TauCeti.DiagonalizableGroup.instLocallyOfFiniteTypeHomSchemeXOverSpecOfObjGrpDiagonalizableGroupSchemeProperty (k : Type u) [Field k] (G : DiagonalizableGroupSchemeCat k) :
      AlgebraicGeometry.LocallyOfFiniteType G.obj.X.hom

      The structural morphism of a bundled diagonalizable group scheme is locally of finite type.

      source
      noncomputable def TauCeti.DiagonalizableGroup.schemeEquivalence (k : Type u) [Field k] :
      FGCommGrpCatᵒᵖ ≌ DiagonalizableGroupSchemeCat k

      Finitely generated commutative groups, with arrows reversed, are equivalent to diagonalizable group schemes over Spec k.

      Equations
      Instances For
        source
        noncomputable def TauCeti.DiagonalizableGroup.schemeEquivalence.functorCompιIso (k : Type u) [Field k] :
        (schemeEquivalence k).functor.comp (diagonalizableGroupSchemeProperty k).ι ≅ schemeFunctor k

        The forward functor of schemeEquivalence, followed by the inclusion into all group schemes, is the existing diagonalizable group-scheme functor.

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