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 affine group schemes correspond to Hopf algebras. 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 (e.g. 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 Mathlib.Algebra.Category.CommHopfAlgCat.

Top edge: Spec as a functor on Hopf algebras

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

noncomputable def AlgebraicGeometry.algΓ (R : CommRingCat) : CategoryTheory.Functor (CategoryTheory.Over (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 AlgebraicGeometry.preservesLimitsOfSize_algSpec {R : CommRingCat} : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (algSpec R)

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

@[simp]

theorem AlgebraicGeometry.algSpec_obj_hom {R : CommRingCat} (X : (CommAlgCat ↑R)ᵒᵖ) : ((algSpec R).obj X).hom = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑(Opposite.unop X)))

@[simp]

theorem AlgebraicGeometry.algSpec_map_left {R : CommRingCat} {X Y : (CommAlgCat ↑R)ᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Over.Hom.left ((algSpec R).map f) = Spec.map (CategoryTheory.Under.Hom.right ((commAlgCatEquivUnder R).functor.map f.unop))

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

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

The monoidal data is copied from Functor.Braided.ofChosenFiniteProducts so that ε, η are definitionally 𝟙 (Spec R) and μ, δ are definitionally pullbackSpecIso.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Spec is full on R-algebras.

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

Spec is faithful on R-algebras.

noncomputable def AlgebraicGeometry.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 AlgebraicGeometry.bialgSpec (R : CommRingCat) : CategoryTheory.Functor (CommBialgCat ↑R)ᵒᵖ (CategoryTheory.Mon (CategoryTheory.Over (Spec R)))

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

Equations

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

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

Spec is full on R-bialgebras.

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

Spec is faithful on R-bialgebras.

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

Spec is full on R-Hopf algebras.

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

Spec is faithful on R-Hopf algebras.

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem AlgebraicGeometry.one_def {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (algSpec R)) ((algSpec R).map CategoryTheory.MonObj.one)

theorem AlgebraicGeometry.one_spec_asOver_spec {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.one_spec_asOver_spec_left {R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))

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

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

@[instance_reducible]

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

Equations

• AlgebraicGeometry.instGrpObjSpecAsOverSpec = { toMonObj := AlgebraicGeometry.instMonObjSpecAsOverSpec, inv := CategoryTheory.GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

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

Equations

• AlgebraicGeometry.instCommGrpObjSpecAsOverSpec = { toGrpObj := AlgebraicGeometry.instGrpObjSpecAsOverSpec, toIsCommMonObj := ⋯ }

instance AlgebraicGeometry.instIsOverMapOfHomSpecOf {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) : Scheme.Hom.IsOver (Spec.map (CommRingCat.ofHom f.toRingHom)) (Spec (CommRingCat.of R))

noncomputable def AlgebraicGeometry.Spec.mapMulEquiv {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Bialgebra R S] [Algebra R T] : WithConv (S →ₐ[R] T) ≃* ((Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶ (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R)))

Spec.map as a MulEquiv on hom-sets.

Equations

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

noncomputable def AlgebraicGeometry.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.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfOverSpecOfIsAffine {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.algebraMap_presheafObj {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.instIsOverToSpecΓSpec {R : CommRingCat} {X : Scheme} [X.Over (Spec R)] [IsAffine X] : Scheme.Hom.IsOver X.toSpecΓ (Spec R)

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

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instBialgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfMonObjOverSchemeSpecAsOverOfIsAffine {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.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instHopfAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfGrpObjOverSchemeSpecAsOverOfIsAffine {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.pullbackSpecIso' (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.Limits.pullback (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) ≅ Spec (CommRingCat.of (TensorProduct R S T))

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.

This is a version of pullbackSpecIso stated in terms of specOverSpec. TODO: Unify with pullbackSpecIso once OverClass is refactored to not bundle the morphism.

Equations

• AlgebraicGeometry.pullbackSpecIso' R S T = AlgebraicGeometry.pullbackSpecIso ↑(CommRingCat.of R) ↑(CommRingCat.of S) ↑(CommRingCat.of T)

theorem AlgebraicGeometry.pullbackSpecIso'_symmetry {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) ≪≫ 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.instIsOverHomSchemeTransPullbackSymmetryOverSpecOfInferInstanceOverClassPullbackSpecIso' {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : Scheme.Hom.IsOver (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) ≪≫ pullbackSpecIso' R S T).hom (Spec (CommRingCat.of S))

theorem AlgebraicGeometry.μ_pullback_left_fst (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (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)))))) (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.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom (Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) ≪≫ pullbackSpecIso' R S T).hom (Spec (CommRingCat.of S))) (Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) ≪≫ pullbackSpecIso' R S T).hom (Spec (CommRingCat.of S))))) (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.instIsMonHomOverSchemeSpecOfAsOverHomTransPullbackSymmetryOverInferInstanceOverClassPullbackSpecIso' {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Bialgebra R T] : CategoryTheory.IsMonHom (Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)) (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) ≪≫ pullbackSpecIso' R S T).hom (Spec (CommRingCat.of S)))

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 AlgebraicGeometry.essImage_algSpec {R : CommRingCat} {G : CategoryTheory.Over (Spec R)} : (algSpec R).essImage G ↔ IsAffine G.left

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

@[simp]

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

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

@[simp]

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

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