Hopf-ideal quotients as categorical subgroup inclusions

A morphism of commutative Hopf algebras represents a morphism in the opposite category of commutative algebras. In particular, the quotient map H ⟶ H/I represents the closed-subgroup inclusion Spec(H/I) ⟶ Spec H. This file supplies that normality-free categorical inclusion and its monomorphism and monoid-homomorphism instances.

Main declarations

• TauCeti.CommHopfAlgCat.quotientGrpObjInclusion: the categorical closed-subgroup inclusion represented by a Hopf-ideal quotient.
• TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_mono: the inclusion is a monomorphism.
• TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_isMonHom: the inclusion preserves the group-object multiplication.

References

This is the categorical form of the Layer 3 Hopf-ideal/closed-subgroup dictionary in the ReductiveGroups roadmap. It uses Mathlib's commHopfAlgCatEquivCogrpCommAlgCat and CategoryTheory.op_mono_of_epi together with the quotient API in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Basic.

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

The categorical closed-subgroup inclusion represented contravariantly by the quotient map H ⟶ H/I.

Equations

• TauCeti.CommHopfAlgCat.quotientGrpObjInclusion H I = TauCeti.CommHopfAlgCat.grpObjMap (TauCeti.CommHopfAlgCat.mkQuotient H I)

theorem TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientGrpObjInclusion H I = grpObjMap (mkQuotient H I)

The categorical quotient inclusion is represented by the group-object map induced by the coordinate quotient morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_unop {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : (quotientGrpObjInclusion H I).unop = CommAlgCat.ofHom ↑(CommHopfAlgCat.Hom.hom (mkQuotient H I))

The categorical quotient inclusion is the opposite of the coordinate quotient map.

instance TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_isMonHom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : CategoryTheory.IsMonHom (quotientGrpObjInclusion H I)

A quotient group-object inclusion preserves multiplication.

instance TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_mono {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : CategoryTheory.Mono (quotientGrpObjInclusion H I)

A quotient group-object inclusion is a monomorphism.