Order of Hopf-ideal quotient point subgroups

A Hopf ideal I cuts out, on every value algebra A, the subgroup of ambient points H(A) which vanish on I. This file records the elementary order behavior of this construction: if I ≤ J, then every point which kills J also kills I, so the subgroup cut out by J is contained in the subgroup cut out by I.

This is the point-level order bookkeeping for the Layer 3 ReductiveGroups roadmap item "Hopf ideals ↔ closed subgroup schemes". Larger Hopf ideals correspond contravariantly to smaller closed subgroup functors, and the inclusion is compatible with functoriality in the value algebra.

Main declarations

• CommHopfAlgCat.quotientPointsSubgroup_antitone: the cut-out point subgroup is antitone in the Hopf ideal.
• CommHopfAlgCat.quotientPointsSubgroup_sup: the point subgroup cut out by a join of Hopf ideals is the intersection of the point subgroups cut out by the joinands.
• CommHopfAlgCat.quotientPointsSubgroupInclusion: the bundled natural inclusion between subgroup functors induced by I ≤ J.
• CommHopfAlgCat.mapQuotientPointsSubgroup_inclusion_apply: these inclusions commute with post-composition in the value algebra.

References

This uses the vanishing characterization of quotient points from TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Basic and the naturality API from TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Naturality.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_antitone {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) : Antitone fun (I : HopfIdeal R ↑H) => quotientPointsSubgroup H I A

The point subgroup cut out by a Hopf ideal is antitone in the Hopf ideal: larger ideals impose more vanishing equations.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_le_of_le {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) : quotientPointsSubgroup H J A ≤ quotientPointsSubgroup H I A

If I ≤ J, then the point subgroup cut out by J is contained in the point subgroup cut out by I.

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_of_le {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) {g : ↑(HopfAlgebra.points A)} (hg : g ∈ quotientPointsSubgroup H J A) : g ∈ quotientPointsSubgroup H I A

Rewriting form of quotientPointsSubgroup_le_of_le as a membership implication.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_eq_of_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I = J) (A : CommAlgCat R) : quotientPointsSubgroup H I A = quotientPointsSubgroup H J A

If I = J, then the point subgroups cut out by I and J are equal.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_bot {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) : quotientPointsSubgroup H ⊥ A = ⊤

The point subgroup cut out by the zero Hopf ideal is the full ambient point group.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_sup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (A : CommAlgCat R) : quotientPointsSubgroup H (I ⊔ J) A = quotientPointsSubgroup H I A ⊓ quotientPointsSubgroup H J A

The point subgroup cut out by a join of Hopf ideals is the intersection of the point subgroups cut out by the joinands: a point vanishes on I ⊔ J exactly when it vanishes on I and on J.

@[simp]

theorem TauCeti.CommHopfAlgCat.mapQuotientPointsSubgroup_inclusion_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) {A B : CommAlgCat R} (χ : A ⟶ B) (g : ↥(quotientPointsSubgroup H J A)) : (mapQuotientPointsSubgroup H I χ) ((Subgroup.inclusion ⋯) g) = (Subgroup.inclusion ⋯) ((mapQuotientPointsSubgroup H J χ) g)

The subgroup inclusions associated to I ≤ J commute with maps of value algebras.

noncomputable def TauCeti.CommHopfAlgCat.quotientPointsSubgroupInclusion {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : quotientPointsSubgroupFunctor H J ⟶ quotientPointsSubgroupFunctor H I

The natural inclusion of subgroup functors associated to I ≤ J.

Equations

• TauCeti.CommHopfAlgCat.quotientPointsSubgroupInclusion H hIJ = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (Subgroup.inclusion ⋯), naturality := ⋯ }

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroupInclusion_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (A : CommAlgCat R) : (quotientPointsSubgroupInclusion H hIJ).app A = GrpCat.ofHom (Subgroup.inclusion ⋯)

The component of quotientPointsSubgroupInclusion is the subgroup inclusion.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroupInclusion_refl {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientPointsSubgroupInclusion H ⋯ = CategoryTheory.CategoryStruct.id (quotientPointsSubgroupFunctor H I)

The inclusion associated to reflexivity is the identity natural transformation.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroupInclusion_comp {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J K : HopfIdeal R ↑H} (hIJ : I ≤ J) (hJK : J ≤ K) : CategoryTheory.CategoryStruct.comp (quotientPointsSubgroupInclusion H hJK) (quotientPointsSubgroupInclusion H hIJ) = quotientPointsSubgroupInclusion H ⋯

Inclusions of quotient point subgroup functors compose along transitive ideal inclusions.