Image factorizations of commutative Hopf-algebra morphisms over a field

For a morphism f : H ⟶ K of commutative Hopf algebras over a field, this file packages the canonical factorization through the quotient by its kernel Hopf ideal:

H ⟶ H / ker f ⟶ K

The first morphism is surjective and an epimorphism, while the second is injective and a monomorphism. Geometrically, this quotient-by-the-ring-kernel construction motivates the coordinate algebra of the scheme-theoretic image of the represented affine-group morphism; that geometric compatibility is not formalized here.

Main declarations

• TauCeti.CommHopfAlgCat.image: the quotient Hopf algebra by the kernel of a morphism.
• TauCeti.CommHopfAlgCat.mkImage: the quotient morphism onto the image quotient.
• TauCeti.CommHopfAlgCat.imageι: the injective factor from the image quotient.
• TauCeti.CommHopfAlgCat.mkImage_comp_imageι: the factorization identity.

References

• J. S. Milne, Algebraic Groups (2017), §5.a.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §§15--16.
• Mathlib's AlgebraicGeometry.specTargetImage, specTargetImageRingHom, and specTargetImageFactorization in Mathlib.AlgebraicGeometry.AffineScheme, whose affine scheme-theoretic image construction this Hopf-level quotient factorization mirrors.

This is image infrastructure for Layer 3, "Subgroups, quotients, components", of the ReductiveGroups roadmap.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.image {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : CommHopfAlgCat k

The quotient Hopf algebra by the kernel of a morphism.

Equations

• TauCeti.CommHopfAlgCat.image f = TauCeti.CommHopfAlgCat.quotient H (TauCeti.HopfIdeal.ker (CommHopfAlgCat.Hom.hom f))

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.mkImage {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : H ⟶ image f

The quotient morphism onto the image quotient.

Equations

• TauCeti.CommHopfAlgCat.mkImage f = TauCeti.CommHopfAlgCat.mkQuotient H (TauCeti.HopfIdeal.ker (CommHopfAlgCat.Hom.hom f))

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.imageι {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : image f ⟶ K

The injective factor from the image quotient into the codomain.

Equations

• TauCeti.CommHopfAlgCat.imageι f = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)) f ⋯

theorem TauCeti.CommHopfAlgCat.mkImage_comp_imageι {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (mkImage f) (imageι f) = f

A morphism factors through its image quotient.

theorem TauCeti.CommHopfAlgCat.mkImage_comp_imageι_assoc {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) {Z : CommHopfAlgCat k} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (mkImage f) (CategoryTheory.CategoryStruct.comp (imageι f) h) = CategoryTheory.CategoryStruct.comp f h

A morphism factors through its image quotient.

theorem TauCeti.CommHopfAlgCat.mkImage_apply {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (mkImage f)) x = (Ideal.Quotient.mkₐ k (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal) x

The quotient morphism onto the image evaluates to the quotient class.

theorem TauCeti.CommHopfAlgCat.imageι_mk {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (imageι f)) ((Ideal.Quotient.mkₐ k (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal) x) = (CommHopfAlgCat.Hom.hom f) x

The injective factor evaluates on a quotient class as the original morphism.

theorem TauCeti.CommHopfAlgCat.imageι_mkImage_apply {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (imageι f)) ((CommHopfAlgCat.Hom.hom (mkImage f)) x) = (CommHopfAlgCat.Hom.hom f) x

The pointwise form of the factorization through the image quotient.

theorem TauCeti.CommHopfAlgCat.mkImage_surjective {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (mkImage f))

The quotient morphism onto the image is surjective.

theorem TauCeti.CommHopfAlgCat.imageι_injective {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (imageι f))

The factor from the image quotient into the codomain is injective.

theorem TauCeti.CommHopfAlgCat.imageι_finiteType {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) [Algebra.FiniteType k ↑K] : (↑(CommHopfAlgCat.Hom.hom (imageι f))).FiniteType

If the source affine group has finite-type coordinate algebra, its canonical morphism onto the scheme-theoretic image is of finite type.

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_imageι {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : kernelHopfIdeal (imageι f) = kernelHopfIdeal f

Passing from a homomorphism to its scheme-theoretic image does not change its kernel closed subgroup, including the possibly nonreduced scheme structure.

instance TauCeti.CommHopfAlgCat.imageι_mono {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : CategoryTheory.Mono (imageι f)

instance TauCeti.CommHopfAlgCat.mkImage_epi {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : CategoryTheory.Epi (mkImage f)