Scheme-valued points of affine Hopf-algebra spectra

For a commutative ring R and a same-universe commutative bialgebra H, this file identifies the convolution monoid of H-points with morphisms over Spec R into Spec H. It treats both affine test schemes Spec A and arbitrary schemes T, whose points are valued in the relative global sections of T through the relative Γ-Spec adjunction.

The monoid law on the scheme side is the pointwise law induced by the monoid object represented by H; the source Spec A need not itself be a monoid object. No cocommutativity assumption is made, so the resulting monoid of points need not be commutative. The target (Spec H).asOver (Spec R) below is definitionally the underlying object of (AlgebraicGeometry.bialgSpec R).obj (Opposite.op (CommBialgCat.of R H)).

The affine equivalence and its multiplicativity are Mathlib's AlgebraicGeometry.Spec.mapMulEquiv. The comparison for arbitrary test schemes upgrades Mathlib's AlgebraicGeometry.algΓAlgSpecAdjunction to a multiplicative equivalence. This file proves this comparison at bialgebra/monoid generality. It additionally records the Hopf-algebra case: transport across named Grp-presentations and the points-presheaf isomorphism for CommHopfAlgCat, together with covariance in the value algebra and contravariance in the coordinate algebra.

Main declarations

• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv: maps from an arbitrary relative scheme to an affine bialgebra spectrum are convolution points valued in its relative global sections.
• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_apply: the forward comparison applies relative global sections and then the adjunction counit.
• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_symm_apply: the inverse comparison is the adjunction unit followed by the spectrum map of the convolution point.
• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_precomp: the comparison is natural in the test scheme.
• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_mapDomain: the comparison is contravariantly natural in the coordinate bialgebra.
• TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation: Mathlib's spectrum-points equivalence with its target transported across a named presentation.
• TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation_apply_left: the underlying spectrum map of the transported equivalence.
• TauCeti.CommHopfAlgCat.mapMulEquiv_mapValue: a value-algebra map becomes precomposition by the corresponding spectrum morphism.
• TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation_mapValue: the same covariance after transport across a named presentation.
• TauCeti.CommHopfAlgCat.mapMulEquiv_mapDomain: a coordinate bialgebra morphism becomes postcomposition by the induced relative spectrum morphism Spec K ⟶ Spec H.
• TauCeti.CommHopfAlgCat.pointMulEquivOfPresentation_mapDomain: contravariance for arbitrary named point equivalences characterized by their underlying spectrum maps.
• TauCeti.CommHopfAlgCat.pointsPresheafIsoSchemePointsPresheaf: the natural comparison between convolution points and relative-spectrum points.

theorem TauCeti.CommHopfAlgCat.mapMulEquiv_left {R : Type u} [CommRing R] {S T : Type u} [CommRing S] [CommRing T] [Bialgebra R S] [Algebra R T] (f : WithConv (S →ₐ[R] T)) : CategoryTheory.Over.Hom.left (AlgebraicGeometry.Spec.mapMulEquiv f) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)

The scheme morphism underlying the spectrum-points equivalence is induced by the underlying ring homomorphism of the algebra point.

theorem TauCeti.CommHopfAlgCat.mapMulEquiv_mapDomain {R : Type u} [CommRing R] {H K : Type u} [CommRing H] [CommRing K] [Bialgebra R H] [Bialgebra R K] (A : CommAlgCat R) (f : H →ₐc[R] K) (p : WithConv (K →ₐ[R] ↑A)) : AlgebraicGeometry.Spec.mapMulEquiv ((AlgHom.mapDomain f) p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.mapMulEquiv p) (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑f).toRingHom)) (AlgebraicGeometry.Spec ↧R))

Mathlib's spectrum-points equivalence is contravariantly natural in the coordinate bialgebra. Precomposing a K-point by f : H →ₐc[R] K corresponds on spectra to postcomposing by the induced morphism Spec K ⟶ Spec H.

Points of affine spectra on arbitrary test schemes

noncomputable def TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv {R : Type u} [CommRing R] (H : Type u) [CommRing H] [Bialgebra R H] (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)) : (T ⟶ (AlgebraicGeometry.Spec ↧H).asOver (AlgebraicGeometry.Spec ↧R)) ≃* WithConv (H →ₐ[R] ↑(Opposite.unop ((AlgebraicGeometry.algΓ ↧R).obj T)))

Maps from an arbitrary scheme T over Spec R to the affine monoid scheme represented by H are the convolution monoid of H-points valued in the relative global sections of T.

Unlike AlgebraicGeometry.Spec.mapMulEquiv, the test scheme here need not be affine. The equivalence is the relative Γ-Spec adjunction, with its target given the convolution product.

Equations

• TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv H T = { toEquiv := TauCeti.CommHopfAlgCat.schemePointsAlgΓEquiv✝ H T, map_mul' := ⋯ }

@[simp]

theorem TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_apply {R : Type u} [CommRing R] (H : Type u) [CommRing H] [Bialgebra R H] (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)) (g : T ⟶ (AlgebraicGeometry.Spec ↧H).asOver (AlgebraicGeometry.Spec ↧R)) : (schemePointsAlgΓMulEquiv H T) g = WithConv.toConv (CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.algΓ ↧R).map g) ((AlgebraicGeometry.algΓAlgSpecAdjunction ↧R).counit.app (Opposite.op ↧H))).unop)

The forward relative Γ-Spec comparison applies relative global sections to the scheme point and composes with the adjunction counit, then regards the resulting algebra morphism as a convolution point.

@[simp]

theorem TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_symm_apply {R : Type u} [CommRing R] (H : Type u) [CommRing H] [Bialgebra R H] (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)) (p : WithConv (H →ₐ[R] ↑(Opposite.unop ((AlgebraicGeometry.algΓ ↧R).obj T)))) : (schemePointsAlgΓMulEquiv H T).symm p = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.algΓAlgSpecAdjunction ↧R).unit.app T) (AlgebraicGeometry.Spec.mapMulEquiv p)

The inverse relative Γ-Spec comparison is the adjunction unit followed by the affine spectrum point represented by p.

theorem TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_precomp {R : Type u} [CommRing R] (H : Type u) [CommRing H] [Bialgebra R H] {S T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)} (φ : S ⟶ T) (g : T ⟶ (AlgebraicGeometry.Spec ↧H).asOver (AlgebraicGeometry.Spec ↧R)) : (schemePointsAlgΓMulEquiv H S) (CategoryTheory.CategoryStruct.comp φ g) = (AlgHom.mapValue (CommAlgCat.Hom.hom ((AlgebraicGeometry.algΓ ↧R).map φ).unop)) ((schemePointsAlgΓMulEquiv H T) g)

The global-sections comparison is natural in the test scheme. Precomposing a T-valued point by φ : S ⟶ T postcomposes its algebra point with the induced map Γ(T) ⟶ Γ(S).

theorem TauCeti.CommHopfAlgCat.schemePointsAlgΓMulEquiv_mapDomain {R : Type u} [CommRing R] {H K : Type u} [CommRing H] [CommRing K] [Bialgebra R H] [Bialgebra R K] (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)) (f : H →ₐc[R] K) (g : T ⟶ (AlgebraicGeometry.Spec ↧K).asOver (AlgebraicGeometry.Spec ↧R)) : (schemePointsAlgΓMulEquiv H T) (CategoryTheory.CategoryStruct.comp g (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑f).toRingHom)) (AlgebraicGeometry.Spec ↧R))) = (AlgHom.mapDomain f) ((schemePointsAlgΓMulEquiv K T) g)

The global-sections comparison is contravariantly natural in the coordinate bialgebra. Postcomposing a scheme-valued point with Spec f is precomposition of its algebra point by f.

Points on affine test schemes

noncomputable def TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : Type u) [CommRing A] [Algebra R A] {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (hG : G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)) : WithConv (↑H →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ G.X)

Mathlib's spectrum-points equivalence with its target transported to an equal named scheme over Spec R.

The equality records the complete presentation as a group object over Spec R, so both the structural morphism and the pointwise group law are preserved by the transport.

Equations

• TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation H A hG = ⋯ ▸ AlgebraicGeometry.Spec.mapMulEquiv

theorem TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation_apply_left {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : Type u) [CommRing A] [Algebra R A] {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (hG : G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)) (hX : G.X.left = AlgebraicGeometry.Spec ↧↑H) (f : WithConv (↑H →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((mapMulEquivOfPresentation H A hG) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying scheme map of the spectrum point transported across a named presentation.

The second equality names the presentation of the wrapped group's underlying scheme as Spec H; it determines the eqToHom appearing in the formula.

theorem TauCeti.CommHopfAlgCat.mapMulEquiv_mapValue {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {A B : CommAlgCat R} (φ : A ⟶ B) (p : ↑(HopfAlgebra.points A)) : AlgebraicGeometry.Spec.mapMulEquiv ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints φ)) p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (CommAlgCat.Hom.hom φ).toRingHom)) (AlgebraicGeometry.Spec ↧R)) (AlgebraicGeometry.Spec.mapMulEquiv p)

Mathlib's spectrum-points equivalence is natural in the value algebra. Postcomposing an A-valued algebra point by φ : A ⟶ B corresponds on spectra to precomposing by Spec B ⟶ Spec A.

theorem TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation_mapValue {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (hG : G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ G.X) : (mapMulEquivOfPresentation H B hG).symm (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints (CommAlgCat.ofHom φ))) ((mapMulEquivOfPresentation H A hG).symm p)

Naturality in the value algebra for spectrum points whose target is transported across a named presentation.

theorem TauCeti.CommHopfAlgCat.pointMulEquivOfPresentation_mapDomain {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (A : Type u) [CommRing A] [Algebra R A] {G H' : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (hG : G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)) (hH' : H' = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)) (eG : WithConv (↑H →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ G.X)) (eH' : WithConv (↑K →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ H'.X)) (eG_apply_left : ∀ (f : WithConv (↑H →ₐ[R] A)), CategoryTheory.Over.Hom.left (eG f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)) (eH'_apply_left : ∀ (f : WithConv (↑K →ₐ[R] A)), CategoryTheory.Over.Hom.left (eH' f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)) (φ : H ⟶ K) (p : ↑(HopfAlgebra.points ↧A)) : CategoryTheory.CategoryStruct.comp (eH' p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hH') (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map φ.op) (CategoryTheory.eqToHom ⋯))).hom.hom = eG ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app ↧A)) p)

Contravariant naturality in the coordinate Hopf algebra for named point equivalences.

The two equivalences may be public wrappers around mapMulEquivOfPresentation; it is enough to characterize their underlying scheme maps. This lets named affine group schemes reuse the presentation compatibility without unfolding their definitions.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.schemePointsPresheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ (Type u)

Scheme-valued affine-group points, restricted along relative Spec and regarded as a type-valued presheaf on opposite commutative algebras.

Equations

• TauCeti.CommHopfAlgCat.schemePointsPresheaf H = (AlgebraicGeometry.algSpec ↧R).op.comp (CategoryTheory.yoneda.obj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X)

theorem TauCeti.CommHopfAlgCat.schemePointsPresheaf_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : (CommAlgCat R)ᵒᵖᵒᵖ) : (schemePointsPresheaf H).obj A = ((AlgebraicGeometry.Spec ↧↑(Opposite.unop (Opposite.unop A))).asOver (AlgebraicGeometry.Spec ↧R) ⟶ ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X)

The scheme-points presheaf at A is the set of morphisms over Spec R from Spec A to Spec H.

noncomputable def TauCeti.CommHopfAlgCat.pointsPresheafIsoSchemePointsPresheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : HopfAlgebra.pointsPresheaf H ≅ schemePointsPresheaf H

Convolution points agree naturally with scheme-valued points. This is Mathlib's Spec.mapMulEquiv, assembled over all value algebras.

Equations

• TauCeti.CommHopfAlgCat.pointsPresheafIsoSchemePointsPresheaf H = CategoryTheory.NatIso.ofComponents (fun (A : (CommAlgCat R)ᵒᵖᵒᵖ) => AlgebraicGeometry.Spec.mapMulEquiv.toIso) ⋯

theorem TauCeti.CommHopfAlgCat.pointsPresheafIsoSchemePointsPresheaf_hom_app_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : (CommAlgCat R)ᵒᵖᵒᵖ) (p : WithConv (↑H →ₐ[R] ↑(Opposite.unop (Opposite.unop A)))) : (CategoryTheory.ConcreteCategory.hom ((pointsPresheafIsoSchemePointsPresheaf H).hom.app A)) p = AlgebraicGeometry.Spec.mapMulEquiv p

The comparison from convolution points to scheme-valued points is Mathlib's spectrum-points equivalence at every value algebra.

theorem TauCeti.CommHopfAlgCat.pointsPresheafIsoSchemePointsPresheaf_inv_app_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : (CommAlgCat R)ᵒᵖᵒᵖ) (p : (schemePointsPresheaf H).obj A) : (CategoryTheory.ConcreteCategory.hom ((pointsPresheafIsoSchemePointsPresheaf H).inv.app A)) p = AlgebraicGeometry.Spec.mapMulEquiv.symm p

The inverse comparison recovers the convolution point represented by a relative spectrum morphism.