Naturality of Hopf-ideal quotient points #
For a Hopf ideal I in a commutative Hopf algebra H, the quotient Hopf algebra
H ⧸ I represents the closed subgroup whose A-points are the ambient H-points killing
I. This file records that this description is natural in the value algebra A.
The quotient-points inclusion commutes with post-composition along a morphism
A ⟶ B of commutative R-algebras. Consequently the subgroup of ambient points cut out by
I is preserved by the functor-of-points map, and the value-algebra map restricts to a
homomorphism between these subgroups.
This is a small Layer 3 prerequisite for the ReductiveGroups roadmap target "Hopf ideals ↔
closed subgroup schemes": the closed-subgroup functor represented by H ⧸ I must be a
subfunctor of the ambient points functor, not just a subgroup at each individual algebra.
The quotient-points inclusion is natural in the value algebra.
The quotient-points inclusion commutes with post-composition, including when the source and target value algebras lie in different universes.
Post-composition by an algebra homomorphism preserves the ambient-point subgroup cut out by a Hopf ideal, including when the source and target value algebras lie in different universes.
Post-composition preserves the ambient-point subgroup cut out by a Hopf ideal.
The functor-of-points map restricted to the subgroups cut out by a Hopf ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restricted map on cut-out subgroups is induced by the ambient functor-of-points map.
Coercing the restricted subgroup map gives the ambient functor-of-points map.
The restricted subgroup maps preserve identity morphisms of value algebras.
The restricted subgroup maps preserve composition of value-algebra morphisms.
The value-algebra functor of the point subgroups cut out by a Hopf ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The object part of the subgroup functor is the cut-out point subgroup.
The map part of the subgroup functor is the restricted value-algebra map.
The subgroup functor includes naturally into the ambient functor of points.
Equations
- TauCeti.CommHopfAlgCat.quotientPointsSubgroupIncl H I = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A).subtype, naturality := ⋯ }
Instances For
The component of the subgroup inclusion is the subgroup subtype map.
Pointwise form of the restricted subgroup map.
The component isomorphism between quotient points and the cut-out subgroup.
Equations
Instances For
The component isomorphism sends a quotient point to its included ambient point.
The inverse component is the quotient point factoring the included ambient point.
The quotient Hopf algebra represents the subgroup functor cut out by the Hopf ideal.
Equations
Instances For
The natural isomorphism's forward component is the quotient-subgroup component isomorphism.
The natural isomorphism's inverse component is the quotient lift of a subgroup point.
The Hopf-ideal cut-out subgroup functor is naturally isomorphic to any stable subgroup family with the same pointwise membership condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A Hopf quotient represents any value-algebra-stable family of ambient point subgroups whose membership condition agrees with vanishing on the Hopf ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The represented subgroup point underlying a quotient point is induced by the quotient coordinate map.
Applying the quotient inclusion to the inverse representing isomorphism recovers the ambient subgroup point.
The image of a quotient point under the subgroup functor is its mapped quotient point, viewed inside the cut-out subgroup.
Factoring an ambient point through the quotient is natural in the value algebra.