Kernels of Hopf algebra morphisms

This file records that the kernel of a surjective morphism of Hopf algebras is a Hopf ideal. The surjectivity hypothesis is the exactness input needed to identify the kernel of the tensor-square map with ker f ⊗ H + H ⊗ ker f.

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.ker: the Hopf ideal given by the kernel of a surjective bialgebra morphism.
• TauCeti.HopfIdeal.ker_toIdeal and TauCeti.HopfIdeal.mem_ker: 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.ker_mkBialgHom: the kernel of the quotient morphism by I is I.

References

The construction is the standard kernel Hopf ideal. The tensor-kernel exactness step uses Mathlib's Algebra.TensorProduct.map_ker.

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] (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.ker f hf = TauCeti.HopfIdeal.ofIdeal (RingHom.ker ↑f) ⋯ ⋯ ⋯

@[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] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (ker f hf).toIdeal = RingHom.ker ↑f

The underlying ideal of the kernel Hopf ideal is the 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] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) {x : H} : x ∈ ker f hf ↔ f x = 0

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

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] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : ker f hf = ⊥ ↔ 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 ⧸ (ker 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.ker 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 (ker 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 (ker 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 ⧸ (ker 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 ⧸ (ker 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.ker_mkBialgHom {R : Type u} {H : Type v} [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : ker (Bialgebra.Quotient.mkBialgHom I.toIdeal) ⋯ = I

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