Points of a group scheme generated by morphisms

Let f i : H ⟶ K i be morphisms of commutative Hopf algebras. The common-kernel quotient of H represents the smallest closed subgroup scheme of Spec H through which all the contravariant morphisms Spec (K i) ⟶ Spec H factor. This file proves the corresponding easy direction on algebra-valued points: the subgroup generated by the images of all K i-points is contained in the points of the common-kernel quotient.

The reverse inclusion is false at this level of generality. Even when it holds after imposing conditions on the value algebra, it is a separate density or generation theorem rather than a formal consequence of the common-kernel construction.

Main declarations

• TauCeti.CommHopfAlgCat.mapPoints_commonKernel_mem_quotientPointsSubgroup: every point in one of the given families lands in the subgroup cut out by the common-kernel Hopf ideal.
• TauCeti.CommHopfAlgCat.closure_iUnion_range_mapPoints_le_commonKernelPoints: the subgroup generated by all these point images lies in the common-kernel quotient points.

This is the pointwise bridge used by the Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap: its explicitly generated group scheme must contain the elementary group generated by its root subgroups.

theorem TauCeti.CommHopfAlgCat.mapPoints_commonKernel_mem_quotientPointsSubgroup {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) : WithConv.toConv (p.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (f i))) ∈ quotientPointsSubgroup H (commonKernelHopfIdeal f) A

Every point obtained from one of the morphisms defining a common-kernel quotient belongs to the subgroup of ambient points cut out by that quotient.

theorem TauCeti.CommHopfAlgCat.closure_iUnion_range_mapPoints_le_commonKernelPoints {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (A : CommAlgCat R) : Subgroup.closure (⋃ (i : ι), Set.range fun (p : ↑(HopfAlgebra.points A)) => WithConv.toConv (p.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (f i)))) ≤ quotientPointsSubgroup H (commonKernelHopfIdeal f) A

The subgroup generated by all point images of a family of Hopf-algebra morphisms is contained in the points of their common-kernel quotient.