Finite locally free commutative group schemes are killed by their rank

Let H be a commutative and cocommutative Hopf algebra over a commutative ring R, so that Spec H is a commutative affine group scheme over R whose group of A-valued points is the convolution group WithConv (H →ₐ[R] A). If H is finite projective over R of constant rank n, that is, Spec H is a finite locally free commutative group scheme of rank n, then every point is killed by n: x ^ n = 1 for every commutative R-algebra A and every x : WithConv (H →ₐ[R] A). This is Deligne's theorem. It is the input which turns a point of exact order n of an elliptic curve into an n-torsion point, and which makes the factorisation construction of dual isogenies possible.

Main results

• TauCeti.AlgHom.convPow_finrank_eq_one: when H is free of finite rank over R, every point is killed by Module.finrank R H.
• TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk: when H is finite projective over R and its rank at every prime is n, every point is killed by n.

Implementation notes

The free case is the norm argument of Deligne, as presented by Tate and Oort. The convolution algebra of linear maps H →ₗ[R] B plays the role of the coordinate ring of the Cartier dual with coefficients in B. For B = H and B' = H ⊗[R] H, a basis of H over R makes the convolution algebra of H →ₗ[R] B' free of rank n over that of H →ₗ[R] B, so it has a norm. Write ι₁ and ι₂ for the two inclusions H → H ⊗[R] H. The shear automorphism a ⊗ b ↦ (a ⊗ 1) Δ b of H ⊗[R] H over its left factor preserves norms and sends ι₂ to Δ = ι₁ * ι₂, where ι₁ comes from the identity of H. Taking norms gives N(ι₂) = id ^ n * N(ι₂), and ι₂ is a unit, so id ^ n = 1. The universal point id then controls every point. The locally free case follows by checking the resulting identity of elements of H after localizing at every maximal ideal of R.

References

• J. Tate and F. Oort, Group schemes of prime order, Ann. Sci. École Norm. Sup. (4) 3 (1970), 1–21, §1.
• J. Tate, Finite flat group schemes, in Modular Forms and Fermat's Last Theorem, Springer, 1997.

theorem TauCeti.AlgHom.convPow_finrank_eq_one {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [Module.Free R H] [Module.Finite R H] {A : Type u_3} [CommSemiring A] [Algebra R A] (x : WithConv (H →ₐ[R] A)) : x ^ Module.finrank R H = 1

Deligne's theorem, free case. Every point of a commutative and cocommutative Hopf algebra which is free of finite rank n over R is killed by n.

theorem TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [Module.Finite R H] [Module.Projective R H] {n : ℕ} (hn : ∀ (p : PrimeSpectrum R), Module.rankAtStalk H p = n) {A : Type u_3} [CommSemiring A] [Algebra R A] (x : WithConv (H →ₐ[R] A)) : x ^ n = 1

Deligne's theorem. Every point of a commutative and cocommutative Hopf algebra which is finite projective of constant rank n over R is killed by n.