The universal property of a bialgebra quotient

For a two-sided ideal J of an R-bialgebra H whose underlying R-submodule is a coideal, Mathlib equips the quotient ring H ⧸ J with the structure of an R-bialgebra, descending the comultiplication and counit from H (see Mathlib.RingTheory.Bialgebra.Quotient). This file supplies the matching universal property that Mathlib lacks: Bialgebra.Quotient.liftBialgHom, the unique bialgebra morphism H ⧸ J →ₐc[R] K induced from a bialgebra morphism H →ₐc[R] K which kills J.

The construction uses only the bialgebra-quotient structure — a two-sided ideal J that is a coideal — so neither an antipode nor a Hopf-algebra structure is required. For the underlying ideal of a TauCeti.HopfIdeal, use Bialgebra.Quotient.liftBialgHom I.toIdeal directly.

Main definitions

• Bialgebra.Quotient.liftBialgHom: the bialgebra morphism H ⧸ J →ₐc[R] K induced from a bialgebra morphism f : H →ₐc[R] K which kills the two-sided coideal J, together with its computation lemmas (liftBialgHom_mk, liftBialgHom_comp_mkBialgHom) and its uniqueness characterization (liftBialgHom_unique).

References

The construction descends an algebra homomorphism through the algebra quotient Ideal.Quotient.liftₐ and upgrades it to a bialgebra morphism via BialgHom.ofAlgHom, on top of Mathlib's quotient bialgebra machinery (Mathlib.RingTheory.Bialgebra.Quotient).

The universal property of a bialgebra quotient by a two-sided coideal

For a two-sided ideal J of an R-bialgebra H whose underlying R-submodule is a coideal, Mathlib equips H ⧸ J with a bialgebra structure (Mathlib.RingTheory.Bialgebra.Quotient). The lift below is the matching universal property: a bialgebra morphism out of H that kills J factors uniquely through H ⧸ J. Only the bialgebra-quotient structure is used, so neither an antipode nor a Hopf-algebra structure is required.

@[simp]

theorem Bialgebra.Quotient.mkBialgHom_toAlgHom {R : Type u_1} {H : Type u_2} [CommRing R] [Ring H] [Bialgebra R H] (J : Ideal H) [J.IsTwoSided] [(Submodule.restrictScalars R J).IsCoideal] : ↑(mkBialgHom J) = Ideal.Quotient.mkₐ R J

The algebra homomorphism underlying the quotient bialgebra morphism is the quotient map.

noncomputable def Bialgebra.Quotient.liftBialgHom {R : Type u_1} {H : Type u_2} [CommRing R] [Ring H] [Bialgebra R H] (J : Ideal H) [J.IsTwoSided] {K : Type u_3} [Semiring K] [Bialgebra R K] [(Submodule.restrictScalars R J).IsCoideal] (f : H →ₐc[R] K) (hf : J ≤ RingHom.ker (↑f).toRingHom) : H ⧸ J →ₐc[R] K

A bialgebra morphism out of H which kills a two-sided coideal J factors through the quotient bialgebra H ⧸ J.

Equations

• Bialgebra.Quotient.liftBialgHom J f hf = BialgHom.ofAlgHom (Bialgebra.Quotient.liftBialgHomAlg✝ J f hf) ⋯ ⋯

@[simp]

theorem Bialgebra.Quotient.liftBialgHom_mk {R : Type u_1} {H : Type u_2} [CommRing R] [Ring H] [Bialgebra R H] (J : Ideal H) [J.IsTwoSided] {K : Type u_3} [Semiring K] [Bialgebra R K] [(Submodule.restrictScalars R J).IsCoideal] (f : H →ₐc[R] K) (hf : J ≤ RingHom.ker (↑f).toRingHom) (h : H) : (liftBialgHom J f hf) ((Ideal.Quotient.mk J) h) = f h

The quotient lift, evaluated on a quotient class.

@[simp]

theorem Bialgebra.Quotient.liftBialgHom_comp_mkBialgHom {R : Type u_1} {H : Type u_2} [CommRing R] [Ring H] [Bialgebra R H] (J : Ideal H) [J.IsTwoSided] {K : Type u_3} [Semiring K] [Bialgebra R K] [(Submodule.restrictScalars R J).IsCoideal] (f : H →ₐc[R] K) (hf : J ≤ RingHom.ker (↑f).toRingHom) : (liftBialgHom J f hf).comp (mkBialgHom J) = f

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

theorem Bialgebra.Quotient.liftBialgHom_unique {R : Type u_1} {H : Type u_2} [CommRing R] [Ring H] [Bialgebra R H] (J : Ideal H) [J.IsTwoSided] {K : Type u_3} [Semiring K] [Bialgebra R K] [(Submodule.restrictScalars R J).IsCoideal] (f : H →ₐc[R] K) (hf : J ≤ RingHom.ker (↑f).toRingHom) (g : H ⧸ J →ₐc[R] K) (hg : g.comp (mkBialgHom J) = f) : g = liftBialgHom J f hf

A bialgebra morphism out of the quotient is determined by its precomposition with the quotient map.