Normal Hopf ideals

A Hopf ideal I in a commutative Hopf algebra H defines a closed subgroup of the affine group represented by H. This file defines normality of that closed subgroup in Hopf-algebra coordinates: the ideal is stable under the coordinate morphism of conjugation,

c♯ : H → H ⊗[R] H,

with the first tensor factor carrying the conjugating variable. Thus I is normal when c♯(I) ⊆ H ⊗ I. It also verifies the pointwise meaning of this condition: over every commutative value algebra, the subgroup cut out by a normal Hopf ideal is a normal subgroup of the ambient group of points.

Normal Hopf ideals are closed under arbitrary suprema. Every Hopf ideal has a normal core: the largest normal Hopf ideal below it. This normal-core API is the Hopf-ideal analogue of Mathlib's Subgroup.normalCore at the level of the ideal lattice. Since the ideal-to-subgroup dictionary is contravariant, J.normalCore cuts out the smallest normal closed subgroup containing the subgroup cut out by J, namely its normal closure.

Main declarations

• TauCeti.HopfIdeal.IsNormal: stability under the coordinate conjugation action.
• TauCeti.HopfIdeal.isNormal_bot: the zero Hopf ideal is normal.
• TauCeti.HopfIdeal.isNormal_iSup: arbitrary suprema of normal Hopf ideals are normal.
• TauCeti.HopfIdeal.normalCore: the largest normal Hopf ideal below a given Hopf ideal.
• TauCeti.HopfIdeal.IsNormal.map: normality is preserved by the image of a Hopf ideal.
• TauCeti.HopfIdeal.IsNormal.comapOfSurjective_of_bijective: normality is preserved by pullback along a bijective bialgebra morphism.
• TauCeti.CommHopfAlgCat.quotientPointsSubgroup_normal: a normal Hopf ideal cuts out a normal subgroup on points over every commutative value algebra.

References

The coordinate criterion is the usual adjoint-coaction characterization of a normal closed subgroup; see J. S. Milne, Algebraic Groups (2017), §3.5 and §10.20. This is the normality prerequisite in Layer 3, “Normality and quotients”, of the ReductiveGroups roadmap.

def TauCeti.HopfIdeal.IsNormal {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : Prop

A Hopf ideal is normal when the coordinate morphism of conjugation carries it into H ⊗ I. The first tensor factor of HopfAlgebra.conjugationAlgHom is the conjugating variable, so the right tensor ideal is the ideal of G × V(I).

Equations

• I.IsNormal = (Ideal.map TauCeti.HopfAlgebra.conjugationAlgHom.toRingHom I.toIdeal ≤ TauCeti.HopfIdeal.rightTensorIdeal R H I.toIdeal)

theorem TauCeti.HopfIdeal.isNormal_def {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.IsNormal ↔ Ideal.map HopfAlgebra.conjugationAlgHom.toRingHom I.toIdeal ≤ rightTensorIdeal R H I.toIdeal

Normality restated as the defining ideal inclusion.

theorem TauCeti.HopfIdeal.isNormal_iff_conjugation_mem {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.IsNormal ↔ ∀ ⦃x : H⦄, x ∈ I → HopfAlgebra.conjugationAlgHom x ∈ rightTensorIdeal R H I.toIdeal

A Hopf ideal is normal exactly when the coordinate conjugation of each of its elements belongs to H ⊗ I.

theorem TauCeti.HopfIdeal.IsNormal.conjugation_mem {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {I : HopfIdeal R H} (hI : I.IsNormal) {x : H} (hx : x ∈ I) : HopfAlgebra.conjugationAlgHom x ∈ rightTensorIdeal R H I.toIdeal

The coordinate conjugation of an element of a normal Hopf ideal belongs to H ⊗ I.

theorem TauCeti.HopfIdeal.IsNormal.map {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {K : Type w} [CommSemiring K] [HopfAlgebra R K] {I : HopfIdeal R H} (hI : I.IsNormal) (f : H →ₐc[R] K) : (I.map f).IsNormal

The image of a normal Hopf ideal under a morphism of commutative Hopf algebras is normal.

Contravariantly, pulling a normal closed subgroup back along a morphism of affine group schemes again gives a normal closed subgroup.

@[simp]

theorem TauCeti.HopfIdeal.isNormal_bot {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] : ⊥.IsNormal

The zero Hopf ideal cuts out the whole affine group, hence is normal.

theorem TauCeti.HopfIdeal.isNormal_iSup {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {i : Sort u_1} {I : i → HopfIdeal R H} (hI : ∀ (j : i), (I j).IsNormal) : (⨆ (j : i), I j).IsNormal

An arbitrary supremum of normal Hopf ideals is normal.

theorem TauCeti.HopfIdeal.isNormal_sSup {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {s : Set (HopfIdeal R H)} (hs : ∀ I ∈ s, I.IsNormal) : (sSup s).IsNormal

The supremum of a set of normal Hopf ideals is normal.

noncomputable def TauCeti.HopfIdeal.normalCore {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (J : HopfIdeal R H) : HopfIdeal R H

The largest normal Hopf ideal contained in J.

Contravariantly, it cuts out the smallest normal closed subgroup containing the subgroup cut out by J, namely its normal closure.

Equations

• J.normalCore = sSup {I : TauCeti.HopfIdeal R H | I.IsNormal ∧ I ≤ J}

@[simp]

theorem TauCeti.HopfIdeal.isNormal_normalCore {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (J : HopfIdeal R H) : J.normalCore.IsNormal

The normal core is normal.

theorem TauCeti.HopfIdeal.normalCore_le {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (J : HopfIdeal R H) : J.normalCore ≤ J

The normal core of a Hopf ideal is contained in that ideal.

theorem TauCeti.HopfIdeal.le_normalCore_iff_of_isNormal {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (I J : HopfIdeal R H) (hI : I.IsNormal) : I ≤ J.normalCore ↔ I ≤ J

A normal Hopf ideal lies below the normal core of J exactly when it lies below J.

theorem TauCeti.HopfIdeal.normalCore_mono {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} (hIJ : I ≤ J) : I.normalCore ≤ J.normalCore

The normal-core operator is monotone.

theorem TauCeti.HopfIdeal.normalCore_eq_self_iff {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (J : HopfIdeal R H) : J.normalCore = J ↔ J.IsNormal

A Hopf ideal equals its normal core exactly when it is normal.

@[simp]

theorem TauCeti.HopfIdeal.normalCore_idempotent {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (J : HopfIdeal R H) : J.normalCore.normalCore = J.normalCore

Taking the normal core twice has the same effect as taking it once.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_normal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : (quotientPointsSubgroup H I A).Normal

A normal Hopf ideal cuts out a normal subgroup of points over every commutative R-algebra.

theorem TauCeti.CommHopfAlgCat.isNormal_iff_quotientPointsSubgroup_normal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : I.IsNormal ↔ ∀ (A : CommAlgCat R), (quotientPointsSubgroup H I A).Normal

A Hopf ideal is normal if and only if it cuts out a normal subgroup over every commutative value algebra.

theorem TauCeti.HopfIdeal.IsNormal.comapOfSurjective_of_bijective {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {I : HopfIdeal R K} (hI : I.IsNormal) (f : H →ₐc[R] K) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑f) : (I.comapOfSurjective f hsurj).IsNormal

Pulling a normal Hopf ideal back along a bijective bialgebra morphism preserves normality.