Abelian varieties over F_q: p-rank, ordinary and supersingular

[CBirkbeck]

Goal

Define the p-rank of an abelian variety A/𝔽_q (q = p^r): p-rank(A) = dim_{𝔽_p} A(𝔽̄_p)[p], and the predicates ordinary (p-rank = g) and supersingular.

What already exists

• AINTLIB HasseWeil: Tate module, torsion-point structure, the g = 1 good-reduction case. mathlib: finite fields, p-torsion of finite abelian groups.

What's missing

• pRank A := dim_{𝔽_p} A(𝔽̄_p)[p], IsOrdinary A ↔ pRank A = g, IsSupersingular A; for g = 1, ordinary ⟺ p ∤ a_p.

Test cases

• An elliptic curve: ordinary ⟺ a_p ≠ 0 (mod p); supersingular ⟺ a_p ≡ 0. p-rank between 0 and g.

LMFDB targets

• av.fq.p_rank
• av.fq.ordinary
• av.fq.supersingular

New area, not yet in the Verso blueprint — links go to the LMFDB knowls.

[CBirkbeck]

Existing mathlib infrastructure. mathlib has no definition of abelian variety or abelian scheme yet (no AbelianVariety/AbelianScheme decl as of v4.31.0-rc2). But the group-scheme foundations landed in 2026 and are the natural base to build on:

• Mathlib/AlgebraicGeometry/Group/Abelian.lean (file titled "Abelian varieties") proves the rigidity result isCommMonObj_of_isProper_of_geometricallyIntegral — a proper geometrically integral group scheme over a field is commutative (Stacks 0BFD).
• Mathlib/AlgebraicGeometry/Group/Smooth.lean — smooth_of_grpObj: a geometrically reduced, locally-of-finite-type group scheme over a field is smooth.
• Group objects in schemes are GrpObj G for G : Over (Spec (.of K)), with IsProper, IsIntegral, GeometricallyIntegral, GeometricallyReduced, Smooth available.

So an abelian variety is essentially a proper smooth geometrically integral GrpObj over Spec K — the ingredients exist but the packaged definition (plus dim, A[p], Tate module for general AVs) does not. The g = 1 test cases here still go through EllipticCurve; defining pRank/IsOrdinary/IsSupersingular in general will likely need the AV definition pinned down on top of this GrpObj API first.