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.extendPoint: extension of ground-ring-valued points to a value algebra.
• HopfAlgebra.mapPoints: the group homomorphism induced by post-composition in the value algebra.
• HopfAlgebra.pointsFunctor: the functor CommAlgCat R ⥤ GrpCat.
• HopfAlgebra.subgroupFunctor: a functor assembled from point subgroups stable under change of value algebra.

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 = ↧(WithConv (H →ₐ[R] ↑A))

noncomputable def TauCeti.HopfAlgebra.extendPoint {R : Type u} [CommRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) : ↑(points ↧R) →* ↑(points A)

Extension of ground-ring-valued points to A-valued points along the structure map of A.

Equations

• TauCeti.HopfAlgebra.extendPoint H A = TauCeti.AlgHom.mapValue (Algebra.ofId R ↑A)

theorem TauCeti.HopfAlgebra.extendPoint_apply {R : Type u} [CommRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) (g : ↑(points ↧R)) : (extendPoint H A) g = WithConv.toConv ((Algebra.ofId R ↑A).comp g.ofConv)

Extension of a point is post-composition with the value algebra's structure map.

@[simp]

theorem TauCeti.HopfAlgebra.extendPoint_ofConv {R : Type u} [CommRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) (g : ↑(points ↧R)) (h : H) : ((extendPoint H A) g).ofConv h = (algebraMap R ↑A) (g.ofConv h)

Evaluation of an extended point is obtained by applying the value algebra's structure map.

@[simp]

theorem TauCeti.HopfAlgebra.extendPoint_self {R : Type u} [CommRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] (g : ↑(points ↧R)) : (extendPoint H ↧R) g = g

Extending a ground-ring-valued point back to the ground ring leaves it unchanged.

theorem TauCeti.HopfAlgebra.mapValue_extendPoint {R : Type u} [CommRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] {A : CommAlgCat R} {B : CommAlgCat R} (f : ↑A →ₐ[R] ↑B) (g : ↑(points ↧R)) : (AlgHom.mapValue f) ((extendPoint H A) g) = (extendPoint H B) g

Post-composition of an extended point is extension to the target algebra.

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.

@[simp]

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

The categorical point map sends an extended point to its extension in the target algebra.

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_hom_ext {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {K : Type v} [Semiring K] [HopfAlgebra R K] {α β : pointsFunctor ⟶ pointsFunctor} (h : ∀ (A : CommAlgCat R) (x : ↑(points A)), (CategoryTheory.ConcreteCategory.hom (α.app A)) x = (CategoryTheory.ConcreteCategory.hom (β.app A)) x) : α = β

Natural transformations between points functors agree if they agree on every point.

theorem TauCeti.HopfAlgebra.pointsFunctor_hom_ext_iff {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {K : Type v} [Semiring K] [HopfAlgebra R K] {α β : pointsFunctor ⟶ pointsFunctor} : α = β ↔ ∀ (A : CommAlgCat R) (x : ↑(points A)), (CategoryTheory.ConcreteCategory.hom (α.app A)) x = (CategoryTheory.ConcreteCategory.hom (β.app A)) x

theorem TauCeti.HopfAlgebra.pointsFunctor_obj {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (A : CommAlgCat R) : pointsFunctor.obj A = ↧(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.

theorem TauCeti.HopfAlgebra.pointsFunctor_map_eqToHom {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (pointsFunctor.map φ) = CategoryTheory.CategoryStruct.comp (mapPoints φ) (CategoryTheory.eqToHom ⋯)

The map of pointsFunctor, transported along its concrete object presentations, is the corresponding map on points.

@[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 φ.

noncomputable def TauCeti.HopfAlgebra.subgroupFunctor {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (S : (A : CommAlgCat R) → Subgroup ↑(points A)) (map : {A B : CommAlgCat R} → (A ⟶ B) → ↥(S A) →* ↥(S B)) (map_id : ∀ (A : CommAlgCat R) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.id A)) g = g) (map_comp : ∀ {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.comp φ ψ)) g = (map ψ) ((map φ) g)) : CategoryTheory.Functor (CommAlgCat R) GrpCat

A family of subgroups of the functor of points, equipped with compatible maps between value algebras, as a group-valued functor.

Equations

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

@[simp]

theorem TauCeti.HopfAlgebra.subgroupFunctor_obj {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (S : (A : CommAlgCat R) → Subgroup ↑(points A)) (map : {A B : CommAlgCat R} → (A ⟶ B) → ↥(S A) →* ↥(S B)) (map_id : ∀ (A : CommAlgCat R) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.id A)) g = g) (map_comp : ∀ {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.comp φ ψ)) g = (map ψ) ((map φ) g)) (A : CommAlgCat R) : (subgroupFunctor S (fun {A B : CommAlgCat R} => map) map_id ⋯).obj A = ↧↥(S A)

The object part of a point-subgroup functor is the specified subgroup.

@[simp]

theorem TauCeti.HopfAlgebra.subgroupFunctor_map {R : Type u} [CommRing R] {H : Type v} [Semiring H] [HopfAlgebra R H] (S : (A : CommAlgCat R) → Subgroup ↑(points A)) (map : {A B : CommAlgCat R} → (A ⟶ B) → ↥(S A) →* ↥(S B)) (map_id : ∀ (A : CommAlgCat R) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.id A)) g = g) (map_comp : ∀ {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) (g : ↥(S A)), (map (CategoryTheory.CategoryStruct.comp φ ψ)) g = (map ψ) ((map φ) g)) {A B : CommAlgCat R} (φ : A ⟶ B) : (subgroupFunctor S (fun {A B : CommAlgCat R} => map) map_id ⋯).map φ = GrpCat.ofHom (map φ)

The map part of a point-subgroup functor is the specified restricted point map.