Point compatibility for order maps between Hopf-ideal quotients

If I ≤ J are Hopf ideals in a commutative Hopf algebra H, then the quotient map H ⟶ H ⧸ J kills I, so it factors through a coordinate morphism H ⧸ I ⟶ H ⧸ J. Contravariantly, this is the map on closed-subgroup functors induced by the inclusion of the subgroup cut out by J into the subgroup cut out by I.

This file records the compatibility of that quotient-to-quotient morphism with the already-defined point subgroup inclusions. The coordinate-level morphism itself is defined in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Basic.

Main declarations

• CommHopfAlgCat.quotientPointsHom_mapPointsFunctor_quotientMapOfLe_app: on points, precomposition with quotientMapOfLe is compatible with the ambient quotient-points inclusions.

References

This is point-level bookkeeping for the ReductiveGroups roadmap, Layer 3, "Hopf ideals ↔ closed subgroup schemes". It uses the quotient universal property from TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Basic and the cut-out subgroup order API from TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Order.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_mapPointsFunctor_quotientMapOfLe_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor (quotientMapOfLe H hIJ)).app A)) f) = (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H J A)) f

On points, precomposition with quotientMapOfLe is compatible with the ambient quotient-points inclusions.

Starting with a point of H ⧸ J, mapping it to a point of H ⧸ I and then including into ambient H-points gives the same ambient point as the direct inclusion from H ⧸ J.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_mapPointsFunctor_quotientMapOfLe_app_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) (h : ↑H) : ((CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor (quotientMapOfLe H hIJ)).app A)) f)).ofConv h = f.ofConv ((Ideal.Quotient.mkₐ R J.toIdeal) h)

The pointwise form of CommHopfAlgCat.quotientPointsHom_mapPointsFunctor_quotientMapOfLe_app.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroupIso_hom_mapPointsFunctor_quotientMapOfLe_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (quotientPointsSubgroupIso H I A).hom) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor (quotientMapOfLe H hIJ)).app A)) f) = (Subgroup.inclusion ⋯) ((CategoryTheory.ConcreteCategory.hom (quotientPointsSubgroupIso H J A).hom) f)

Under the quotient-point subgroup isomorphisms, the points map induced by quotientMapOfLe is exactly the subgroup inclusion attached to I ≤ J.