Kernels of Hopf algebra morphisms

This file records two conditions under which the kernel of a morphism of Hopf algebras is a Hopf ideal. Over an arbitrary commutative base, surjectivity provides the exactness needed to identify the kernel of the tensor-square map with ker f ⊗ H + H ⊗ ker f. Over a field, no surjectivity hypothesis is needed: after factoring through H / ker f, the tensor square of the injective factor remains injective.

This is a Layer 3 prerequisite for the reductive-groups roadmap target "Hopf ideals ↔ closed subgroup schemes", specifically the "kernels" part of the Hopf-ideal/closed-subgroup dictionary.

Main declarations

• TauCeti.HopfIdeal.kerOfSurjective: the Hopf ideal given by the kernel of a surjective bialgebra morphism.
• TauCeti.HopfIdeal.ker: the kernel Hopf ideal of an arbitrary bialgebra morphism over a field.
• TauCeti.HopfIdeal.ker_le_ker_comp: a Hopf kernel grows under postcomposition.
• TauCeti.HopfIdeal.kerOfSurjective_eq_ker: comparison of the two constructions over a field.
• 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.kerOfSurjective_mkBialgHom: the kernel of the quotient morphism by I is I.
• TauCeti.HopfIdeal.ker_lTensor_eq_rightTensorIdeal: tensoring on the left by a flat algebra carries the kernel of an algebra map to the corresponding right tensor ideal.

References

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

theorem TauCeti.HopfIdeal.ker_lTensor_eq_rightTensorIdeal {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Module.Flat R A] (f : A →ₐ[R] B) : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) f) = rightTensorIdeal R A (RingHom.ker f)

Tensoring on the left by a flat algebra carries the kernel of an algebra map to the corresponding right tensor ideal.

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 = TauCeti.HopfIdeal.ofKerComul✝ f ⋯

@[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.

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 {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) : HopfIdeal k H

The ordinary kernel of a morphism of Hopf algebras over a field, as a Hopf ideal. No surjectivity hypothesis is needed over a field.

Equations

• TauCeti.HopfIdeal.ker f = TauCeti.HopfIdeal.ofKerComul✝ f ⋯

@[simp]

theorem TauCeti.HopfIdeal.ker_toIdeal {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) : (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 {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) {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 {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] {L : Type x} [Ring L] [HopfAlgebra k L] (f : H →ₐc[k] K) (g : K →ₐc[k] L) : 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 {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) (hf : Function.Surjective ⇑f) : kerOfSurjective f hf = ker f

Over a field, the kernel constructed for a surjective morphism agrees with the canonical kernel, which does not require the surjectivity hypothesis.

@[simp]

theorem TauCeti.HopfIdeal.ker_mkBialgHom {H : Type v} [Ring H] {k : Type u} [Field k] [HopfAlgebra k H] (I : HopfIdeal k H) : ker (Bialgebra.Quotient.mkBialgHom I.toIdeal) = I

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

@[simp]

theorem TauCeti.HopfIdeal.ker_eq_bot_iff {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [Field k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) : ker f = ⊥ ↔ Function.Injective ⇑f

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

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ₐ R (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.

@[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.