Finite locally free commutative group schemes are killed by their rank

Let G be a finite locally free commutative group scheme over an arbitrary scheme S, of constant rank n. Then every point of G is killed by n: for every scheme X over S and every x : X ⟶ G over S, the n-th power of x in the group of X-valued points is the unit. This is Deligne's theorem. It is what makes a point of exact order n of an elliptic curve an n-torsion point, and the kernel of an isogeny of degree n a subgroup killed by n.

The affine case is TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk, stated for a commutative and cocommutative Hopf algebra which is finite flat of constant stalk rank. Over Spec R, the group scheme G is the Hopf spectrum of its coordinate Hopf algebra (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.hopfSpecCoordinateHopfAlgebraIso), whose local rank is the rank of G (finrank_eq_rankAtStalk_coordinateHopfAlgebra), and Mathlib's AlgebraicGeometry.Spec.mapMulEquiv identifies the points of a Hopf spectrum with the convolution group, so every point of the Hopf spectrum is killed by n. Over a general base, it suffices to show that the identity of G is killed by n. This is checked on the cover of G by its base changes to the affine opens of S: base change is a monoidal functor, so it commutes with powers in the groups of points.

Main results

• TauCeti.AlgebraicGeometry.Spec.pow_eq_one_of_rankAtStalk: the Hopf spectrum of a commutative and cocommutative Hopf algebra which is finite flat of constant stalk rank n is killed by n.
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank: a finite locally free commutative group scheme of constant rank n is killed by n.
• TauCeti.GroupScheme.pow_eq_one_of_finrank_of_mono: a finite locally free subgroup of constant rank n in a commutative group scheme is killed by n after its inclusion.

References

• J. Tate and F. Oort, Group schemes of prime order, Ann. Sci. École Norm. Sup. (4) 3 (1970), 1–21, §1.
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.12.

theorem TauCeti.AlgebraicGeometry.Spec.pow_eq_one_of_rankAtStalk {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [Module.Finite R H] [Module.Flat R H] {n : ℕ} (hn : ∀ (p : PrimeSpectrum R), Module.rankAtStalk H p = n) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)} (x : X ⟶ (AlgebraicGeometry.Spec ↧H).asOver (AlgebraicGeometry.Spec ↧R)) : x ^ n = 1

Every point of the Hopf spectrum of a commutative and cocommutative Hopf algebra which is finite flat of constant stalk rank n is killed by n: for every scheme X over Spec R and every x : X ⟶ Spec H over Spec R, the n-th power of x in the group of X-valued points is the unit.

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) {n : ℕ} (hn : ∀ (s : ↥S), AlgebraicGeometry.Scheme.Hom.finrank G.structureMap s = n) {X : CategoryTheory.Over S} (x : X ⟶ G.toOver) : x ^ n = 1

Deligne's theorem. Let G be a finite locally free commutative group scheme over S whose rank is n at every point of S. Then every point x : X ⟶ G over S is killed by n: its n-th power in the group of X-valued points of G is the unit.

theorem TauCeti.GroupScheme.pow_eq_one_of_finrank_of_mono {S X Y : AlgebraicGeometry.Scheme} {p : X ⟶ S} {q : Y ⟶ S} [CategoryTheory.GrpObj (CategoryTheory.Over.mk p)] [CategoryTheory.GrpObj (CategoryTheory.Over.mk q)] [CategoryTheory.IsCommMonObj (CategoryTheory.Over.mk q)] (i : CategoryTheory.Over.mk p ⟶ CategoryTheory.Over.mk q) [CategoryTheory.IsMonHom i] [CategoryTheory.Mono i] {n : ℕ} (hfinite : AlgebraicGeometry.IsFinite p) (hflat : AlgebraicGeometry.Flat p) (hlfp : AlgebraicGeometry.LocallyOfFinitePresentation p) (hn : ∀ (s : ↥S), AlgebraicGeometry.Scheme.Hom.finrank p s = n) : i ^ n = 1

Let i : H ⟶ G be a monomorphism of group schemes into a commutative group scheme. If H is finite locally free of constant rank n, then the point of G given by i is killed by n. This is the form of Deligne's rank theorem used to place finite locally free subgroup schemes inside torsion subgroup schemes.