Commutative Hopf algebras and their functor of points

This file packages the contravariant functor that sends a commutative coordinate Hopf algebra H over a commutative ring R to its group-valued functor of points A ↦ Hom_R(H, A).

The category of commutative Hopf algebras is Mathlib's bundled CommHopfAlgCat; this file adds the functor-of-points stack on top of it.

This is the categorical form of the first concrete target in the Tau Ceti reductive-groups roadmap, Layer 0, "R-points as a group": for a commutative Hopf algebra representing an affine group scheme, the functor of points is group-valued by convolution, and a morphism of coordinate Hopf algebras acts on points by pre-composition.

Main declarations

• CommHopfAlgCat.mapPointsFunctor: a coordinate morphism H ⟶ K induces a natural transformation from the points functor of K to the points functor of H.
• CommHopfAlgCat.pointsFunctor: the contravariant functor (CommHopfAlgCat R)ᵒᵖ ⥤ CommAlgCat R ⥤ GrpCat.

References

The bundled category CommHopfAlgCat, its forgetful functor to CommBialgCat, and the equivalence CommHopfAlgCat.commHopfAlgCatEquivCogrpCommAlgCat with cogroup objects in commutative algebras are Mathlib's Mathlib.Algebra.Category.CommHopfAlgCat. The points functoriality uses Mathlib's convolution monoid and bialgebra morphism API, in particular AlgHom.convMul_comp_bialgHom_distrib from Mathlib.RingTheory.Bialgebra.Convolution, through the Tau Ceti wrapper AlgHom.mapDomain.

noncomputable def TauCeti.CommHopfAlgCat.mapPointsFunctor {R : Type u} [CommRing R] {H K : _root_.CommHopfAlgCat R} (φ : H ⟶ K) : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

A morphism of coordinate commutative Hopf algebras induces a natural transformation between their group-valued points functors, contravariantly in the coordinate algebra.

At a commutative R-algebra A, this sends an A-valued point f : K →ₐ[R] A to f ∘ φ : H →ₐ[R] A.

Equations

• TauCeti.CommHopfAlgCat.mapPointsFunctor φ = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.AlgHom.mapDomain (CommHopfAlgCat.Hom.hom φ)), naturality := ⋯ }

@[simp]

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_app_apply {R : Type u} [CommRing R] {H K : _root_.CommHopfAlgCat R} (φ : H ⟶ K) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app A)) f = WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom φ))

On points, mapPointsFunctor φ is pre-composition with φ.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_app_apply_apply {R : Type u} [CommRing R] {H K : _root_.CommHopfAlgCat R} (φ : H ⟶ K) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) (h : ↑H) : ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app A)) f).ofConv h = f.ofConv ((CommHopfAlgCat.Hom.hom φ) h)

Pointwise form of mapPointsFunctor_app_apply.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_naturality_apply {R : Type u} [CommRing R] {H K : _root_.CommHopfAlgCat R} (φ : H ⟶ K) {A B : CommAlgCat R} (χ : A ⟶ B) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app A)) f) = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app B)) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) f)

Naturality of the point map induced by a coordinate morphism, applied to a point.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_app_injective_of_surjective {R : Type u} [CommRing R] {H K : _root_.CommHopfAlgCat R} (φ : H ⟶ K) (hφ : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom φ)) (A : CommAlgCat R) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app A))

Pre-composition with a surjective coordinate morphism is injective on points.

@[simp]

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_id {R : Type u} [CommRing R] (H : _root_.CommHopfAlgCat R) : mapPointsFunctor (CategoryTheory.CategoryStruct.id H) = CategoryTheory.CategoryStruct.id HopfAlgebra.pointsFunctor

mapPointsFunctor sends the identity coordinate morphism to the identity natural transformation.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_comp {R : Type u} [CommRing R] {H K L : _root_.CommHopfAlgCat R} (φ : H ⟶ K) (ψ : K ⟶ L) : mapPointsFunctor (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (mapPointsFunctor ψ) (mapPointsFunctor φ)

mapPointsFunctor sends coordinate-algebra composition to reverse composition of natural transformations.

noncomputable def TauCeti.CommHopfAlgCat.pointsFunctor {R : Type u} [CommRing R] : CategoryTheory.Functor (_root_.CommHopfAlgCat R)ᵒᵖ (CategoryTheory.Functor (CommAlgCat R) GrpCat)

The contravariant functor assigning to a commutative Hopf algebra its group-valued functor of points.

A coordinate Hopf algebra H is sent to the functor A ↦ WithConv (H →ₐ[R] A). A morphism φ : H ⟶ K is sent contravariantly to the natural transformation that pre-composes K-points by φ.

Equations

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

theorem TauCeti.CommHopfAlgCat.pointsFunctor_obj {R : Type u} [CommRing R] (H : (_root_.CommHopfAlgCat R)ᵒᵖ) : pointsFunctor.obj H = HopfAlgebra.pointsFunctor

The object part of pointsFunctor is the points functor of the underlying commutative Hopf algebra.

theorem TauCeti.CommHopfAlgCat.pointsFunctor_map {R : Type u} [CommRing R] {H K : (_root_.CommHopfAlgCat R)ᵒᵖ} (φ : H ⟶ K) : pointsFunctor.map φ = mapPointsFunctor φ.unop

The morphism part of pointsFunctor is pre-composition in the coordinate commutative Hopf algebra.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsFunctor_map_app_apply_apply {R : Type u} [CommRing R] {H K : (_root_.CommHopfAlgCat R)ᵒᵖ} (φ : H ⟶ K) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) (h : ↑(Opposite.unop K)) : ((CategoryTheory.ConcreteCategory.hom ((pointsFunctor.map φ).app A)) f).ofConv h = f.ofConv ((CommHopfAlgCat.Hom.hom φ.unop) h)

Pointwise form of the morphism part of pointsFunctor.

@[reducible, inline, deprecated CommHopfAlgCat (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat (R : Type u') [CommRing R] : Type (max (v' + 1) u')

Deprecated: the Tau Ceti-local category alias forwards to Mathlib's bundled CommHopfAlgCat.

Equations

• TauCeti.CommHopfAlgCat R = CommHopfAlgCat R

@[reducible, inline, deprecated "Provided by Mathlib's bundled CommHopfAlgCat" (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.commRing {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CommRing ↑H

Deprecated. The underlying ring of an object of CommHopfAlgCat R is commutative; this is now provided directly by Mathlib's bundled CommHopfAlgCat.

Equations

• H.commRing = inferInstance

@[reducible, inline, deprecated "Provided by Mathlib's bundled CommHopfAlgCat" (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.hopfAlgebra {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : HopfAlgebra R ↑H

Deprecated. The underlying type of an object of CommHopfAlgCat R is a Hopf algebra; this is now provided directly by Mathlib's bundled CommHopfAlgCat.

Equations

• H.hopfAlgebra = inferInstance

@[reducible, inline, deprecated CommHopfAlgCat.Hom.hom (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.toBialgHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (φ : H ⟶ K) : ↑H →ₐc[R] ↑K

Deprecated: use φ.hom. Turn a morphism in CommHopfAlgCat back into a bialgebra morphism; this is Mathlib's CommHopfAlgCat.Hom.hom.

Equations

• TauCeti.CommHopfAlgCat.toBialgHom φ = CommHopfAlgCat.Hom.hom φ

@[reducible, inline, deprecated CommHopfAlgCat.of (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.of (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CommHopfAlgCat R

Deprecated: use CommHopfAlgCat.of. Build a bundled commutative Hopf algebra from the usual unbundled typeclasses.

Equations

• TauCeti.CommHopfAlgCat.of R H = { X := H, commRing := inst✝¹, hopfAlgebra := inst✝ }

@[reducible, inline, deprecated CommHopfAlgCat.ofHom (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.ofHom {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (φ : H →ₐc[R] K) : of R H ⟶ of R K

Deprecated: use CommHopfAlgCat.ofHom. Typecheck a bialgebra morphism as a morphism in CommHopfAlgCat.

Equations

• TauCeti.CommHopfAlgCat.ofHom φ = CommHopfAlgCat.ofHom φ

@[deprecated CommHopfAlgCat.hom_id (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.toBialgHom_id {R : Type u} [CommRing R] {H : CommHopfAlgCat R} : toBialgHom (CategoryTheory.CategoryStruct.id H) = BialgHom.id R ↑H

Deprecated: toBialgHom (𝟙 H) = BialgHom.id R H; use CommHopfAlgCat.hom_id.

@[deprecated CommHopfAlgCat.hom_comp (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.toBialgHom_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (φ : H ⟶ K) (ψ : K ⟶ L) : toBialgHom (CategoryTheory.CategoryStruct.comp φ ψ) = (toBialgHom ψ).comp (toBialgHom φ)

Deprecated: toBialgHom (φ ≫ ψ) = (toBialgHom ψ).comp (toBialgHom φ); use CommHopfAlgCat.hom_comp.

@[deprecated CommHopfAlgCat.ofHom_hom (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.ofHom_toBialgHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (φ : H ⟶ K) : _root_.CommHopfAlgCat.ofHom (toBialgHom φ) = φ

Deprecated: ofHom (toBialgHom φ) = φ; use CommHopfAlgCat.ofHom_hom.

@[deprecated CommHopfAlgCat.hom_ofHom (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.toBialgHom_ofHom {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (φ : H →ₐc[R] K) : toBialgHom (_root_.CommHopfAlgCat.ofHom φ) = φ

Deprecated: toBialgHom (ofHom φ) = φ; use CommHopfAlgCat.hom_ofHom.

@[deprecated CommHopfAlgCat.hom_ext (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.hom_ext {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {φ ψ : H ⟶ K} (h : CommHopfAlgCat.Hom.hom φ = CommHopfAlgCat.Hom.hom ψ) : φ = ψ

Deprecated: use CommHopfAlgCat.hom_ext. Two morphisms of commutative Hopf algebras are equal when their underlying bialgebra morphisms are equal.

@[reducible, inline, deprecated CommHopfAlgCat.hasForgetToCommBialgCat (since := "2026-06-19")]

abbrev TauCeti.CommHopfAlgCat.hasForgetToCommBialgCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CommHopfAlgCat R) (CommBialgCat R)

Deprecated: use CommHopfAlgCat.hasForgetToCommBialgCat. The forgetful functor from commutative Hopf algebras to commutative bialgebras.

Equations

• TauCeti.CommHopfAlgCat.hasForgetToCommBialgCat = CommHopfAlgCat.hasForgetToCommBialgCat

@[deprecated CommHopfAlgCat.forget₂_commBialgCat_obj (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.forget₂_commBialgCat_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).obj H = CommBialgCat.of R ↑H

Deprecated: use CommHopfAlgCat.forget₂_commBialgCat_obj.

@[deprecated CommHopfAlgCat.forget₂_commBialgCat_map (since := "2026-06-19")]

theorem TauCeti.CommHopfAlgCat.forget₂_commBialgCat_map {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (φ : H ⟶ K) : (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).map φ = CommBialgCat.ofHom (CommHopfAlgCat.Hom.hom φ)

Deprecated: use CommHopfAlgCat.forget₂_commBialgCat_map.