Is a finite locally free group scheme killed by its order?

What is the conjecture

Let $G$ be a finite locally free group scheme of rank $n$ over a base scheme $S$, and let
$[n] : G \to G$ be the $n$-th power map. Lagrange's theorem says that a finite group of order $n$
satisfies $g^n = 1$, and Grothendieck asked whether the same holds for group schemes: does $[n]$
factor through the unit section?

Two cases are known to be affirmative:

• over a reduced base (SGA 3, Exp. VII$_A$, Prop. 8.5 for a field and Cor. 8.5.2 in general);
• for commutative $G$ over an arbitrary base, by a theorem of Deligne (1969).

The general case was open for sixty years. It has a negative answer: there is a group scheme of
rank $4$, over a finite non-reduced ring, whose fourth power map is not trivial (its eighth power
map is). The counterexample is in Mathlib as Counterexamples/GrothendieckPower.lean.

What remains open is the refinement: for each $n$, what is the least $m$ such that every finite
locally free group scheme of rank $n$ over every base is killed by $m$? Grothendieck's question
was whether this optimal exponent is $n$; it is not, already for $n = 4$.

Sources:

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exp. VIII, Rem. 7.3.1 (the
  question) and Exp. VII$_A$, Prop. 8.5, Cor. 8.5.2, Rem. 8.5.3 (the known cases);
  re-edition at https://webusers.imj-prg.fr/~patrick.polo/SGA3/
• R. Schoof, Is a finite locally free group scheme killed by its order?, in Open Problems in
  Arithmetic Algebraic Geometry, ALM 46, Int. Press 2019,
  https://reneschoof.github.io/schoof_oortAAG.pdf
• J. Tate and F. Oort, Group schemes of prime order, Ann. Sci. ENS 3 (1970), 1-21;
  p. 4 for Deligne's theorem, p. 5 for the remark that the general question was open
• Mathlib, A finite free group scheme of rank four that is not killed by four,
  https://leanprover-community.github.io/mathlib4_docs/Counterexamples/GrothendieckPower.html

Prerequisites needed

Everything needed is in Mathlib: HopfAlgebra, the convolution group structure on
WithConv (A →ₐ[R] A) from Mathlib/RingTheory/HopfAlgebra/Convolution.lean, Coalgebra.IsCocomm,
and Module.rankAtStalk together with Module.Finite and Module.Flat.

AMS categories

• ams-14
• ams-16

Choose either option

• I plan on working on this issue

Start with Counterexamples/GrothendieckPower.lean, then read HopfAlgebra, Mathlib/RingTheory/HopfAlgebra/Convolution.lean, Coalgebra.IsCocomm, Module.rankAtStalk, Module.Finite, and Module.Flat. The issue provides the mathematical context and prerequisites, but does not specify a precise formalization target or a completion test.