Finite generation of Hopf subalgebras

Every finite subset of a commutative Hopf algebra over a field lies in the image of an injective morphism from a finite-type commutative Hopf algebra. A finite-dimensional regular subcomodule containing the subset gives a representation; the image of its coordinate morphism supplies the finite-type algebra.

If a coordinate morphism lands in a Noetherian algebra, a finite-type part of its source already detects its entire scheme-theoretic kernel. When the codomain is geometrically reduced and finite type, the existing faithful-flatness theorem makes this finite-type approximation surjective onto an injective morphism's source. Consequently every Hopf subalgebra of a geometrically reduced finite-type commutative Hopf algebra is finite type. This supplies finite generation of coordinate algebras for normal affine-group quotients.

The construction reuses Comodule.coordinateBialgHom and the finite-dimensional subcoalgebra argument in Comodule.exists_coordinateBialgHom_surjective.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§3.3 and 16.3.
• J. S. Milne, Algebraic Groups (2017), §4.a and §5.c.

theorem CommHopfAlgCat.exists_finiteType_injective_range_contains {k : Type u} [Field k] (H : CommHopfAlgCat k) (s : Set ↑H) (hs : s.Finite) : ∃ (L : CommHopfAlgCat k) (_ : Algebra.FiniteType k ↑L) (i : L ⟶ H), Function.Injective ⇑(Hom.hom i) ∧ s ⊆ ↑(↑(Hom.hom i)).range

Every finite subset of a commutative Hopf algebra over a field lies in the image of an injective coordinate morphism from a finite-type commutative Hopf algebra. No finite-generation hypothesis on the ambient algebra is required.

theorem CommHopfAlgCat.exists_finiteType_injective_kernelHopfIdeal_eq {k : Type u} [Field k] {H K : CommHopfAlgCat k} [IsNoetherianRing ↑K] (f : H ⟶ K) : ∃ (L : CommHopfAlgCat k) (_ : Algebra.FiniteType k ↑L) (i : L ⟶ H), Function.Injective ⇑(Hom.hom i) ∧ TauCeti.CommHopfAlgCat.kernelHopfIdeal (CategoryTheory.CategoryStruct.comp i f) = TauCeti.CommHopfAlgCat.kernelHopfIdeal f

A finite-type part of the target of a homomorphism from an affine group with Noetherian coordinate ring detects the entire scheme-theoretic kernel. In coordinates, precomposing with an injective morphism from a finite-type Hopf algebra leaves kernelHopfIdeal unchanged.

theorem CommHopfAlgCat.finiteType_of_injective {k : Type u} [Field k] {H K : CommHopfAlgCat k} [Algebra.FiniteType k ↑K] [Algebra.IsGeometricallyReduced k ↑K] (f : H ⟶ K) (hf : Function.Injective ⇑(Hom.hom f)) : Algebra.FiniteType k ↑H

A commutative Hopf algebra that embeds in a geometrically reduced finite-type commutative Hopf algebra over a field is itself finite type.