Commutative Hopf algebras and their functor of points

This file packages the group object represented by a commutative coordinate Hopf algebra and the contravariant functor that sends it 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.

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.mapPointsFunctor_comp_app_apply: pointwise contravariance under composition of coordinate morphisms.
• CommHopfAlgCat.pointsFunctor: the contravariant functor (CommHopfAlgCat R)ᵒᵖ ⥤ CommAlgCat R ⥤ GrpCat.
• CommHopfAlgCat.grpObj: the underlying object of the represented group object.
• CommHopfAlgCat.grpObjMap: the contravariant morphism of represented group objects induced by a coordinate Hopf-algebra morphism.
• CommHopfAlgCat.whiskerLeft_grpObjMap_unop_hom: the coordinate description of left whiskering a represented group-object map.
• CommHopfAlgCat.grpObjMap_injective: represented group-object maps determine their coordinate Hopf-algebra morphisms.

See also

• Mathlib.Algebra.Category.CommHopfAlgCat: the bundled category CommHopfAlgCat, its forgetful functor to CommBialgCat, and the equivalence commHopfAlgCatEquivCogrpCommAlgCat.
• Mathlib.RingTheory.Bialgebra.Convolution: convolution monoid and bialgebra morphism API, in particular AlgHom.convMul_comp_bialgHom_distrib.
• TauCeti.Algebra.AlgebraicGroup.Hopf.Map: the AlgHom.mapDomain wrapper.

@[reducible, inline]

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

The underlying object op (CommAlgCat.of R H) of the group object represented by the commutative Hopf algebra H, carrying the induced GrpObj structure.

Equations

• TauCeti.CommHopfAlgCat.grpObj H = Opposite.op ↧↑H

noncomputable def TauCeti.CommHopfAlgCat.grpObjMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : grpObj K ⟶ grpObj H

The morphism of underlying group objects represented contravariantly by a morphism of commutative Hopf algebras.

Equations

• TauCeti.CommHopfAlgCat.grpObjMap f = (CommAlgCat.ofHom ↑(CommHopfAlgCat.Hom.hom f)).op

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjMap_unop {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : (grpObjMap f).unop = CommAlgCat.ofHom ↑(CommHopfAlgCat.Hom.hom f)

Unopping grpObjMap f gives the underlying commutative-algebra morphism of f.

theorem TauCeti.CommHopfAlgCat.grpObjMap_unop_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : CommAlgCat.Hom.hom (grpObjMap f).unop = ↑(CommHopfAlgCat.Hom.hom f)

The underlying algebra homomorphism obtained by unopping grpObjMap f is the underlying algebra homomorphism of f.

theorem TauCeti.CommHopfAlgCat.whiskerLeft_grpObjMap_unop_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (grpObj H) (grpObjMap f)).unop = Algebra.TensorProduct.map (AlgHom.id R ↑H) ↑(CommHopfAlgCat.Hom.hom f)

Unopping the left whiskering of a represented group-object map gives the tensor product of the identity with its underlying coordinate algebra map.

theorem TauCeti.CommHopfAlgCat.grpObjMap_injective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} : Function.Injective grpObjMap

Represented group-object maps determine their coordinate Hopf-algebra morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjMap_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : grpObjMap (CategoryTheory.CategoryStruct.id H) = CategoryTheory.CategoryStruct.id (grpObj H)

The identity coordinate morphism represents the identity group-object morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjMap_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) : grpObjMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (grpObjMap g) (grpObjMap f)

Composition of coordinate morphisms is represented contravariantly.

instance TauCeti.CommHopfAlgCat.grpObjMap_isMonHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : CategoryTheory.IsMonHom (grpObjMap f)

A morphism represented by a commutative Hopf-algebra morphism preserves the group-object multiplication.

noncomputable def TauCeti.CommHopfAlgCat.mapPointsFunctor {R : Type u} [CommRing R] {H K : 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 : 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 : 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 : 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 : 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 : 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 : 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.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_comp_app_apply {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (φ : H ⟶ K) (ψ : K ⟶ L) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor (CategoryTheory.CategoryStruct.comp φ ψ)).app A)) f = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor φ).app A)) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor ψ).app A)) f)

Pointwise form of contravariance of mapPointsFunctor under composition.

noncomputable def TauCeti.CommHopfAlgCat.pointsFunctor {R : Type u} [CommRing R] : CategoryTheory.Functor (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 : (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 : (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 : (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.