The equivalence between Hopf algebras and affine group schemes

This file constructs Spec as a functor from R-Hopf algebras to group schemes over Spec R, shows it is full and faithful, and has affine group schemes as essential image.

We want to show that Hopf algebras correspond to affine group schemes. This can easily be done categorically assuming both categories on either side are defined thoughtfully. However, the categorical version will not be workable with if we do not also have links to the non-categorical notions. Therefore, one solution would be to build the left, top and right edges of the following diagram so that the bottom edge can be obtained by composing the three.

  Cogrp Mod_R ≌ Grp AffSch_{Spec R} ≌ Aff Grp Sch_{Spec R}
      ↑ ↓                                      ↑ ↓
R-Hopf algebras         ≃       Affine group schemes over Spec R

If we do not care about going back from affine group schemes over Spec R to R-Hopf algebras (eg because all our affine group schemes are given as the Spec of some algebra), then we can follow the following simpler diagram:

  Cogrp Mod_R   ⥤        Grp Sch_{Spec R}
      ↑ ↓                        ↓
R-Hopf algebras → Affine group schemes over Spec R

where the top ≌ comes from the essentially surjective functor Cogrp Mod_R ⥤ Grp Sch_{Spec R}, so that in particular we do not easily know that its inverse is given by Γ.

Left edge: R-Hopf algebras correspond to cogroup objects under R

Ways to turn an unbundled R-Hopf algebra into a bundled cogroup object under R, and vice versa, are already provided in Toric.Mathlib.Algebra.Category.CommHopfAlgCat.

Top edge: Spec as a functor on Hopf algebras

In this section we construct Spec as a functor from R-Hopf algebras to affine group schemes over Spec R.

@[reducible, inline]

noncomputable abbrev algSpec (R : CommRingCat) : CategoryTheory.Functor (CommAlgCat ↑R)ᵒᵖ (CategoryTheory.Over (AlgebraicGeometry.Spec R))

Spec as a functor from R-algebras to schemes over Spec R.

Equations

• algSpec R = (commAlgCatEquivUnder R).op.functor.comp ((CategoryTheory.Over.opEquivOpUnder R).inverse.comp (CategoryTheory.Over.post AlgebraicGeometry.Scheme.Spec))

@[reducible, inline]

noncomputable abbrev algΓ (R : CommRingCat) : CategoryTheory.Functor (CategoryTheory.Over (AlgebraicGeometry.Spec R)) (CommAlgCat ↑R)ᵒᵖ

The Gamma functor as a functor from schemes over Spec R to R-algebras.

Equations

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

instance preservesLimitsOfSize_algSpec {R : CommRingCat} : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (algSpec R)

instance preservesColimitsOfSize_algΓ {R : CommRingCat} : CategoryTheory.Limits.PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (algΓ R)

noncomputable instance braided_algSpec {R : CommRingCat} : (algSpec R).Braided

Equations

• braided_algSpec = CategoryTheory.Functor.Braided.ofChosenFiniteProducts (algSpec R)

@[simp]

theorem algSpec_ε_left {R : CommRingCat} : (CategoryTheory.Functor.LaxMonoidal.ε (algSpec R)).left = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)

@[simp]

theorem algSpec_η_left {R : CommRingCat} : (CategoryTheory.Functor.OplaxMonoidal.η (algSpec R)).left = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)

@[simp]

theorem algSpec_δ_left {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ) : (CategoryTheory.Functor.OplaxMonoidal.δ (algSpec R) X Y).left = (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).inv

@[simp]

theorem algSpec_μ_left {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ) : (CategoryTheory.Functor.LaxMonoidal.μ (algSpec R) X Y).left = (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).hom

@[simp]

theorem prodComparison_algSpec_left {R : CommRingCat} (A B : (CommAlgCat ↑R)ᵒᵖ) : (CategoryTheory.CartesianMonoidalCategory.prodComparison (algSpec R) A B).left = (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop A) ↑(Opposite.unop B)).inv

@[simp]

theorem prodComparisonIso_algSpec_inv_left {R : CommRingCat} (A B : (CommAlgCat ↑R)ᵒᵖ) : (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (algSpec R) A B).inv.left = (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop A) ↑(Opposite.unop B)).hom

theorem preservesTerminalIso_algSpec {R : CommRingCat} : CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (algSpec R) = CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (AlgebraicGeometry.Spec R)) ⋯

@[simp]

theorem preservesTerminalIso_algSpec_inv_left {R : CommRingCat} : (CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (algSpec R)).inv.left = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)

instance algSpec.instFull {R : CommRingCat} : (algSpec R).Full

Spec is full on R-algebras.

instance algSpec.instFaithful {R : CommRingCat} : (algSpec R).Faithful

Spec is faithful on R-algebras.

noncomputable def algSpec.fullyFaithful {R : CommRingCat} : (algSpec R).FullyFaithful

Spec is fully faithful on R-algebras, with inverse Gamma.

Equations

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

@[reducible, inline]

noncomputable abbrev bialgSpec (R : CommRingCat) : CategoryTheory.Functor (CommBialgCat ↑R)ᵒᵖ (CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R)))

Spec as a functor from R-bialgebras to monoid schemes over Spec R.

Equations

• bialgSpec R = (commBialgCatEquivComonCommAlgCat ↑R).functor.leftOp.comp (algSpec R).mapMon

instance bialgSpec.instFull {R : CommRingCat} : (bialgSpec R).Full

Spec is full on R-bialgebras.

instance bialgSpec.instFaithful {R : CommRingCat} : (bialgSpec R).Faithful

Spec is faithful on R-bialgebras.

noncomputable def bialgSpec.fullyFaithful {R : CommRingCat} : (bialgSpec R).FullyFaithful

Spec is fully faithful on R-bialgebras, with inverse Gamma.

Equations

• bialgSpec.fullyFaithful = (commBialgCatEquivComonCommAlgCat ↑R).fullyFaithfulFunctor.leftOp.comp algSpec.fullyFaithful.mapMon

@[reducible, inline]

noncomputable abbrev hopfSpec (R : CommRingCat) : CategoryTheory.Functor (CommHopfAlgCat ↑R)ᵒᵖ (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec R)))

Spec as a functor from R-Hopf algebras to group schemes over Spec R.

Equations

• hopfSpec R = (commHopfAlgCatEquivCogrpCommAlgCat ↑R).functor.leftOp.comp (algSpec R).mapGrp

instance hopfSpec.instFull {R : CommRingCat} : (hopfSpec R).Full

Spec is full on R-Hopf algebras.

instance hopfSpec.instFaithful {R : CommRingCat} : (hopfSpec R).Faithful

Spec is faithful on R-Hopf algebras.

noncomputable def hopfSpec.fullyFaithful {R : CommRingCat} : (hopfSpec R).FullyFaithful

Spec is fully faithful on R-Hopf algebras, with inverse Gamma.

Equations

• hopfSpec.fullyFaithful = (commHopfAlgCatEquivCogrpCommAlgCat ↑R).fullyFaithfulFunctor.leftOp.comp algSpec.fullyFaithful.mapGrp

noncomputable instance AlgebraicGeometry.Scheme.specOverSpec {R A : CommRingCat} [Algebra ↑R ↑A] : (Spec A).Over (Spec R)

Equations

• AlgebraicGeometry.Scheme.specOverSpec = { hom := AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)) }

theorem AlgebraicGeometry.Scheme.specOverSpec_over {R A : CommRingCat} [Algebra ↑R ↑A] : Spec A ↘ Spec R = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))

instance AlgebraicGeometry.Scheme.locallyOfFiniteType_specOverSpec {R A : CommRingCat} [Algebra ↑R ↑A] [Algebra.FiniteType ↑R ↑A] : LocallyOfFiniteType (Spec A ↘ Spec R)

noncomputable instance AlgebraicGeometry.Scheme.asOver.instMonObj {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj ((Spec A).asOver (Spec R))

Equations

• AlgebraicGeometry.Scheme.asOver.instMonObj = ((bialgSpec R).obj (Opposite.op (CommBialgCat.of ↑R ↑A))).mon

@[simp]

theorem AlgebraicGeometry.Scheme.asOver.one_def {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (algSpec R)) (CategoryTheory.Over.homMk (Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))) ⋯)

theorem AlgebraicGeometry.Scheme.specOverSpec_one {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (algSpec R)) (CategoryTheory.Over.homMk (Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))) ⋯)

theorem AlgebraicGeometry.Scheme.specOverSpec_one_left {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one.left = Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))

theorem AlgebraicGeometry.Scheme.μIso_algSpec_inv_left {R A : CommRingCat} [Algebra ↑R ↑A] : (CategoryTheory.Functor.Monoidal.μIso (algSpec R) (Opposite.op (CommAlgCat.of ↑R ↑A)) (Opposite.op (CommAlgCat.of ↑R ↑A))).inv.left = (pullbackSpecIso ↑R ↑A ↑A).inv

theorem AlgebraicGeometry.Scheme.μ_algSpec_left {R A : CommRingCat} [Algebra ↑R ↑A] : (CategoryTheory.Functor.LaxMonoidal.μ (algSpec R) (Opposite.op (CommAlgCat.of ↑R ↑A)) (Opposite.op (CommAlgCat.of ↑R ↑A))).left = (pullbackSpecIso ↑R ↑A ↑A).hom

theorem AlgebraicGeometry.Scheme.mul_left {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.mul.left = CategoryTheory.CategoryStruct.comp (pullbackSpecIso ↑R ↑A ↑A).hom (Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom ↑R ↑A)))

instance AlgebraicGeometry.Scheme.asOver.instIsCommMonObj {R A : CommRingCat} [Bialgebra ↑R ↑A] [Coalgebra.IsCocomm ↑R ↑A] : CategoryTheory.IsCommMonObj ((Spec A).asOver (Spec R))

noncomputable instance AlgebraicGeometry.Scheme.asOver.instGrpObj {R A : CommRingCat} [HopfAlgebra ↑R ↑A] : CategoryTheory.GrpObj ((Spec A).asOver (Spec R))

Equations

• AlgebraicGeometry.Scheme.asOver.instGrpObj = ((hopfSpec R).obj (Opposite.op (CommHopfAlgCat.of ↑R ↑A))).grp

noncomputable instance AlgebraicGeometry.Scheme.asOver.instCommGrpObj {R A : CommRingCat} [HopfAlgebra ↑R ↑A] [Coalgebra.IsCocomm ↑R ↑A] : CategoryTheory.CommGrpObj ((Spec A).asOver (Spec R))

Equations

• AlgebraicGeometry.Scheme.asOver.instCommGrpObj = { toGrpObj := AlgebraicGeometry.Scheme.asOver.instGrpObj, toIsCommMonObj := ⋯ }

instance AlgebraicGeometry.Scheme.instIsOverMapOfHomSpecOf_toric {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) : Hom.IsOver (Spec.map (CommRingCat.ofHom f.toRingHom)) (Spec { carrier := R, commRing := inst✝ })

noncomputable def AlgebraicGeometry.Scheme.Spec.mapMulEquiv {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Bialgebra R S] [Algebra R T] : (S →ₐ[R] T) ≃* ((Spec { carrier := T, commRing := inst✝ }).asOver (Spec { carrier := R, commRing := inst✝¹ }) ⟶ (Spec { carrier := S, commRing := inst✝² }).asOver (Spec { carrier := R, commRing := inst✝¹ }))

Spec.map as a MulEquiv on hom-sets.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.algΓAlgSpecAdjunction (R : CommRingCat) : algΓ R ⊣ algSpec R

The adjunction between Spec and Γ as functors between commutative R-algebras and schemes over Spec R.

Equations

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

noncomputable instance AlgebraicGeometry.Scheme.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfOverSpecOfIsAffine_toric {R : CommRingCat} {X : Scheme} [X.Over (Spec R)] [IsAffine X] : Algebra ↑R ↑(X.presheaf.obj (Opposite.op ⊤))

The global sections of an affine scheme over Spec R are a R-algebra.

Equations

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

theorem AlgebraicGeometry.Scheme.algebraMap_Γ {R : CommRingCat} {X : Scheme} [X.Over (Spec R)] [IsAffine X] : algebraMap ↑R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (Spec.fullyFaithful.preimage (CategoryTheory.CategoryStruct.comp X.isoSpec.inv (X ↘ Spec R))).unop

instance AlgebraicGeometry.Scheme.instIsOverInvIsoSpecSpec_toric {R : CommRingCat} {X : Scheme} [X.Over (Spec R)] [IsAffine X] : Hom.IsOver X.isoSpec.inv (Spec R)

noncomputable instance AlgebraicGeometry.Scheme.instBialgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfMonObjOverSpecAsOverOfIsAffine_toric {R : CommRingCat} {M : Scheme} [M.Over (Spec R)] [CategoryTheory.MonObj (M.asOver (Spec R))] [IsAffine M] : Bialgebra ↑R ↑(M.presheaf.obj (Opposite.op ⊤))

The global sections of an affine monoid scheme over Spec R are a R-bialgebra.

Equations

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

noncomputable instance AlgebraicGeometry.Scheme.instHopfAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfGrpObjOverSpecAsOverOfIsAffine_toric {R : CommRingCat} {G : Scheme} [G.Over (Spec R)] [CategoryTheory.GrpObj (G.asOver (Spec R))] [IsAffine G] : HopfAlgebra ↑R ↑(G.presheaf.obj (Opposite.op ⊤))

The global sections of an affine group scheme over Spec R are a R-Hopf algebra.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.pullbackSpecIso' (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.Limits.pullback (Spec { carrier := S, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := T, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≅ Spec { carrier := TensorProduct R S T, commRing := Algebra.TensorProduct.instCommRing }

The isomorphism between the fiber product of two schemes Spec S and Spec T over a scheme Spec R and the Spec of the tensor product S ⊗[R] T.

Equations

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

theorem AlgebraicGeometry.Scheme.pullbackSpecIso'_symmetry {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : (CategoryTheory.Limits.pullbackSymmetry (Spec { carrier := T, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := S, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≪≫ pullbackSpecIso' R S T).hom = CategoryTheory.CategoryStruct.comp (pullbackSpecIso' R T S).hom (Spec.map (CommRingCat.ofHom ↑(Algebra.TensorProduct.comm R S T)))

instance AlgebraicGeometry.Scheme.instIsOverHomTransPullbackSymmetryOverSpecOfInferInstanceOverClassPullbackSpecIso' {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : Hom.IsOver (CategoryTheory.Limits.pullbackSymmetry (Spec { carrier := T, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := S, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≪≫ pullbackSpecIso' R S T).hom (Spec { carrier := S, commRing := inst✝² })

theorem AlgebraicGeometry.Scheme.μ_pullback_left_fst (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback (Spec.map (CommRingCat.ofHom (algebraMap R S)))) (CategoryTheory.Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R T)))) (CategoryTheory.Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R T))))).left (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R T)))) (CategoryTheory.Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R T))))).hom (Spec.map (CommRingCat.ofHom (algebraMap R S)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec { carrier := T, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := S, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≪≫ pullbackSpecIso' R S T).hom (Spec { carrier := S, commRing := inst✝² })) (Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec { carrier := T, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := S, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≪≫ pullbackSpecIso' R S T).hom (Spec { carrier := S, commRing := inst✝² }))).left (CategoryTheory.CategoryStruct.comp (pullbackSpecIso S (TensorProduct R S T) (TensorProduct R S T)).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.mapRingHom (algebraMap R S) Algebra.TensorProduct.includeRight.toRingHom Algebra.TensorProduct.includeRight.toRingHom ⋯ ⋯))) (pullbackSpecIso R T T).inv))

instance AlgebraicGeometry.Scheme.instIsMonHomOverSpecOfAsOverHomTransPullbackSymmetryOverInferInstanceOverClassPullbackSpecIso' {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Bialgebra R T] : CategoryTheory.IsMonHom (Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec { carrier := T, commRing := inst✝ } ↘ Spec { carrier := R, commRing := inst✝¹ }) (Spec { carrier := S, commRing := inst✝² } ↘ Spec { carrier := R, commRing := inst✝¹ }) ≪≫ pullbackSpecIso' R S T).hom (Spec { carrier := S, commRing := inst✝² }))

Right edge: The essential image of Spec on Hopf algebras

In this section we show that the essential image of R-Hopf algebras under Spec is precisely affine group schemes over Spec R.

@[simp]

theorem essImage_algSpec {R : CommRingCat} {G : CategoryTheory.Over (AlgebraicGeometry.Spec R)} : (algSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.left

The essential image of R-algebras under Spec is precisely affine schemes over Spec R.

@[simp]

theorem essImage_bialgSpec {R : CommRingCat} {G : CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R))} : (bialgSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left

The essential image of R-bialgebras under Spec is precisely affine monoid schemes over Spec R.

@[simp]

theorem essImage_hopfSpec {R : CommRingCat} {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec R))} : (hopfSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left

The essential image of R-Hopf algebras under Spec is precisely affine group schemes over Spec R.