Normal scheme-theoretic images

Let f : H →ₐc[k] K be a morphism of commutative Hopf algebras over a commutative ring, representing a homomorphism from Spec K to Spec H. Its scheme-theoretic image has coordinate algebra H / ker f. This file proves that the image is normal when ambient conjugation admits an algebra-homomorphic lift along the coordinate map.

In coordinate algebras, such a lift is an algebra homomorphism

α♯ : K →ₐ[k] H ⊗[k] K

such that (id ⊗ f) ∘ conj♯ = α♯ ∘ f. If f(x) = 0, equivariance says that (id ⊗ f)(conj♯(x)) = 0. Flatness of H identifies this kernel with H ⊗ ker f, which is precisely normality of the image Hopf ideal. Flatness of K and H / ker f supplies that Hopf ideal. Over a field all these flatness conditions are automatic.

Main declarations

• TauCeti.HopfIdeal.IsNormal.comap_of_injective: inverse image along an injective bialgebra morphism preserves normality when the source and the relevant quotients are flat.
• TauCeti.HopfIdeal.isNormal_ker_of_conjugation_equivariant: the scheme-theoretic image of an equivariant affine-group homomorphism is normal.

References

• J. S. Milne, Algebraic Groups (2017), §5.a and §10.20.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §§16--17.
• The tensor-kernel identity is Algebra.TensorProduct.lTensor_ker_of_flat from TauCeti.RingTheory.Flat.TensorProduct, using Mathlib's Module.Flat.ker_lTensor_eq.

Applied to multiplication from the semidirect product of two normal closed subgroups, the lifted action is simultaneous ambient conjugation and the image is their normal product.

theorem TauCeti.HopfIdeal.IsNormal.comap_of_injective {k : Type u} [CommRing k] {H : Type v} {K : Type w} [CommRing H] [CommRing K] [HopfAlgebra k H] [HopfAlgebra k K] [Module.Flat k H] {I : HopfIdeal k K} (hI : I.IsNormal) (f : H →ₐc[k] K) (hf : Function.Injective ⇑f) [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] : (I.comap f).IsNormal

Pulling a normal Hopf ideal back along an injective bialgebra morphism preserves normality when the source, quotient, and preimage quotient are flat over the base.

Contravariantly, the scheme-theoretic image of a normal closed affine subgroup under a surjective affine-group morphism is normal. Injectivity is used only to reflect vanishing after tensoring the first coordinate map.

theorem TauCeti.HopfIdeal.isNormal_ker_of_conjugation_equivariant {k : Type u} [CommRing k] {H : Type v} {K : Type w} [CommRing H] [CommRing K] [HopfAlgebra k H] [HopfAlgebra k K] [Module.Flat k H] (f : H →ₐc[k] K) [Module.Flat k K] [Module.Flat k (H ⧸ RingHom.ker ↑f)] (conjLift : K →ₐ[k] TensorProduct k H K) (hequiv : (Algebra.TensorProduct.map (AlgHom.id k H) ↑f).comp HopfAlgebra.conjugationAlgHom = conjLift.comp ↑f) : (ker f).IsNormal

An equivariant affine-group homomorphism has normal scheme-theoretic image.

The morphism f : H →ₐc[k] K is contravariant: it represents a homomorphism from the affine group with coordinate algebra K into the ambient group with coordinate algebra H. The algebra homomorphism conjLift lifts ambient conjugation along f; no action-law hypotheses are required. Consequently the kernel Hopf ideal, and hence the scheme-theoretic image Spec (H / ker f), is normal. The source, codomain, and kernel quotient are assumed flat over the base.