Points of the equalizer of two homomorphisms of affine group schemes #
The quotient by TauCeti.CommHopfAlgCat.equalizerHopfIdeal cuts out a subgroup of each point
group. This file identifies that subgroup: an A-point of K lies in it exactly when the two
morphisms induce the same map on it, which is the defining condition of the equalizer subfunctor.
Main declarations #
TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_equalizerHopfIdeal_iff: on points, the subgroup cut out by the equalizer Hopf ideal is where the two induced maps agree.
References #
The equalizer of two homomorphisms of group schemes is a closed subgroup scheme, described on
points by exactly this condition; see Milne, Algebraic Groups, §1.h, and Waterhouse,
Introduction to Affine Group Schemes, §15.3. It serves
TauCetiRoadmap/ReductiveGroups/README.md, "Hopf ideals ↔ closed subgroup schemes".
theorem
TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_equalizerHopfIdeal_iff
{R : Type u}
[CommRing R]
{H K : CommHopfAlgCat R}
(f g : H ⟶ K)
(A : CommAlgCat R)
(x : ↑(HopfAlgebra.points A))
:
x ∈ quotientPointsSubgroup K (equalizerHopfIdeal f g) A ↔ (AlgHom.mapDomain (CommHopfAlgCat.Hom.hom f)) x = (AlgHom.mapDomain (CommHopfAlgCat.Hom.hom g)) x
On points, the closed subgroup cut out by the equalizer Hopf ideal is exactly the set of points on which the two induced maps of point groups agree.