Points of Hopf-ideal quotients

For a Hopf ideal I in a commutative Hopf algebra H, the quotient coordinate Hopf algebra H ⧸ I represents a closed subgroup of the affine group represented by H. On functors of points this is the injective group homomorphism (H ⧸ I →ₐ[R] A) → (H →ₐ[R] A) obtained by pre-composing with the quotient map H → H ⧸ I.

This file records the point-level part of that dictionary. The image is characterized by the ordinary algebraic condition that an A-point of H vanish on the ideal I; equivalently, the point factors uniquely through the quotient algebra.

Main declarations

• CommHopfAlgCat.quotientPointsHom: the group homomorphism from quotient points to ambient points.
• CommHopfAlgCat.liftQuotientPoint: factor an ambient point through H ⧸ I when it kills I.
• CommHopfAlgCat.mem_range_quotientPointsHom_iff: quotient points are exactly ambient points killing I.
• CommHopfAlgCat.quotientPointsSubgroup: the subgroup of ambient points cut out by I.
• CommHopfAlgCat.eq_one_of_mem_quotientPointsSubgroup_augmentation: the subgroup cut out by the augmentation ideal consists only of the identity point.
• CommHopfAlgCat.instIsMulCommutativeQuotientPointsSubgroup: when the quotient Hopf algebra is cocommutative, the cut-out point subgroup is commutative.
• CommHopfAlgCat.mem_quotientPointsSubgroup_map_iff: membership in the point subgroup cut out by an ideal mapped along a morphism is detected after pullback.
• CommHopfAlgCat.mapDomainMulEquiv_mem_quotientPointsSubgroup_comapOfSurjective_iff: transport of quotient-subgroup membership along a bialgebra equivalence.

References

This is a Layer 3 prerequisite for TauCetiRoadmap/ReductiveGroups/README.md, "Hopf ideals ↔ closed subgroup schemes". It builds on the quotient Hopf algebra API in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Basic and Mathlib's algebra quotient universal property Ideal.Quotient.liftₐ.

noncomputable def TauCeti.CommHopfAlgCat.quotientPointsHom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) : HopfAlgebra.points A ⟶ HopfAlgebra.points A

The map on A-points induced by the quotient coordinate morphism H ⟶ H ⧸ I.

Contravariantly, this is the closed-subgroup inclusion on points: it sends a point of the quotient Hopf algebra to its composite with the quotient map from H.

Equations

• TauCeti.CommHopfAlgCat.quotientPointsHom H I A = (TauCeti.CommHopfAlgCat.mapPointsFunctor (TauCeti.CommHopfAlgCat.mkQuotient H I)).app A

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) f = WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (mkQuotient H I)))

The quotient-points map acts by pre-composition with the quotient morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_apply_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) (h : ↑H) : ((CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) f).ofConv h = f.ofConv ((Ideal.Quotient.mkₐ R I.toIdeal) h)

Pointwise form of CommHopfAlgCat.quotientPointsHom_apply.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_eq_quotientPointsHom_of_mkQuotient_comp {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : quotient H I ⟶ K) (g : H ⟶ K) (hfg : CategoryTheory.CategoryStruct.comp (mkQuotient H I) f = g) (A : CommAlgCat R) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor g).app A)) q = (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) ((CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) q)

Mapping a point along a coordinate morphism that factors through a Hopf-ideal quotient is the same as first mapping it to the quotient and then including the quotient point into the ambient point group.

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_injective {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A))

The map from quotient points to ambient points is injective.

noncomputable def TauCeti.CommHopfAlgCat.liftQuotientPoint {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (hg : ∀ h ∈ I, g.ofConv h = 0) : ↑(HopfAlgebra.points A)

An ambient A-point factors through H ⧸ I when it kills the Hopf ideal I.

Equations

• TauCeti.CommHopfAlgCat.liftQuotientPoint H I A g hg = WithConv.toConv (Ideal.Quotient.liftₐ I.toIdeal g.ofConv ⋯)

@[simp]

theorem TauCeti.CommHopfAlgCat.liftQuotientPoint_mk {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (hg : ∀ h ∈ I, g.ofConv h = 0) (h : ↑H) : (liftQuotientPoint H I A g hg).ofConv ((Ideal.Quotient.mkₐ R I.toIdeal) h) = g.ofConv h

The quotient point built from a point killing I evaluates on a quotient class by choosing any representative.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_liftQuotientPoint {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (hg : ∀ h ∈ I, g.ofConv h = 0) : (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) (liftQuotientPoint H I A g hg) = g

Factoring a point that kills I through the quotient and then including it back in the ambient point group recovers the original point.

@[simp]

theorem TauCeti.CommHopfAlgCat.commutator_liftQuotientPoint_apply_mkQuotient {R : Type u} [CommRing R] {A : CommHopfAlgCat R} (I : HopfIdeal R ↑A) (B : CommAlgCat R) (g h : WithConv (↑A →ₐ[R] ↑B)) (hg : ∀ x ∈ I, g.ofConv x = 0) (hh : ∀ x ∈ I, h.ofConv x = 0) (x : ↑A) : ⁅liftQuotientPoint A I B g hg, liftQuotientPoint A I B h hh⁆.ofConv ((CommHopfAlgCat.Hom.hom (mkQuotient A I)) x) = ⁅g, h⁆.ofConv x

Evaluating the commutator of two lifted quotient points on a quotient class gives the commutator of the original ambient points on its representative.

theorem TauCeti.CommHopfAlgCat.mem_range_quotientPointsHom_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : g ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) ↔ ∀ h ∈ I, g.ofConv h = 0

A point of the ambient Hopf algebra lies in the image of quotient points if and only if it kills the Hopf ideal.

noncomputable def TauCeti.CommHopfAlgCat.quotientPointsSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) : Subgroup ↑(HopfAlgebra.points A)

The subgroup of ambient A-points cut out by a Hopf ideal I.

Its elements are exactly those algebra maps H →ₐ[R] A that vanish on I; this is the point-level closed subgroup represented by the quotient coordinate Hopf algebra H ⧸ I.

Equations

• TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A = (GrpCat.Hom.hom (TauCeti.CommHopfAlgCat.quotientPointsHom H I A)).range

instance TauCeti.CommHopfAlgCat.instIsMulCommutativeQuotientPointsSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) [Coalgebra.IsCocomm R ↑(quotient H I)] (A : CommAlgCat R) : IsMulCommutative ↥(quotientPointsSubgroup H I A)

The points cut out by I form a commutative group whenever the quotient coordinate Hopf algebra is cocommutative.

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : g ∈ quotientPointsSubgroup H I A ↔ ∀ h ∈ I, g.ofConv h = 0

Membership in the subgroup of points cut out by a Hopf ideal is vanishing on that ideal.

theorem TauCeti.CommHopfAlgCat.eq_one_of_mem_quotientPointsSubgroup_augmentation {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) {g : ↑(HopfAlgebra.points A)} (hg : g ∈ quotientPointsSubgroup H (HopfIdeal.augmentation R ↑H) A) : g = 1

A point killing the augmentation ideal is the identity point: the trivial subgroup has only the identity over every value algebra.

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_augmentation_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : g ∈ quotientPointsSubgroup H (HopfIdeal.augmentation R ↑H) A ↔ g = 1

The subgroup of points cut out by the augmentation ideal consists exactly of the identity point.

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_map_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (phi : H ⟶ K) (J : HopfIdeal R ↑H) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : f ∈ quotientPointsSubgroup K (J.map (CommHopfAlgCat.Hom.hom phi)) A ↔ (have this := (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor phi).app A)) f; this) ∈ quotientPointsSubgroup H J A

A point vanishes on a Hopf ideal mapped along a morphism exactly when its pullback along that morphism vanishes on the original ideal.

theorem TauCeti.CommHopfAlgCat.mapDomainMulEquiv_mem_quotientPointsSubgroup_comapOfSurjective_iff {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑f) (I : HopfIdeal R K) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : (AlgHom.mapDomainMulEquiv (BialgEquiv.ofBijective f ⋯)) g ∈ quotientPointsSubgroup (↧H) (I.comapOfSurjective f hsurj) A ↔ g ∈ quotientPointsSubgroup (↧K) I A

Precomposition by a bijective bialgebra morphism identifies the points cut out by a Hopf ideal with the points cut out by its pullback.

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_mem_quotientPointsSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) f ∈ quotientPointsSubgroup H I A

The included quotient point belongs to the subgroup cut out by the Hopf ideal.