Hopf-ideal quotients of commutative Hopf algebras

This file packages the quotient of a commutative Hopf algebra by a Hopf ideal as an object of CommHopfAlgCat, with its quotient morphism, the induced morphisms out of it, its kernel, the maps between quotients by nested Hopf ideals, and its transport along surjective ambient morphisms; the quotient by the zero Hopf ideal is the original Hopf algebra. The Hopf algebra structure and quotient bialgebra morphism are supplied by Mathlib's quotient instances and morphisms.

The same quotient of a finite-type commutative Hopf algebra is again an object of FiniteTypeCommHopfAlgCat: finite type descends along the surjective quotient algebra map.

Main declarations

• TauCeti.CommHopfAlgCat.quotient: the quotient object in CommHopfAlgCat.
• TauCeti.CommHopfAlgCat.mkQuotient_surjective: the quotient morphism is surjective.
• TauCeti.CommHopfAlgCat.mkQuotient_hom_ext: morphisms out of a quotient are determined after precomposition with the quotient morphism.
• TauCeti.FiniteTypeCommHopfAlgCat.quotient: the quotient object in FiniteTypeCommHopfAlgCat.
• TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient: the quotient morphism.
• TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_hom_ext: morphisms out of a quotient are determined after precomposition with the quotient morphism.
• TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_ker: its kernel characterization.
• TauCeti.CommHopfAlgCat.liftQuotient, TauCeti.CommHopfAlgCat.liftQuotient_unique: the morphism out of a quotient induced by a morphism killing the Hopf ideal, and its uniqueness.
• TauCeti.FiniteTypeCommHopfAlgCat.liftQuotient: the induced morphism out of a quotient.
• TauCeti.CommHopfAlgCat.toIdeal_le_ker_of_mkQuotient_comp: a morphism factoring through the quotient by a Hopf ideal kills that ideal.
• TauCeti.CommHopfAlgCat.quotientMapOfLe: the morphism H ⧸ I ⟶ H ⧸ J induced by I ≤ J.
• TauCeti.CommHopfAlgCat.quotientMapOfLe_surjective: quotient-to-quotient coordinate maps are surjective.
• TauCeti.CommHopfAlgCat.quotientMapOfLe_comp_liftQuotient_eq: a quotient-to-quotient coordinate map followed by a lift through the larger ideal is identified by its precomposition with the quotient morphism.
• TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe_surjective: the finite-type form of quotient-to-quotient surjectivity.
• TauCeti.CommHopfAlgCat.kerOfSurjective_quotientMapOfLe: over a commutative ring, the Hopf ideal J/I is the surjective kernel of the induced quotient map.
• TauCeti.CommHopfAlgCat.ker_quotientMapOfLe: over a field, the Hopf ideal J/I is the kernel of the induced quotient map.
• TauCeti.CommHopfAlgCat.quotientBotIso: quotienting by the zero Hopf ideal does not change a commutative Hopf algebra.
• TauCeti.CommHopfAlgCat.quotientIsoOfSurjective: a surjective ambient morphism identifies the source quotient by an inverse-image Hopf ideal with the target quotient.
• TauCeti.CommHopfAlgCat.quotientIsoOfIso: the specialization to an ambient isomorphism.
• TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso: the quotient by the kernel of a surjective morphism is its target.
• TauCeti.CommHopfAlgCat.quotientIsoOfKerOfSurjectiveEq: the quotient by a Hopf ideal equal to the kernel of a surjective morphism is its target.
• TauCeti.CommHopfAlgCat.quotientIsoOfComapEq: an ambient isomorphism pulling one Hopf ideal back to another induces an isomorphism of the quotients.
• TauCeti.HopfIdeal.comapOfSurjective_eq_of_hom_le_of_inv_le: two inverse containments under an ambient automorphism imply invariance of a Hopf ideal.
• TauCeti.FiniteTypeCommHopfAlgCat.quotientIsoOfIso: an ambient isomorphism induces an isomorphism between the corresponding finite-type Hopf-ideal quotients.
• TauCeti.FiniteTypeCommHopfAlgCat.minimal_quotientProperty_comapOfIso: a minimal Hopf ideal among those whose quotient has an isomorphism-closed property pulls back to a minimal one along an ambient isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.quotientBotIso: quotienting by the zero Hopf ideal does not change a finite-type commutative Hopf algebra.

References

The quotient Hopf algebra construction is Mathlib's (Mathlib.RingTheory.HopfAlgebra.Quotient), applied through the instances of TauCeti.Algebra.HopfAlgebra.HopfIdeal.Basic; see Sweedler, Hopf Algebras, Chapter 4, and Waterhouse, Introduction to Affine Group Schemes, §16. The finite-type descent is Mathlib's Algebra.FiniteType.quotient.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.quotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : CommHopfAlgCat R

The quotient of a commutative Hopf algebra by a Hopf ideal, as a bundled commutative Hopf algebra.

Equations

• TauCeti.CommHopfAlgCat.quotient H I = ↧(↑H ⧸ I.toIdeal)

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.mkQuotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : H ⟶ quotient H I

The quotient morphism H ⟶ H ⧸ I in CommHopfAlgCat.

Equations

• TauCeti.CommHopfAlgCat.mkQuotient H I = CommHopfAlgCat.ofHom (Bialgebra.Quotient.mkBialgHom I.toIdeal)

theorem TauCeti.CommHopfAlgCat.hom_mkQuotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : CommHopfAlgCat.Hom.hom (mkQuotient H I) = Bialgebra.Quotient.mkBialgHom I.toIdeal

The quotient morphism has the expected underlying bialgebra morphism.

theorem TauCeti.CommHopfAlgCat.mkQuotient_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (h : ↑H) : (CommHopfAlgCat.Hom.hom (mkQuotient H I)) h = (Ideal.Quotient.mkₐ R I.toIdeal) h

The quotient morphism sends an element to its quotient class.

theorem TauCeti.CommHopfAlgCat.mkQuotient_toLinearMap {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : (CommHopfAlgCat.Hom.hom (mkQuotient H I)).toLinearMap = (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap

The linear map underlying the quotient morphism is the ideal quotient map.

theorem TauCeti.CommHopfAlgCat.mkQuotient_ker {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : RingHom.ker (↑(CommHopfAlgCat.Hom.hom (mkQuotient H I))).toRingHom = I.toIdeal

The kernel of the quotient morphism is the Hopf ideal being quotiented by.

theorem TauCeti.CommHopfAlgCat.mkQuotient_eq_zero_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (h : ↑H) : (CommHopfAlgCat.Hom.hom (mkQuotient H I)) h = 0 ↔ h ∈ I.toIdeal

An element maps to zero in the quotient exactly when it belongs to the Hopf ideal.

theorem TauCeti.CommHopfAlgCat.mkQuotient_surjective {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (mkQuotient H I))

The quotient morphism is surjective.

instance TauCeti.CommHopfAlgCat.mkQuotient_epi {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} : CategoryTheory.Epi (mkQuotient H I)

A Hopf-algebra quotient morphism is an epimorphism.

theorem TauCeti.CommHopfAlgCat.mkQuotient_hom_ext {R : Type u} [CommRing R] {H X : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {f g : quotient H I ⟶ X} (h : CategoryTheory.CategoryStruct.comp (mkQuotient H I) f = CategoryTheory.CategoryStruct.comp (mkQuotient H I) g) : f = g

Morphisms out of a Hopf-algebra quotient are determined by their composites with the quotient morphism.

theorem TauCeti.CommHopfAlgCat.mkQuotient_hom_ext_iff {R : Type u} [CommRing R] {H X : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {f g : quotient H I ⟶ X} : f = g ↔ CategoryTheory.CategoryStruct.comp (mkQuotient H I) f = CategoryTheory.CategoryStruct.comp (mkQuotient H I) g

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.liftQuotient {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : quotient H I ⟶ K

A morphism of commutative Hopf algebras out of H which kills a Hopf ideal factors through the quotient object.

Equations

• TauCeti.CommHopfAlgCat.liftQuotient I f hf = CommHopfAlgCat.ofHom (Bialgebra.Quotient.liftBialgHom I.toIdeal (CommHopfAlgCat.Hom.hom f) hf)

theorem TauCeti.CommHopfAlgCat.hom_liftQuotient {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : CommHopfAlgCat.Hom.hom (liftQuotient I f hf) = Bialgebra.Quotient.liftBialgHom I.toIdeal (CommHopfAlgCat.Hom.hom f) hf

The quotient lift has the expected underlying bialgebra morphism.

theorem TauCeti.CommHopfAlgCat.liftQuotient_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (h : ↑H) : (CommHopfAlgCat.Hom.hom (liftQuotient I f hf)) ((Ideal.Quotient.mkₐ R I.toIdeal) h) = (CommHopfAlgCat.Hom.hom f) h

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

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_liftQuotient {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : CategoryTheory.CategoryStruct.comp (mkQuotient H I) (liftQuotient I f hf) = f

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

theorem TauCeti.CommHopfAlgCat.liftQuotient_unique {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (g : quotient H I ⟶ K) (hg : CategoryTheory.CategoryStruct.comp (mkQuotient H I) g = f) : g = liftQuotient I f hf

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

theorem TauCeti.CommHopfAlgCat.liftQuotient_surjective_of_surjective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (hsurj : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (liftQuotient I f hf))

A surjective morphism remains surjective after factoring through a Hopf-ideal quotient.

noncomputable def TauCeti.CommHopfAlgCat.quotientIsoOfSurjective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (I : HopfIdeal R ↑K) : quotient H (I.comapOfSurjective (CommHopfAlgCat.Hom.hom f) hf) ≅ quotient K I

A surjective morphism of commutative Hopf algebras identifies the quotient by the inverse-image Hopf ideal with the corresponding quotient of the target.

Equations

• TauCeti.CommHopfAlgCat.quotientIsoOfSurjective f hf I = TauCeti.CommHopfAlgCat.quotientIsoOfSurjectiveAux✝ f hf I (I.comapOfSurjective (CommHopfAlgCat.Hom.hom f) hf) ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfSurjective_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (I : HopfIdeal R ↑K) : CategoryTheory.CategoryStruct.comp (mkQuotient H (I.comapOfSurjective (CommHopfAlgCat.Hom.hom f) hf)) (quotientIsoOfSurjective f hf I).hom = CategoryTheory.CategoryStruct.comp f (mkQuotient K I)

The forward quotient isomorphism induced by a surjective morphism commutes with the quotient morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientIsoOfSurjective_hom_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (I : HopfIdeal R ↑K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (quotientIsoOfSurjective f hf I).hom) ((Ideal.Quotient.mk (I.comapOfSurjective (CommHopfAlgCat.Hom.hom f) hf).toIdeal) x) = (Ideal.Quotient.mkₐ R I.toIdeal) ((CommHopfAlgCat.Hom.hom f) x)

The forward quotient isomorphism induced by a surjective morphism evaluates on quotient classes by applying the morphism before taking the target quotient.

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_eqToHom {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I J : HopfIdeal R ↑H} (hIJ : I = J) : CategoryTheory.CategoryStruct.comp (mkQuotient H J) (CategoryTheory.eqToHom ⋯) = mkQuotient H I

Transporting the quotient object along an equality of Hopf ideals transports its quotient morphism. This is the identity that lets an automorphism preserving a Hopf ideal be compared with the isomorphism it induces on the quotient.

noncomputable def TauCeti.CommHopfAlgCat.quotientIsoOfIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) : quotient H (I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯) ≅ quotient K I

An isomorphism of commutative Hopf algebras induces an isomorphism from the quotient by the inverse-image Hopf ideal to the corresponding quotient of the target.

Equations

• TauCeti.CommHopfAlgCat.quotientIsoOfIso e I = TauCeti.CommHopfAlgCat.quotientIsoOfSurjective e.hom ⋯ I

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfIso_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) : CategoryTheory.CategoryStruct.comp (mkQuotient H (I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯)) (quotientIsoOfIso e I).hom = CategoryTheory.CategoryStruct.comp e.hom (mkQuotient K I)

The forward map of the quotient isomorphism commutes with the quotient morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfIso_inv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) : CategoryTheory.CategoryStruct.comp (mkQuotient K I) (quotientIsoOfIso e I).inv = CategoryTheory.CategoryStruct.comp e.inv (mkQuotient H (I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯))

The inverse map of the quotient isomorphism commutes with the quotient morphisms.

theorem TauCeti.HopfIdeal.comapOfSurjective_eq_of_hom_le_of_inv_le {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (e : H ≅ H) (I : HopfIdeal R ↑H) (hhom : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ ≤ I) (hinv : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.inv) ⋯ ≤ I) : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = I

A Hopf ideal is invariant under an ambient automorphism if both the automorphism and its inverse pull it into itself.

noncomputable def TauCeti.CommHopfAlgCat.quotientIsoOfComapEq {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) {J : HopfIdeal R ↑H} (hI : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = J) : quotient H J ≅ quotient K I

An isomorphism e : H ≅ K that pulls the Hopf ideal I of K back to the Hopf ideal J of H induces an isomorphism of the quotients. For K = H and J = I this is the automorphism of the quotient induced by an ideal-preserving automorphism.

Equations

• TauCeti.CommHopfAlgCat.quotientIsoOfComapEq e I hI = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.CommHopfAlgCat.quotientIsoOfIso e I

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfComapEq_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) {J : HopfIdeal R ↑H} (hI : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = J) : CategoryTheory.CategoryStruct.comp (mkQuotient H J) (quotientIsoOfComapEq e I hI).hom = CategoryTheory.CategoryStruct.comp e.hom (mkQuotient K I)

The quotient isomorphism induced by an ideal-matching ambient isomorphism commutes with the quotient morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfComapEq_inv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) {J : HopfIdeal R ↑H} (hI : I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = J) : CategoryTheory.CategoryStruct.comp (mkQuotient K I) (quotientIsoOfComapEq e I hI).inv = CategoryTheory.CategoryStruct.comp e.inv (mkQuotient H J)

The inverse of the quotient isomorphism induced by an ideal-matching ambient isomorphism commutes with the quotient morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientIsoOfIso_hom_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (quotientIsoOfIso e I).hom) ((Ideal.Quotient.mk (I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯).toIdeal) x) = (Ideal.Quotient.mkₐ R I.toIdeal) ((CommHopfAlgCat.Hom.hom e.hom) x)

The forward quotient isomorphism induced by an ambient isomorphism evaluates on quotient classes by applying the ambient isomorphism before taking the target quotient.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientIsoOfIso_inv_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K) (y : ↑K) : (CommHopfAlgCat.Hom.hom (quotientIsoOfIso e I).inv) ((Ideal.Quotient.mk I.toIdeal) y) = (Ideal.Quotient.mkₐ R (I.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯).toIdeal) ((CommHopfAlgCat.Hom.hom e.inv) y)

The inverse quotient isomorphism induced by an ambient isomorphism evaluates on quotient classes by applying the inverse ambient isomorphism before taking the source quotient.

noncomputable def TauCeti.CommHopfAlgCat.quotientBotIso {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : quotient H ⊥ ≅ H

Quotienting a commutative Hopf algebra by the zero Hopf ideal gives an isomorphic object of CommHopfAlgCat.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientBotIso_hom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (quotientBotIso H).hom = liftQuotient ⊥ (CategoryTheory.CategoryStruct.id H) ⋯

The forward map of the quotient-by-zero isomorphism is the lift of the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientBotIso_inv {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (quotientBotIso H).inv = mkQuotient H ⊥

The inverse map of the quotient-by-zero isomorphism is the quotient morphism.

noncomputable def TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) : quotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf) ≅ K

A surjective morphism of commutative Hopf algebras identifies the quotient by its Hopf-ideal kernel with its target.

Equations

• TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso f hf = CommHopfAlgCat.isoMk (TauCeti.HopfIdeal.kerLiftBialgEquiv (CommHopfAlgCat.Hom.hom f) hf)

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientKerOfSurjectiveIso_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) : CategoryTheory.CategoryStruct.comp (mkQuotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)) (quotientKerOfSurjectiveIso f hf).hom = f

The kernel quotient isomorphism identifies the quotient morphism with the original surjective morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientKerOfSurjectiveIso_hom_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {Z : CommHopfAlgCat R} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (mkQuotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)) (CategoryTheory.CategoryStruct.comp (quotientKerOfSurjectiveIso f hf).hom h) = CategoryTheory.CategoryStruct.comp f h

The kernel quotient isomorphism identifies the quotient morphism with the original surjective morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.comp_quotientKerOfSurjectiveIso_inv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) : CategoryTheory.CategoryStruct.comp f (quotientKerOfSurjectiveIso f hf).inv = mkQuotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)

The inverse of the kernel quotient isomorphism identifies the original surjective morphism with the quotient morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.comp_quotientKerOfSurjectiveIso_inv_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {Z : CommHopfAlgCat R} (h : quotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (quotientKerOfSurjectiveIso f hf).inv h) = CategoryTheory.CategoryStruct.comp (mkQuotient H (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)) h

The inverse of the kernel quotient isomorphism identifies the original surjective morphism with the quotient morphism.

noncomputable def TauCeti.CommHopfAlgCat.quotientIsoOfKerOfSurjectiveEq {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {I : HopfIdeal R ↑H} (hI : HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf = I) : quotient H I ≅ K

A surjective morphism of commutative Hopf algebras identifies the quotient by any Hopf ideal equal to its Hopf-ideal kernel with its target.

Equations

• TauCeti.CommHopfAlgCat.quotientIsoOfKerOfSurjectiveEq f hf hI = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso f hf

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfKerOfSurjectiveEq_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {I : HopfIdeal R ↑H} (hI : HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf = I) : CategoryTheory.CategoryStruct.comp (mkQuotient H I) (quotientIsoOfKerOfSurjectiveEq f hf hI).hom = f

The identification of a quotient by the kernel of a surjective morphism with its target identifies the quotient morphism with the original surjective morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientIsoOfKerOfSurjectiveEq_hom_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {I : HopfIdeal R ↑H} (hI : HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf = I) {Z : CommHopfAlgCat R} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (mkQuotient H I) (CategoryTheory.CategoryStruct.comp (quotientIsoOfKerOfSurjectiveEq f hf hI).hom h) = CategoryTheory.CategoryStruct.comp f h

The identification of a quotient by the kernel of a surjective morphism with its target identifies the quotient morphism with the original surjective morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.comp_quotientIsoOfKerOfSurjectiveEq_inv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {I : HopfIdeal R ↑H} (hI : HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf = I) : CategoryTheory.CategoryStruct.comp f (quotientIsoOfKerOfSurjectiveEq f hf hI).inv = mkQuotient H I

The inverse identification of a quotient by the kernel of a surjective morphism with its target identifies the original surjective morphism with the quotient morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.comp_quotientIsoOfKerOfSurjectiveEq_inv_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {I : HopfIdeal R ↑H} (hI : HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf = I) {Z : CommHopfAlgCat R} (h : quotient H I ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (quotientIsoOfKerOfSurjectiveEq f hf hI).inv h) = CategoryTheory.CategoryStruct.comp (mkQuotient H I) h

The inverse identification of a quotient by the kernel of a surjective morphism with its target identifies the original surjective morphism with the quotient morphism.

theorem TauCeti.CommHopfAlgCat.toIdeal_le_ker_mkQuotient_of_le {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (mkQuotient H J))).toRingHom

If I ≤ J, then the quotient map by J kills every element of I.

theorem TauCeti.CommHopfAlgCat.toIdeal_le_ker_of_mkQuotient_comp {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {g : quotient H I ⟶ K} {f : H ⟶ K} (hg : CategoryTheory.CategoryStruct.comp (mkQuotient H I) g = f) : I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom

A morphism out of H that factors through the quotient by I kills I.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.quotientMapOfLe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : quotient H I ⟶ quotient H J

The coordinate morphism H ⧸ I ⟶ H ⧸ J induced by an inclusion I ≤ J of Hopf ideals.

It is the unique morphism out of H ⧸ I whose composite with H ⟶ H ⧸ I is the quotient map H ⟶ H ⧸ J.

Equations

• TauCeti.CommHopfAlgCat.quotientMapOfLe H hIJ = TauCeti.CommHopfAlgCat.liftQuotient I (TauCeti.CommHopfAlgCat.mkQuotient H J) ⋯

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_mk {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (h : ↑H) : (CommHopfAlgCat.Hom.hom (quotientMapOfLe H hIJ)) ((Ideal.Quotient.mkₐ R I.toIdeal) h) = (Ideal.Quotient.mkₐ R J.toIdeal) h

The quotient-to-quotient morphism sends the class of h modulo I to its class modulo J.

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_surjective {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (quotientMapOfLe H hIJ))

A quotient-to-quotient coordinate morphism induced by an inclusion of Hopf ideals is surjective.

@[simp]

theorem TauCeti.CommHopfAlgCat.kerOfSurjective_quotientMapOfLe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : HopfIdeal.kerOfSurjective (Bialgebra.Quotient.liftBialgHom I.toIdeal (Bialgebra.Quotient.mkBialgHom J.toIdeal) ⋯) ⋯ = J.map (Bialgebra.Quotient.mkBialgHom I.toIdeal)

The surjective kernel Hopf ideal of the induced map H ⧸ I ⟶ H ⧸ J is the image of J in H ⧸ I.

@[simp]

theorem TauCeti.CommHopfAlgCat.ker_quotientMapOfLe {k : Type u} [Field k] (H : CommHopfAlgCat k) {I J : HopfIdeal k ↑H} (hIJ : I ≤ J) : HopfIdeal.ker (Bialgebra.Quotient.liftBialgHom I.toIdeal (Bialgebra.Quotient.mkBialgHom J.toIdeal) ⋯) = J.map (Bialgebra.Quotient.mkBialgHom I.toIdeal)

Over a field, the kernel Hopf ideal of the induced map H ⧸ I ⟶ H ⧸ J is the image of J in H ⧸ I.

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientMapOfLe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : CategoryTheory.CategoryStruct.comp (mkQuotient H I) (quotientMapOfLe H hIJ) = mkQuotient H J

Composing the quotient map H ⟶ H ⧸ I with the quotient-to-quotient morphism for I ≤ J gives the quotient map H ⟶ H ⧸ J.

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientMapOfLe_assoc {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) {Z : CommHopfAlgCat R} (h : quotient H J ⟶ Z) : CategoryTheory.CategoryStruct.comp (mkQuotient H I) (CategoryTheory.CategoryStruct.comp (quotientMapOfLe H hIJ) h) = CategoryTheory.CategoryStruct.comp (mkQuotient H J) h

Composing the quotient map H ⟶ H ⧸ I with the quotient-to-quotient morphism for I ≤ J gives the quotient map H ⟶ H ⧸ J.

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_comp_liftQuotient_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {K : CommHopfAlgCat R} {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) (f : H ⟶ K) (hf : J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (g : quotient H I ⟶ K) (hg : CategoryTheory.CategoryStruct.comp (mkQuotient H I) g = f) : CategoryTheory.CategoryStruct.comp (quotientMapOfLe H hIJ) (liftQuotient J f hf) = g

A lift through the larger of two Hopf ideals is recognized by its precomposition with the quotient morphism. Composing H ⧸ I ⟶ H ⧸ J with the lift of f : H ⟶ K through H ⧸ J gives the unique morphism g : H ⧸ I ⟶ K with mkQuotient H I ≫ g = f.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_refl {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientMapOfLe H ⋯ = CategoryTheory.CategoryStruct.id (quotient H I)

The quotient-to-quotient morphism for I ≤ I is the identity morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_comp {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J K : HopfIdeal R ↑H} (hIJ : I ≤ J) (hJK : J ≤ K) : CategoryTheory.CategoryStruct.comp (quotientMapOfLe H hIJ) (quotientMapOfLe H hJK) = quotientMapOfLe H ⋯

Quotient-to-quotient morphisms compose along inclusions of Hopf ideals.

theorem TauCeti.CommHopfAlgCat.quotientMapOfLe_injective_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (quotientMapOfLe H hIJ)) ↔ I = J

The quotient-to-quotient morphism induced by an inclusion I ≤ J of Hopf ideals is injective exactly when I = J.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.quotient {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : FiniteTypeCommHopfAlgCat R

The quotient of a finite-type commutative Hopf algebra by a Hopf ideal, as a bundled finite-type commutative Hopf algebra.

Equations

• H.quotient I = { obj := TauCeti.CommHopfAlgCat.quotient H.obj I, property := ⋯ }

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.quotientBotIso {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : H.quotient ⊥ ≅ H

Quotienting a finite-type commutative Hopf algebra by the zero Hopf ideal gives an isomorphic finite-type commutative Hopf algebra.

Equations

• H.quotientBotIso = (TauCeti.finiteTypeCommHopfAlgProperty R).isoMk (TauCeti.CommHopfAlgCat.quotientBotIso H.obj)

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : H ⟶ H.quotient I

The quotient morphism H ⟶ H ⧸ I in FiniteTypeCommHopfAlgCat.

Equations

• H.mkQuotient I = CategoryTheory.ObjectProperty.homMk (TauCeti.CommHopfAlgCat.mkQuotient H.obj I)

theorem TauCeti.FiniteTypeCommHopfAlgCat.forget₂_commHopfAlgCat_map_mkQuotient {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).map (H.mkQuotient I) = CommHopfAlgCat.mkQuotient H.obj I

The finite-type quotient morphism forgets to the CommHopfAlgCat quotient morphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_hom_ext {R : Type u} [CommRing R] {H X : FiniteTypeCommHopfAlgCat R} {I : HopfIdeal R ↑H.obj} {f g : H.quotient I ⟶ X} (h : CategoryTheory.CategoryStruct.comp (H.mkQuotient I) f = CategoryTheory.CategoryStruct.comp (H.mkQuotient I) g) : f = g

Morphisms out of a finite-type Hopf-algebra quotient are determined by their composites with the quotient morphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_hom_ext_iff {R : Type u} [CommRing R] {H X : FiniteTypeCommHopfAlgCat R} {I : HopfIdeal R ↑H.obj} {f g : H.quotient I ⟶ X} : f = g ↔ CategoryTheory.CategoryStruct.comp (H.mkQuotient I) f = CategoryTheory.CategoryStruct.comp (H.mkQuotient I) g

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientBotIso_inv {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : H.quotientBotIso.inv = H.mkQuotient ⊥

The inverse map of the finite-type quotient-by-zero isomorphism is the quotient morphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_ker {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : RingHom.ker (↑(toBialgHom (H.mkQuotient I))).toRingHom = I.toIdeal

The kernel of the finite-type quotient morphism is the Hopf ideal being quotiented by.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_eq_zero_iff {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) (h : ↑H.obj) : (toBialgHom (H.mkQuotient I)) h = 0 ↔ h ∈ I.toIdeal

An element maps to zero in the finite-type quotient exactly when it belongs to the Hopf ideal.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.quotientIsoOfIso {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K.obj) : H.quotient (I.comapOfSurjective (toBialgHom e.hom) ⋯) ≅ K.quotient I

An isomorphism of finite-type commutative Hopf algebras induces an isomorphism from the quotient by the inverse-image Hopf ideal to the corresponding quotient of the target.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.FiniteTypeCommHopfAlgCat.minimal_quotientProperty_comapOfIso {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat R)) [P.IsClosedUnderIsomorphisms] (I : HopfIdeal R ↑K.obj) (hI : Minimal (fun (J : HopfIdeal R ↑K.obj) => P (K.quotient J)) I) (e : H ≅ K) : Minimal (fun (J : HopfIdeal R ↑H.obj) => P (H.quotient J)) (I.comapOfSurjective (toBialgHom e.hom) ⋯)

If I is a minimal Hopf ideal of K among those whose quotient satisfies the isomorphism-closed property P, then its inverse image along an isomorphism e : H ≅ K is a minimal such Hopf ideal of H.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_eqToHom {R : Type u} [CommRing R] {H : FiniteTypeCommHopfAlgCat R} {I J : HopfIdeal R ↑H.obj} (hIJ : I = J) : CategoryTheory.CategoryStruct.comp (H.mkQuotient J) (CategoryTheory.eqToHom ⋯) = H.mkQuotient I

Transporting a finite-type quotient object along an equality of Hopf ideals transports its quotient morphism.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_quotientIsoOfIso_hom {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K.obj) : CategoryTheory.CategoryStruct.comp (H.mkQuotient (I.comapOfSurjective (toBialgHom e.hom) ⋯)) (quotientIsoOfIso e I).hom = CategoryTheory.CategoryStruct.comp e.hom (K.mkQuotient I)

The forward finite-type quotient isomorphism commutes with the quotient morphisms.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_quotientIsoOfIso_inv {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (e : H ≅ K) (I : HopfIdeal R ↑K.obj) : CategoryTheory.CategoryStruct.comp (K.mkQuotient I) (quotientIsoOfIso e I).inv = CategoryTheory.CategoryStruct.comp e.inv (H.mkQuotient (I.comapOfSurjective (toBialgHom e.hom) ⋯))

The inverse finite-type quotient isomorphism commutes with the quotient morphisms.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.liftQuotient {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (I : HopfIdeal R ↑H.obj) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(toBialgHom f)).toRingHom) : H.quotient I ⟶ K

A morphism of finite-type commutative Hopf algebras out of H which kills a Hopf ideal factors through the quotient object.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.liftQuotient I f hf = CategoryTheory.ObjectProperty.homMk (TauCeti.CommHopfAlgCat.liftQuotient I f.hom hf)

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientBotIso_hom {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : H.quotientBotIso.hom = liftQuotient ⊥ (CategoryTheory.CategoryStruct.id H) ⋯

The forward map of the finite-type quotient-by-zero isomorphism is the lift of the identity.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_liftQuotient {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (I : HopfIdeal R ↑H.obj) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(toBialgHom f)).toRingHom) : CategoryTheory.CategoryStruct.comp (H.mkQuotient I) (liftQuotient I f hf) = f

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

theorem TauCeti.FiniteTypeCommHopfAlgCat.liftQuotient_unique {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (I : HopfIdeal R ↑H.obj) (f : H ⟶ K) (hf : I.toIdeal ≤ RingHom.ker (↑(toBialgHom f)).toRingHom) (g : H.quotient I ⟶ K) (hg : CategoryTheory.CategoryStruct.comp (H.mkQuotient I) g = f) : g = liftQuotient I f hf

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) : H.quotient I ⟶ H.quotient J

The finite-type coordinate morphism H ⧸ I ⟶ H ⧸ J induced by an inclusion I ≤ J of Hopf ideals.

Equations

• H.quotientMapOfLe hIJ = CategoryTheory.ObjectProperty.homMk (TauCeti.CommHopfAlgCat.quotientMapOfLe H.obj hIJ)

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe_mk {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) (h : ↑H.obj) : (toBialgHom (H.quotientMapOfLe hIJ)) ((Ideal.Quotient.mkₐ R I.toIdeal) h) = (Ideal.Quotient.mkₐ R J.toIdeal) h

The finite-type quotient-to-quotient morphism sends the class of h modulo I to its class modulo J.

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe_surjective {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) : Function.Surjective ⇑(toBialgHom (H.quotientMapOfLe hIJ))

A finite-type quotient-to-quotient coordinate morphism induced by an inclusion of Hopf ideals is surjective.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_quotientMapOfLe {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) : CategoryTheory.CategoryStruct.comp (H.mkQuotient I) (H.quotientMapOfLe hIJ) = H.mkQuotient J

Composing the finite-type quotient map H ⟶ H ⧸ I with the quotient-to-quotient morphism for I ≤ J gives the quotient map H ⟶ H ⧸ J.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mkQuotient_comp_quotientMapOfLe_assoc {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) {Z : FiniteTypeCommHopfAlgCat R} (h : H.quotient J ⟶ Z) : CategoryTheory.CategoryStruct.comp (H.mkQuotient I) (CategoryTheory.CategoryStruct.comp (H.quotientMapOfLe hIJ) h) = CategoryTheory.CategoryStruct.comp (H.mkQuotient J) h

Composing the finite-type quotient map H ⟶ H ⧸ I with the quotient-to-quotient morphism for I ≤ J gives the quotient map H ⟶ H ⧸ J.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe_refl {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : H.quotientMapOfLe ⋯ = CategoryTheory.CategoryStruct.id (H.quotient I)

The finite-type quotient-to-quotient morphism for I ≤ I is the identity morphism.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.quotientMapOfLe_comp {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) {I J K : HopfIdeal R ↑H.obj} (hIJ : I ≤ J) (hJK : J ≤ K) : CategoryTheory.CategoryStruct.comp (H.quotientMapOfLe hIJ) (H.quotientMapOfLe hJK) = H.quotientMapOfLe ⋯

Finite-type quotient-to-quotient morphisms compose along inclusions of Hopf ideals.