Points of the kernel of an affine group-scheme morphism

For a morphism f : H ⟶ K of commutative Hopf algebras, the kernel closed subgroup scheme TauCeti.CommHopfAlgCat.kernelSpec f is cut out by the kernel Hopf ideal. This file records its kernel semantics on functors of points: for every commutative R-algebra A, an A-point of the source group scheme maps to the unit point exactly when it lies in the subgroup of points cut out by the kernel Hopf ideal — the A-points of the kernel. Since this holds for all test algebras, by Yoneda the kernel closed subgroup scheme represents the kernel of the induced morphism of group-valued points functors.

Main declarations

• TauCeti.CommHopfAlgCat.mapPointsFunctor_app_eq_one_iff: the points-level kernel property.
• TauCeti.CommHopfAlgCat.quotientPointsSubgroup_kernelHopfIdeal_eq_ker_mapPointsFunctor: the same property as an equality of subgroups of points.

@[simp]

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_app_eq_one_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : WithConv.toConv (g.ofConv.comp ↑(CommHopfAlgCat.Hom.hom f)) = 1 ↔ g ∈ quotientPointsSubgroup K (kernelHopfIdeal f) A

Kernel semantics on functors of points: for every commutative R-algebra A, an A-point of the source is sent to the unit point exactly when it lies in the subgroup of points cut out by the kernel Hopf ideal — the A-points of kernelSpec f. This is the universal property of the kernel tested against arbitrary algebras; by Yoneda, kernelSpec f represents the kernel of the induced morphism of group-valued points functors.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_kernelHopfIdeal_eq_ker_mapPointsFunctor {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) : quotientPointsSubgroup K (kernelHopfIdeal f) A = (GrpCat.Hom.hom ((mapPointsFunctor f).app A)).ker

For every commutative R-algebra A, the subgroup of A-points cut out by the kernel Hopf ideal of f is the kernel of the induced map on A-points.