Kernels of Hopf algebra morphisms

A morphism of Hopf algebras over a commutative semiring has a Hopf-ideal kernel whenever comultiplication carries its kernel into ker f ⊗ H + H ⊗ ker f; the counit and antipode conditions are automatic. Over a commutative ring, this file gives two sufficient conditions for that comultiplication property. Surjectivity provides the exactness needed to identify the kernel of the tensor-square map with ker f ⊗ H + H ⊗ ker f. Alternatively, flatness of the codomain and H / ker f makes the tensor square of the injective factor through H / ker f injective. This second construction needs no surjectivity hypothesis and applies in particular over fields, where every module is flat.

Main declarations

• BialgHom.kerOfComul: the kernel Hopf ideal from the comultiplication condition, over a commutative semiring.
• TauCeti.HopfIdeal.kerOfSurjective: the Hopf ideal given by the kernel of a surjective bialgebra morphism.
• TauCeti.HopfIdeal.ker: the kernel Hopf ideal of a bialgebra morphism with flat codomain and flat kernel quotient.
• TauCeti.HopfIdeal.ker_le_ker_comp: a Hopf kernel grows under postcomposition.
• TauCeti.HopfIdeal.kerOfSurjective_eq_ker: comparison of the two constructions when both apply.
• TauCeti.HopfIdeal.kerOfSurjective_toIdeal and TauCeti.HopfIdeal.mem_kerOfSurjective: its characteristic API.
• TauCeti.HopfIdeal.kerLiftBialgHom: the induced bialgebra morphism from the quotient by the kernel of a surjective morphism.
• TauCeti.HopfIdeal.kerLiftBialgEquiv: the resulting bialgebra equivalence from the quotient by the kernel to the codomain.
• TauCeti.HopfIdeal.isReduced_quotient_kerOfSurjective: the kernel quotient is reduced when the codomain is.
• TauCeti.HopfIdeal.kerOfSurjective_mkBialgHom: the kernel of the quotient morphism by I is I.

References

The construction is the standard kernel Hopf ideal. The tensor-kernel exactness steps use Mathlib's Algebra.TensorProduct.map_ker and flatness API.

def BialgHom.kerOfComul {R : Type u} {H : Type v} {K : Type w} [CommSemiring R] [Semiring H] [Semiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hcomul : ∀ ⦃x : H⦄, x ∈ RingHom.ker ↑f → CoalgebraStruct.comul x ∈ TauCeti.HopfIdeal.leftTensorIdeal R H (RingHom.ker ↑f) ⊔ TauCeti.HopfIdeal.rightTensorIdeal R H (RingHom.ker ↑f)) : TauCeti.HopfIdeal R H

The kernel of a bialgebra morphism as a Hopf ideal, assuming comultiplication carries its kernel into ker f ⊗ H + H ⊗ ker f. The counit and antipode conditions follow from preservation of the Hopf structure. This construction works over commutative semirings.

Equations

• f.kerOfComul hcomul = TauCeti.HopfIdeal.ofIdeal (RingHom.ker ↑f) hcomul ⋯ ⋯

@[simp]

theorem BialgHom.kerOfComul_toIdeal {R : Type u} {H : Type v} {K : Type w} [CommSemiring R] [Semiring H] [Semiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hcomul : ∀ ⦃x : H⦄, x ∈ RingHom.ker ↑f → CoalgebraStruct.comul x ∈ TauCeti.HopfIdeal.leftTensorIdeal R H (RingHom.ker ↑f) ⊔ TauCeti.HopfIdeal.rightTensorIdeal R H (RingHom.ker ↑f)) : (f.kerOfComul hcomul).toIdeal = RingHom.ker ↑f

The underlying ideal of kerOfComul is the ordinary morphism kernel.

@[simp]

theorem BialgHom.mem_kerOfComul {R : Type u} {H : Type v} {K : Type w} [CommSemiring R] [Semiring H] [Semiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hcomul : ∀ ⦃x : H⦄, x ∈ RingHom.ker ↑f → CoalgebraStruct.comul x ∈ TauCeti.HopfIdeal.leftTensorIdeal R H (RingHom.ker ↑f) ⊔ TauCeti.HopfIdeal.rightTensorIdeal R H (RingHom.ker ↑f)) {x : H} : x ∈ f.kerOfComul hcomul ↔ f x = 0

Membership in kerOfComul is vanishing under the morphism.

@[simp]

theorem BialgHom.kerOfComul_eq_bot_iff {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hcomul : ∀ ⦃x : H⦄, x ∈ RingHom.ker ↑f → CoalgebraStruct.comul x ∈ TauCeti.HopfIdeal.leftTensorIdeal R H (RingHom.ker ↑f) ⊔ TauCeti.HopfIdeal.rightTensorIdeal R H (RingHom.ker ↑f)) : f.kerOfComul hcomul = ⊥ ↔ Function.Injective ⇑f

Over rings, the kernel Hopf ideal is bottom exactly when the morphism is injective.

def TauCeti.HopfIdeal.kerOfSurjective {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : HopfIdeal R H

The kernel of a surjective bialgebra morphism, as a Hopf ideal.

Equations

• TauCeti.HopfIdeal.kerOfSurjective f hf = f.kerOfComul ⋯

@[simp]

theorem TauCeti.HopfIdeal.kerOfSurjective_toIdeal {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (kerOfSurjective f hf).toIdeal = RingHom.ker ↑f

The underlying ideal of the kernel Hopf ideal is the ring-hom kernel.

@[simp]

theorem TauCeti.HopfIdeal.mem_kerOfSurjective {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) {x : H} : x ∈ kerOfSurjective f hf ↔ f x = 0

Membership in the kernel Hopf ideal is vanishing under the bialgebra morphism.

@[simp]

theorem TauCeti.HopfIdeal.kerOfSurjective_eq_bot_iff {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : kerOfSurjective f hf = ⊥ ↔ Function.Injective ⇑f

The kernel Hopf ideal is bottom exactly when the morphism is injective.

def TauCeti.HopfIdeal.ker {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] (f : H →ₐc[R] K) [Module.Flat R (H ⧸ RingHom.ker ↑f)] : HopfIdeal R H

The ordinary kernel of a morphism of Hopf algebras with flat codomain and flat kernel quotient, as a Hopf ideal. In particular, these hypotheses hold over a field.

Equations

• TauCeti.HopfIdeal.ker f = f.kerOfComul ⋯

@[simp]

theorem TauCeti.HopfIdeal.ker_toIdeal {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] (f : H →ₐc[R] K) [Module.Flat R (H ⧸ RingHom.ker ↑f)] : (ker f).toIdeal = RingHom.ker ↑f

The underlying ideal of the kernel Hopf ideal is the ordinary ring-hom kernel.

@[simp]

theorem TauCeti.HopfIdeal.mem_ker {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] (f : H →ₐc[R] K) [Module.Flat R (H ⧸ RingHom.ker ↑f)] {x : H} : x ∈ ker f ↔ f x = 0

Membership in the kernel Hopf ideal is vanishing under the morphism.

theorem TauCeti.HopfIdeal.ker_le_ker_comp {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] {L : Type x} [Ring L] [HopfAlgebra R L] (f : H →ₐc[R] K) (g : K →ₐc[R] L) [Module.Flat R L] [Module.Flat R (H ⧸ RingHom.ker ↑f)] [Module.Flat R (H ⧸ RingHom.ker ↑(g.comp f))] : ker f ≤ ker (g.comp f)

The kernel Hopf ideal of a morphism is contained in the kernel after postcomposition.

@[simp]

theorem TauCeti.HopfIdeal.kerOfSurjective_eq_ker {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] (f : H →ₐc[R] K) [Module.Flat R (H ⧸ RingHom.ker ↑f)] (hf : Function.Surjective ⇑f) : kerOfSurjective f hf = ker f

The surjective and flat kernel constructions agree whenever both apply.

@[simp]

theorem TauCeti.HopfIdeal.ker_eq_bot_iff {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [Module.Flat R K] (f : H →ₐc[R] K) [Module.Flat R (H ⧸ RingHom.ker ↑f)] : ker f = ⊥ ↔ Function.Injective ⇑f

The kernel Hopf ideal is bottom exactly when the morphism is injective.

@[simp]

theorem TauCeti.HopfIdeal.ker_mkBialgHom {R : Type u} {H : Type v} [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) [Module.Flat R (H ⧸ I.toIdeal)] : ker (Bialgebra.Quotient.mkBialgHom I.toIdeal) = I

The kernel of the quotient bialgebra morphism by I is I.

noncomputable def TauCeti.HopfIdeal.kerLiftBialgHom {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : H ⧸ (kerOfSurjective f hf).toIdeal →ₐc[R] K

The bialgebra morphism induced from a surjective morphism on the quotient by its Hopf-ideal kernel.

Equations

• TauCeti.HopfIdeal.kerLiftBialgHom f hf = Bialgebra.Quotient.liftBialgHom (TauCeti.HopfIdeal.kerOfSurjective f hf).toIdeal f ⋯

@[simp]

theorem TauCeti.HopfIdeal.kerLiftBialgHom_mk {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (h : H) : (kerLiftBialgHom f hf) ((Ideal.Quotient.mk (kerOfSurjective f hf).toIdeal) h) = f h

The kernel quotient lift evaluates on quotient classes as the original morphism.

@[simp]

theorem TauCeti.HopfIdeal.kerLiftBialgHom_comp_mkBialgHom {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (kerLiftBialgHom f hf).comp (Bialgebra.Quotient.mkBialgHom (kerOfSurjective f hf).toIdeal) = f

The kernel quotient lift composed with the quotient map is the original morphism.

theorem TauCeti.HopfIdeal.kerLiftBialgHom_bijective {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : Function.Bijective ⇑(kerLiftBialgHom f hf)

The quotient by the Hopf-ideal kernel of a surjective morphism maps bijectively to the codomain.

noncomputable def TauCeti.HopfIdeal.kerLiftBialgEquiv {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (H ⧸ (kerOfSurjective f hf).toIdeal) ≃ₐc[R] K

The quotient by the Hopf-ideal kernel of a surjective morphism is bialgebra-equivalent to the codomain.

Equations

• TauCeti.HopfIdeal.kerLiftBialgEquiv f hf = BialgEquiv.ofBijective (TauCeti.HopfIdeal.kerLiftBialgHom f hf) ⋯

@[simp]

theorem TauCeti.HopfIdeal.kerLiftBialgEquiv_apply {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (q : H ⧸ (kerOfSurjective f hf).toIdeal) : (kerLiftBialgEquiv f hf) q = (kerLiftBialgHom f hf) q

The kernel quotient equivalence applies as the kernel quotient lift.

@[simp]

theorem TauCeti.HopfIdeal.kerLiftBialgEquiv_toBialgHom {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : ↑(kerLiftBialgEquiv f hf) = kerLiftBialgHom f hf

The bialgebra morphism underlying the kernel quotient equivalence is the kernel quotient lift.

theorem TauCeti.HopfIdeal.isReduced_quotient_kerOfSurjective {R : Type u} {H : Type v} {K : Type w} [CommRing R] [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] [IsReduced K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : IsReduced (H ⧸ (kerOfSurjective f hf).toIdeal)

The quotient by the Hopf-ideal kernel of a surjective morphism is reduced when the codomain is.

@[simp]

theorem TauCeti.HopfIdeal.kerOfSurjective_mkBialgHom {R : Type u} {H : Type v} [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : kerOfSurjective (Bialgebra.Quotient.mkBialgHom I.toIdeal) ⋯ = I

The Hopf-ideal kernel of the quotient morphism by I is I.