Kernels of isogenies

The kernel of an isogeny of affine group schemes is finite and faithfully flat over the base. The kernel square is a pullback of the isogeny along the identity section, so each of finiteness, flatness, and surjectivity is inherited by the structural morphism of the kernel: the represented kernel is itself an isogeny over the base.

Over a Noetherian base ring, the kernel of a central isogeny is therefore a finite locally free bicommutative Hopf algebra, the shape required by Cartier duality: its coordinate ring is finite and faithfully flat over the base, hence finite projective.

Main declarations

• TauCeti.CommHopfAlgCat.IsIsogeny.isIsogeny_kernelSpec_to_trivial: the structural morphism from the represented kernel to the trivial group scheme is an isogeny.
• TauCeti.CommHopfAlgCat.IsCentralIsogeny.kernelFiniteLocallyFree: over a Noetherian base ring, the kernel of a central isogeny as a finite locally free bicommutative Hopf algebra.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 4.
• J. S. Milne, Algebraic Groups (2017), Proposition 2.21.

theorem TauCeti.CommHopfAlgCat.IsIsogeny.isIsogeny_kernelSpec_to_trivial {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) : GroupScheme.IsIsogeny 0

The structural morphism from the represented kernel of an isogeny to the trivial group scheme is itself an isogeny. Equivalently, the kernel is a finite faithfully flat group scheme over the base.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.IsCentralIsogeny.kernelFiniteLocallyFree {R : Type u} [CommRing R] [IsNoetherianRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) : FiniteLocallyFreeBicommutativeHopfAlgCat R

Over a Noetherian base ring, package the kernel of a central isogeny as a finite locally free bicommutative Hopf algebra, ready for Cartier duality. The kernel coordinate ring is finite and faithfully flat over the base, hence finite projective.

Equations

• hf.kernelFiniteLocallyFree = TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.of R (↑K ⧸ (TauCeti.CommHopfAlgCat.kernelHopfIdeal f).toIdeal)