Affine group schemes are anti-equivalent to commutative Hopf algebras

Over a commutative ring S, the contravariant functor Spec is an equivalence from the opposite of the category of commutative S-Hopf algebras onto the category of affine group schemes over Spec S. This is the assembled Layer 0 dictionary of the reductive-groups roadmap.

Mathlib's AlgebraicGeometry/Group/Affine.lean provides the functor (AlgebraicGeometry.hopfSpec), its full faithfulness, and the characterization of its essential image as the affine group schemes (AlgebraicGeometry.essImage_hopfSpec); this file composes them into the equivalence with the category TauCeti.AffineGroupSchemeCat of the parent file.

TauCeti.AffineGroupSchemeCat.hopfSpecCoordinateHopfAlgebraIso identifies an affine group scheme with the Hopf spectrum of its coordinate algebra, using the counit of this equivalence.

noncomputable def TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat (S : CommRingCat) : (CommHopfAlgCat ↑S)ᵒᵖ ≌ AffineGroupSchemeCat S

Spec as an anti-equivalence from commutative S-Hopf algebras onto affine group schemes over Spec S. The underlying functor is Mathlib's AlgebraicGeometry.hopfSpec, which is fully faithful with essential image the affine group schemes; the isomorphism commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso records this on the level of functors, and is the intended interface for computing with the equivalence.

Equations

• TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat S = (AlgebraicGeometry.hopfSpec S).toEssImage.asEquivalence.trans (CategoryTheory.ObjectProperty.fullSubcategoryCongr ⋯)

noncomputable def TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso (S : CommRingCat) : (commHopfAlgCatOpEquivAffineGroupSchemeCat S).functor.comp (affineGroupSchemeProperty S).ι ≅ AlgebraicGeometry.hopfSpec S

The forward functor of commHopfAlgCatOpEquivAffineGroupSchemeCat, followed by the inclusion of the full subcategory, is hopfSpec: the anti-equivalence really does act by Spec. Consumers should transport along this isomorphism (and its app components and naturality squares) rather than unfold the equivalence.

Equations

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

noncomputable def TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat.functorObjIso (R : Type u) [CommRing R] (H : (CommHopfAlgCat R)ᵒᵖ) : (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor.obj H ≅ { obj := (AlgebraicGeometry.hopfSpec ↧R).obj H, property := ⋯ }

The object produced by the affine Hopf/group-scheme anti-equivalence is the bundled Hopf spectrum.

Equations

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

noncomputable def TauCeti.AffineGroupSchemeCat.hopfSpecCoordinateHopfAlgebraIso (R : Type u) [CommRing R] (G : AffineGroupSchemeCat ↧R) : (AlgebraicGeometry.hopfSpec ↧R).obj ((commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).inverse.obj G) ≅ G.obj

An affine group scheme is the Hopf spectrum of its coordinate Hopf algebra.

Equations

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

theorem TauCeti.objectProperty_inverseImage_commHopfAlgCatOpEquiv (R : Type u) [CommRing R] (P : CategoryTheory.ObjectProperty (AffineGroupSchemeCat ↧R)) [P.IsClosedUnderIsomorphisms] (Q : CategoryTheory.ObjectProperty (CommHopfAlgCat R)) (h : ∀ (H : CommHopfAlgCat ↑↧R), P { obj := (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H), property := ⋯ } ↔ Q H) : P.inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor = Q.op

To identify the inverse image of an isomorphism-invariant property of affine group schemes under the Hopf-algebra/group-scheme anti-equivalence, it suffices to identify that property on Hopf spectra.