Points of a normal closed subgroup generated by morphisms #
This file gives the point-level consequences of the normal common-kernel construction. The quotient cuts out a normal subgroup over every commutative value algebra, and the abstract normal subgroup generated by the defining point images lies in it. No equality of point sets is asserted.
Main declarations #
TauCeti.CommHopfAlgCat.normalCommonKernelPoints_normal: normality on algebra-valued points.TauCeti.CommHopfAlgCat.mapPoints_normalCommonKernel_mem_quotientPointsSubgroup: every point in one of the defining families belongs to the normal common-kernel quotient points.TauCeti.CommHopfAlgCat.normalClosure_iUnion_range_mapPoints_le_normalCommonKernelPoints: the abstract normal subgroup generated by the defining point images lies in the normal quotient points.
instance
TauCeti.CommHopfAlgCat.normalCommonKernelPoints_normal
{R : Type u}
[CommRing R]
{H : CommHopfAlgCat R}
{ι : Type w}
{K : ι → CommHopfAlgCat R}
(f : (i : ι) → H ⟶ K i)
(A : CommAlgCat R)
:
The normal common-kernel quotient cuts out a normal subgroup of the ambient point group over every commutative value algebra.
theorem
TauCeti.CommHopfAlgCat.mapPoints_normalCommonKernel_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 (normalCommonKernelHopfIdeal f) A
Every point obtained from one of the defining morphisms belongs to the normal closed subgroup generated by the family.
theorem
TauCeti.CommHopfAlgCat.normalClosure_iUnion_range_mapPoints_le_normalCommonKernelPoints
{R : Type u}
[CommRing R]
{H : CommHopfAlgCat R}
{ι : Type w}
{K : ι → CommHopfAlgCat R}
(f : (i : ι) → H ⟶ K i)
(A : CommAlgCat R)
:
Subgroup.normalClosure
(⋃ (i : ι),
Set.range fun (p : ↑(HopfAlgebra.points A)) => WithConv.toConv (p.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (f i)))) ≤ quotientPointsSubgroup H (normalCommonKernelHopfIdeal f) A
The abstract normal subgroup generated by all point images lies in their normal generated closed subgroup. No equality of point sets is asserted.