Yoneda theory for the functor of points

The underlying type-valued functor of points of a commutative Hopf algebra H is corepresented by H as a commutative algebra. Concretely, a morphism CommAlgCat.of R H ⟶ A is the same data as an A-valued point WithConv (H →ₐ[R] A).

This file packages that tautological equivalence as a Functor.CorepresentableBy, exposes the resulting coyoneda isomorphism, and proves that the contravariant CommHopfAlgCat.pointsFunctor is fully faithful. The group-valued result identifies the points functor with group-object Yoneda, after transporting commutative Hopf algebras to cogroup commutative algebras and removing a double opposite. Its essential image consists exactly of the group-valued functors whose underlying type-valued functor is corepresentable.

The corepresenting object and value algebras live in the same universe as H. Universe transport for a points functor valued in a different universe is deliberately left to the later universe-lifting bridge; shrinkYonedaGrp supplies only the group-valued hom-set shrinking part.

Main declarations

• TauCeti.HopfAlgebra.pointsHomEquiv: a morphism out of the coordinate algebra is the same data as a point, with the computation rules in both directions.
• TauCeti.HopfAlgebra.pointsCorepresentableBy: the underlying type-valued points functor is corepresented by the coordinate algebra.
• TauCeti.HopfAlgebra.coyonedaObjIsoPointsFunctorForget: the corresponding coyoneda isomorphism.
• TauCeti.HopfAlgebra.pointsFunctorForget_isCorepresentable: the discoverable corepresentability instance.
• TauCeti.HopfAlgebra.pointsGroupPresheaf and TauCeti.HopfAlgebra.pointsPresheaf: the group- and type-valued points functors as presheaves on opposite commutative algebras.
• TauCeti.CommHopfAlgCat.groupYonedaPointsFunctor: the group-object Yoneda model of the functor of points.
• TauCeti.CommHopfAlgCat.groupYonedaPointsHomEquiv: the carrier equivalence from the opaque group-Yoneda model to algebra morphisms.
• TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv: generalized points of the represented group object are its convolution points.
• TauCeti.CommHopfAlgCat.grpObj_conj_unop_hom: categorical conjugation unops to the coordinate conjugation algebra map.
• TauCeti.CommHopfAlgCat.groupYonedaPointsFunctorIso: the group-valued Yoneda model is naturally isomorphic to the existing points functor.
• TauCeti.CommHopfAlgCat.pointsFunctor_faithful and TauCeti.CommHopfAlgCat.pointsFunctor_full: points recover coordinate Hopf algebra morphisms.
• TauCeti.CommHopfAlgCat.isIso_of_isIso_mapPointsFunctor: a coordinate morphism is an isomorphism when its induced natural map on points is an isomorphism.
• TauCeti.CommHopfAlgCat.homOfPointsMap: the coordinate morphism a natural map of points functors comes from, with TauCeti.CommHopfAlgCat.mapPointsFunctor_homOfPointsMap its defining property, TauCeti.CommHopfAlgCat.homOfPointsMap_mapPointsFunctor the converse recovery law, and TauCeti.CommHopfAlgCat.homOfPointsMap_id and TauCeti.CommHopfAlgCat.homOfPointsMap_comp its functoriality. This is the form in which fullness is used downstream, where a group-scheme morphism is built from its natural action on points.
• TauCeti.CommHopfAlgCat.essImage_pointsFunctor: the essential image consists exactly of group functors with corepresentable underlying functor.

References

This is the Yoneda/corepresentability step in ReductiveGroups/README.md, Layer 0, "the functor of points and the three-way dictionary". It reuses Mathlib's Functor.CorepresentableBy, ConcreteCategory.homEquiv, and WithConv.equiv. Stating the corepresenting equivalence separately, at the type of points, follows Mathlib's CategoryTheory.Functor.RepresentableBy.homEquiv', which plays the same role for a representable functor of the form F ⋙ forget D. The group-valued result uses Mathlib's Hopf-algebra/cogroup equivalence, CategoryTheory.yonedaGrp, and its essential-image theorem.

noncomputable def TauCeti.HopfAlgebra.pointsHomEquiv {R : Type u} [CommRing R] (H : Type v) [CommRing H] [Algebra R H] (A : CommAlgCat R) : (↧H ⟶ A) ≃ WithConv (H →ₐ[R] ↑A)

The tautological equivalence between morphisms of commutative R-algebras CommAlgCat.of R H ⟶ A and A-valued points of H: both are the algebra homomorphism H →ₐ[R] A underlying the morphism.

This is the equivalence corepresenting the points functor, stated on its own rather than only as a field of pointsCorepresentableBy, in the same way as Mathlib's Functor.RepresentableBy.homEquiv'. It is what carries the computation rules: a left-hand side mentioning the value (pointsFunctor ⋙ forget GrpCat).obj A of the corepresented functor is not in simp normal form, since Functor.comp_obj rewrites that type. The codomain is spelled as WithConv (H →ₐ[R] A), the underlying type of points A, so that the two sides of the rules below have the same type; simp does not use a rule whose sides agree only definitionally. Only the commutative R-algebra structure of H is used here; the Hopf structure enters when the codomain carries its convolution group structure.

Equations

• TauCeti.HopfAlgebra.pointsHomEquiv H A = CategoryTheory.ConcreteCategory.homEquiv.trans (WithConv.equiv (CategoryTheory.ToHom (↧H) A)).symm

@[simp]

theorem TauCeti.HopfAlgebra.pointsHomEquiv_apply {R : Type u} [CommRing R] (H : Type v) [CommRing H] [Algebra R H] {A : CommAlgCat R} (f : ↧H ⟶ A) : (pointsHomEquiv H A) f = WithConv.toConv (CommAlgCat.Hom.hom f)

pointsHomEquiv regards a morphism of commutative R-algebras as an A-valued point.

@[simp]

theorem TauCeti.HopfAlgebra.pointsHomEquiv_symm_apply {R : Type u} [CommRing R] (H : Type v) [CommRing H] [Algebra R H] {A : CommAlgCat R} (p : WithConv (H →ₐ[R] ↑A)) : (pointsHomEquiv H A).symm p = CommAlgCat.ofHom p.ofConv

The inverse of pointsHomEquiv forgets the convolution wrapper and bundles the resulting algebra homomorphism as a morphism in CommAlgCat.

noncomputable def TauCeti.HopfAlgebra.pointsCorepresentableBy {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (pointsFunctor.comp (CategoryTheory.forget GrpCat)).CorepresentableBy ↧H

The underlying type-valued functor of points of a commutative Hopf algebra H is corepresented by H as a commutative R-algebra.

Equations

• TauCeti.HopfAlgebra.pointsCorepresentableBy H = { homEquiv := fun {A : CommAlgCat R} => TauCeti.HopfAlgebra.pointsHomEquiv H A, homEquiv_comp := ⋯ }

noncomputable def TauCeti.HopfAlgebra.coyonedaObjIsoPointsFunctorForget {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.coyoneda.obj (Opposite.op ↧H) ≅ pointsFunctor.comp (CategoryTheory.forget GrpCat)

The coyoneda functor corepresented by H is isomorphic to the underlying type-valued functor of points of H.

Equations

• TauCeti.HopfAlgebra.coyonedaObjIsoPointsFunctorForget H = (TauCeti.HopfAlgebra.pointsCorepresentableBy H).toIso

instance TauCeti.HopfAlgebra.pointsFunctorForget_isCorepresentable {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (pointsFunctor.comp (CategoryTheory.forget GrpCat)).IsCorepresentable

The underlying type-valued functor of points is registered as corepresentable, so the generic corepresentability API can recover a representing object and universal element.

@[reducible, inline]

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

The group-valued presheaf of convolution points of a commutative Hopf algebra.

The double-opposite equivalence presents the covariant functor on CommAlgCat R as a presheaf on the opposite category.

Equations

• TauCeti.HopfAlgebra.pointsGroupPresheaf H = (CategoryTheory.unopUnop (CommAlgCat R)).comp TauCeti.HopfAlgebra.pointsFunctor

@[reducible, inline]

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

The underlying type-valued presheaf of convolution points of a commutative Hopf algebra.

Equations

• TauCeti.HopfAlgebra.pointsPresheaf H = (TauCeti.HopfAlgebra.pointsGroupPresheaf H).comp (CategoryTheory.forget GrpCat)

theorem TauCeti.HopfAlgebra.pointsPresheaf_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : (CommAlgCat R)ᵒᵖᵒᵖ) : (pointsPresheaf H).obj A = WithConv (↑H →ₐ[R] ↑(Opposite.unop (Opposite.unop A)))

Evaluating the points presheaf at an affine R-scheme gives its convolution group of algebra-valued points, with the group structure forgotten.

theorem TauCeti.HopfAlgebra.coyonedaObjIsoPointsFunctorForget_hom_app_apply {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (A : CommAlgCat R) (f : ↧H ⟶ A) : (CategoryTheory.ConcreteCategory.hom ((coyonedaObjIsoPointsFunctorForget H).hom.app A)) f = WithConv.toConv (CommAlgCat.Hom.hom f)

The forward map of coyonedaObjIsoPointsFunctorForget regards an algebra morphism as a point.

theorem TauCeti.HopfAlgebra.coyonedaObjIsoPointsFunctorForget_inv_app_apply {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (A : CommAlgCat R) (p : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom ((coyonedaObjIsoPointsFunctorForget H).inv.app A)) p = CommAlgCat.ofHom p.ofConv

The inverse map of coyonedaObjIsoPointsFunctorForget bundles a point as a morphism in CommAlgCat.

instance TauCeti.CommHopfAlgCat.pointsFunctor_faithful {R : Type u} [CommRing R] : pointsFunctor.Faithful

The contravariant functor of points is faithful: a coordinate Hopf-algebra morphism is recovered by evaluating its map on points at the identity point of its target algebra.

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

The group-object Yoneda model of the same-universe functor of points.

The Hopf-algebra/cogroup equivalence sends an opposite commutative Hopf algebra to a group object in opposite commutative algebras. Group-valued Yoneda then produces a functor on the double opposite of CommAlgCat, and the final equivalence precomposes it with opOp to give a covariant functor on commutative algebras.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.groupYonedaPointsHomEquiv {R : Type u} [CommRing R] (H : (CommHopfAlgCat R)ᵒᵖ) (A : CommAlgCat R) : ↑((groupYonedaPointsFunctor.obj H).obj A) ≃ (↧↑(Opposite.unop H) ⟶ A)

The carrier of the group-Yoneda model at a Hopf algebra H and value algebra A is canonically the type of algebra morphisms H ⟶ A. This equivalence is the narrow carrier API for the otherwise opaque composite groupYonedaPointsFunctor.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.groupYonedaPointsHomEquiv_map {R : Type u} [CommRing R] (H : (CommHopfAlgCat R)ᵒᵖ) {A B : CommAlgCat R} (g : A ⟶ B) (f : ↑((groupYonedaPointsFunctor.obj H).obj A)) : (groupYonedaPointsHomEquiv H B) ((CategoryTheory.ConcreteCategory.hom ((groupYonedaPointsFunctor.obj H).map g)) f) = CategoryTheory.CategoryStruct.comp ((groupYonedaPointsHomEquiv H A) f) g

Under a map of value algebras, the algebra morphism underlying a group-Yoneda element is postcomposed with that map.

@[simp]

theorem TauCeti.CommHopfAlgCat.groupYonedaPointsHomEquiv_map_app {R : Type u} [CommRing R] {H K : (CommHopfAlgCat R)ᵒᵖ} (f : H ⟶ K) (A : CommAlgCat R) (p : ↑((groupYonedaPointsFunctor.obj H).obj A)) : (groupYonedaPointsHomEquiv K A) ((CategoryTheory.ConcreteCategory.hom ((groupYonedaPointsFunctor.map f).app A)) p) = CategoryTheory.CategoryStruct.comp (CommAlgCat.ofHom ↑(CommHopfAlgCat.Hom.hom f.unop)) ((groupYonedaPointsHomEquiv H A) p)

Under a map of coordinate Hopf algebras, the algebra morphism underlying a group-Yoneda element is precomposed with that map.

noncomputable def TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (X : (CommAlgCat R)ᵒᵖ) : (X ⟶ grpObj H) ≃* ↑(HopfAlgebra.points (Opposite.unop X))

Generalized points of the group object represented by H are the convolution group of algebra-valued points of H. It sends the categorical multiplication lift f g ≫ μ to the convolution product of the underlying algebra morphisms.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (X : (CommAlgCat R)ᵒᵖ) (g : X ⟶ grpObj H) : (grpObjPointsMulEquiv H X) g = WithConv.toConv (CommAlgCat.Hom.hom g.unop)

The group-object point equivalence regards a categorical point as the convolution wrapper of its underlying algebra morphism.

theorem TauCeti.CommHopfAlgCat.grpObj_conj_unop_hom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CommAlgCat.Hom.hom (CategoryTheory.GrpObj.conj (grpObj H)).unop = HopfAlgebra.conjugationAlgHom

Unopping categorical conjugation on the represented group object gives the coordinate conjugation algebra map.

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv_symm_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (X : (CommAlgCat R)ᵒᵖ) (p : ↑(HopfAlgebra.points (Opposite.unop X))) : (grpObjPointsMulEquiv H X).symm p = (CategoryTheory.opEquiv X (grpObj H)).symm (CommAlgCat.ofHom p.ofConv)

The inverse point equivalence bundles a convolution point as a morphism in the opposite category of commutative algebras.

@[simp]

theorem TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv_comp_grpObjMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (X : (CommAlgCat R)ᵒᵖ) (q : X ⟶ grpObj K) : (grpObjPointsMulEquiv H X) (CategoryTheory.CategoryStruct.comp q (grpObjMap f)) = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app (Opposite.unop X))) ((grpObjPointsMulEquiv K X) q)

Under the group-object point equivalences, composition with the morphism represented by f is precomposition of algebra-valued points with f.

noncomputable def TauCeti.CommHopfAlgCat.groupYonedaPointsFunctorIso {R : Type u} [CommRing R] : groupYonedaPointsFunctor ≅ pointsFunctor

Group-object Yoneda, transported through the Hopf-algebra/cogroup and double-opposite equivalences, is naturally isomorphic to the existing group-valued functor of points.

Equations

• TauCeti.CommHopfAlgCat.groupYonedaPointsFunctorIso = CategoryTheory.NatIso.ofComponents TauCeti.CommHopfAlgCat.groupYonedaPointsObjIso✝ ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.groupYonedaPointsFunctorIso_hom_app_app_apply {R : Type u} [CommRing R] (H : (CommHopfAlgCat R)ᵒᵖ) (A : CommAlgCat R) (f : ↑((groupYonedaPointsFunctor.obj H).obj A)) : (CategoryTheory.ConcreteCategory.hom ((groupYonedaPointsFunctorIso.hom.app H).app A)) f = WithConv.toConv (CommAlgCat.Hom.hom ((groupYonedaPointsHomEquiv H A) f))

The forward map of groupYonedaPointsFunctorIso unops a Yoneda morphism and regards its underlying algebra homomorphism as a convolution point.

@[simp]

theorem TauCeti.CommHopfAlgCat.groupYonedaPointsFunctorIso_inv_app_app_apply {R : Type u} [CommRing R] (H : (CommHopfAlgCat R)ᵒᵖ) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((groupYonedaPointsFunctorIso.inv.app H).app A)) p = (groupYonedaPointsHomEquiv H A).symm (CommAlgCat.ofHom p.ofConv)

The inverse map of groupYonedaPointsFunctorIso bundles a convolution point as a commutative-algebra morphism and takes its opposite.

instance TauCeti.CommHopfAlgCat.pointsFunctor_full {R : Type u} [CommRing R] : pointsFunctor.Full

The same-universe group-valued functor of points is full: every natural group homomorphism between point functors is induced by a coordinate Hopf-algebra morphism.

theorem TauCeti.CommHopfAlgCat.isIso_of_isIso_mapPointsFunctor {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) [CategoryTheory.IsIso (mapPointsFunctor f)] : CategoryTheory.IsIso f

A coordinate Hopf-algebra morphism is an isomorphism when its induced natural map on points is an isomorphism.

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

The coordinate Hopf-algebra morphism that a natural transformation of group-valued points functors comes from, recovered by fullness of the functor of points.

Its direction is K ⟶ H, opposite to that of the natural map pointsFunctor H ⟶ pointsFunctor K it is recovered from.

Equations

• TauCeti.CommHopfAlgCat.homOfPointsMap α = (TauCeti.CommHopfAlgCat.pointsFunctor.preimage α).unop

@[simp]

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_homOfPointsMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (α : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor) : mapPointsFunctor (homOfPointsMap α) = α

Pre-composition by the recovered coordinate morphism is the natural points map it was recovered from. This is the defining property of TauCeti.CommHopfAlgCat.homOfPointsMap, and the only thing its users need.

@[simp]

theorem TauCeti.CommHopfAlgCat.homOfPointsMap_mapPointsFunctor {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (φ : K ⟶ H) : homOfPointsMap (mapPointsFunctor φ) = φ

Recovering a coordinate morphism from the points map it induces returns that morphism. With TauCeti.CommHopfAlgCat.mapPointsFunctor_homOfPointsMap this makes TauCeti.CommHopfAlgCat.homOfPointsMap a two-sided inverse of TauCeti.CommHopfAlgCat.mapPointsFunctor, and it is where faithfulness of the functor of points is used rather than only its fullness.

@[simp]

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

The recovered coordinate morphism of an identity points map is the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.homOfPointsMap_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (α : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor) (β : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor) : homOfPointsMap (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (homOfPointsMap β) (homOfPointsMap α)

The recovered coordinate morphism of a composite points map is the composite of the recovered morphisms, in the opposite order: TauCeti.CommHopfAlgCat.homOfPointsMap is contravariant, like TauCeti.CommHopfAlgCat.mapPointsFunctor.

instance TauCeti.CommHopfAlgCat.pointsFunctorForget_unopUnop_isRepresentable {R : Type u} [CommRing R] (H : Type u) [CommRing H] [HopfAlgebra R H] : ((CategoryTheory.unopUnop (CommAlgCat R)).comp (HopfAlgebra.pointsFunctor.comp (CategoryTheory.forget GrpCat))).IsRepresentable

Presenting the corepresentable underlying points functor on the double opposite of CommAlgCat R produces a representable presheaf on (CommAlgCat R)ᵒᵖ.

theorem TauCeti.CommHopfAlgCat.essImage_pointsFunctor {R : Type u} [CommRing R] : pointsFunctor.essImage = fun (F : CategoryTheory.Functor (CommAlgCat R) GrpCat) => (F.comp (CategoryTheory.forget GrpCat)).IsCorepresentable

A same-universe group-valued functor on commutative R-algebras lies in the essential image of the functor of points exactly when its underlying type-valued functor is corepresentable.

instance TauCeti.HopfAlgebra.pointsPresheaf_isRepresentable {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsPresheaf H).IsRepresentable

The type-valued points presheaf is represented by the coordinate algebra on the opposite category.