Generalized points of Hopf-ideal quotient inclusions #
This file identifies composition with the categorical closed-subgroup inclusion represented by a Hopf-ideal quotient with the usual precomposition map on algebra-valued points.
Main declarations #
TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv_comp_quotientGrpObjInclusion: the represented quotient inclusion acts on generalized points by the quotient-points homomorphism.
References #
This is the generalized-point form of the Layer 3 Hopf-ideal/closed-subgroup dictionary in the ReductiveGroups roadmap. It combines the represented group-object Yoneda equivalence with the point-level quotient API.
@[simp]
theorem
TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv_comp_quotientGrpObjInclusion
{R : Type u}
[CommRing R]
(H : CommHopfAlgCat R)
(I : HopfIdeal R ↑H)
(X : (CommAlgCat R)ᵒᵖ)
(q : X ⟶ grpObj (quotient H I))
:
(grpObjPointsMulEquiv H X) (CategoryTheory.CategoryStruct.comp q (quotientGrpObjInclusion H I)) = (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I (Opposite.unop X)))
((grpObjPointsMulEquiv (quotient H I) X) q)
Under the group-object point equivalences, composition with the categorical quotient inclusion is the usual quotient-points homomorphism.