The functor of points of a Hopf algebra

This file packages the convolution group of algebra homomorphisms out of a Hopf algebra as a functor from commutative algebras to groups. For a Hopf algebra H over R, an object A : CommAlgCat R is sent to the convolution group on H →ₐ[R] A; a morphism φ : A ⟶ B acts by post-composition with φ.

This is the categorical form of the ReductiveGroups roadmap Layer 0 target "R-points as a group": for the affine group scheme represented by a commutative Hopf algebra H, its functor of points has values A ↦ (H →ₐ[R] A) and group law given by convolution.

Main definitions

• HopfAlgebra.points: the bundled group of A-points.
• HopfAlgebra.mapPoints: the group homomorphism induced by post-composition in the value algebra.
• HopfAlgebra.pointsFunctor: the functor CommAlgCat R ⥤ GrpCat.

References

This packages the "R-points as a group via convolution" milestone of the Tau Ceti ReductiveGroups roadmap, Layer 0. It builds on Mathlib's convolution monoid for algebra homomorphisms and the convolution-group inverse already developed in TauCeti.Algebra.AlgebraicGroup.FunctorOfPoints.

@[reducible, inline]

noncomputable abbrev TauCeti.HopfAlgebra.points {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) : GrpCat

The group of A-points of the affine group object represented by a Hopf algebra H.

The underlying type is WithConv (H →ₐ[R] A): algebra homomorphisms from H to A, with the convolution group structure supplied by the antipode of H.

Equations

• TauCeti.HopfAlgebra.points A = GrpCat.of (WithConv (H →ₐ[R] ↑A))

noncomputable def TauCeti.HopfAlgebra.mapPoints {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) : points A ⟶ points B

The group homomorphism on points induced by a morphism of value algebras.

It sends an A-point f : H →ₐ[R] A to the B-point φ ∘ f.

Equations

• TauCeti.HopfAlgebra.mapPoints φ = GrpCat.ofHom (TauCeti.AlgHom.mapValue (CommAlgCat.Hom.hom φ))

@[simp]

theorem TauCeti.HopfAlgebra.mapPoints_apply {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) (f : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) f = WithConv.toConv ((CommAlgCat.Hom.hom φ).comp f.ofConv)

On points, mapPoints is post-composition with the algebra homomorphism φ.

theorem TauCeti.HopfAlgebra.mapPoints_one {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) : (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) 1 = 1

The map on points sends the identity point to the identity point.

theorem TauCeti.HopfAlgebra.mapPoints_mul {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) (f g : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) (f * g) = (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) f * (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) g

The map on points preserves multiplication of points.

theorem TauCeti.HopfAlgebra.mapPoints_inv {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) (f : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom (mapPoints φ)) f⁻¹ = ((CategoryTheory.ConcreteCategory.hom (mapPoints φ)) f)⁻¹

The map on points preserves inverses of points.

@[simp]

theorem TauCeti.HopfAlgebra.mapPoints_id {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) : mapPoints (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (points A)

mapPoints preserves identity morphisms of value algebras.

theorem TauCeti.HopfAlgebra.mapPoints_comp {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) : mapPoints (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (mapPoints φ) (mapPoints ψ)

mapPoints preserves composition of morphisms of value algebras.

noncomputable def TauCeti.HopfAlgebra.pointsFunctor {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] : CategoryTheory.Functor (CommAlgCat R) GrpCat

The functor of points of the affine group object represented by a Hopf algebra.

It maps a commutative R-algebra A to the convolution group on algebra homomorphisms H →ₐ[R] A, and maps φ : A ⟶ B to post-composition with φ.

Equations

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

theorem TauCeti.HopfAlgebra.pointsFunctor_obj {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) : pointsFunctor.obj A = GrpCat.of (WithConv (H →ₐ[R] ↑A))

The object part of pointsFunctor is the convolution group of algebra homomorphisms.

theorem TauCeti.HopfAlgebra.pointsFunctor_map {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) : pointsFunctor.map φ = mapPoints φ

The morphism part of pointsFunctor is post-composition in the value algebra.

@[simp]

theorem TauCeti.HopfAlgebra.pointsFunctor_map_apply_apply {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) (f : WithConv (H →ₐ[R] ↑A)) (h : H) : ((CategoryTheory.ConcreteCategory.hom (pointsFunctor.map φ)) f).ofConv h = (CommAlgCat.Hom.hom φ) (f.ofConv h)

The pointwise value of the image of an A-point under pointsFunctor.map φ.