Documentation

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.EssentialImage

The essential image of diagonalizable coordinate Hopf algebras #

Over a field k, a finite-type commutative Hopf algebra is the coordinate algebra of a diagonalizable group exactly when its group-like elements span the whole carrier. This file identifies that intrinsic object property with the essential image of DiagonalizableGroup.coordinateRingFunctor and packages the resulting equivalence of categories.

The proof reconstructs a group-like-spanned Hopf algebra H from its group of group-like elements. The canonical evaluation map k[GroupLike k H] → H is a bialgebra equivalence: spanning gives surjectivity, while linear independence of group-like elements over a field gives injectivity. Finite type then implies that GroupLike k H is finitely generated. Conversely, the standard basis elements of every group algebra are group-like and span, and this property is invariant under coalgebra equivalence.

All categories and carriers in the equivalence lie in the universe of k. Applying Spec, and the resulting scheme-side anti-equivalence, are outside the scope of this file.

Main declarations #

References #

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

source
def TauCeti.DiagonalizableGroup.groupLikeSpannedProperty (k : Type u) [Field k] :
CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting finite-type commutative Hopf algebras whose group-like elements span the whole carrier.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.groupLikeSpannedProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) :
    groupLikeSpannedProperty k H ↔ Subcoalgebra.groupLikeSetSpan Set.univ = ⊤

    Membership in the group-like-spanned object property.

    source
    theorem TauCeti.DiagonalizableGroup.essImage_coordinateRingFunctor (k : Type u) [Field k] :
    (coordinateRingFunctor k).essImage = groupLikeSpannedProperty k

    The essential image of the finite-type diagonalizable coordinate-ring functor consists exactly of the finite-type commutative Hopf algebras spanned by their group-like elements.

    source
    instance TauCeti.DiagonalizableGroup.groupLikeSpannedProperty_isClosedUnderIsomorphisms (k : Type u) [Field k] :
    (groupLikeSpannedProperty k).IsClosedUnderIsomorphisms

    The property of being spanned by group-like elements is invariant under isomorphisms of finite-type commutative Hopf algebras.

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

    The category of finite-type commutative Hopf algebras spanned by their group-like elements.

    Equations
    Instances For
      source
      noncomputable def TauCeti.DiagonalizableGroup.coordinateRingEquivalence (k : Type u) [Field k] :
      FGCommGrpCat ≌ GroupLikeSpannedCommHopfAlgCat k

      Finitely generated commutative groups are equivalent to finite-type commutative Hopf algebras spanned by their group-like elements, via the group-algebra coordinate-ring functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.DiagonalizableGroup.coordinateRingEquivalence.functorCompιIso (k : Type u) [Field k] :
        (coordinateRingEquivalence k).functor.comp (groupLikeSpannedProperty k).ι ≅ coordinateRingFunctor k

        The forward functor of coordinateRingEquivalence, followed by the inclusion into all finite-type commutative Hopf algebras, is the coordinate-ring functor.

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