The n-torsion of an elliptic curve over a field is étale when n is invertible

Let E be an elliptic curve over a field K and let n be an integer which is invertible in K. This file proves that the n-torsion E[n] (EllipticCurveGeom.torsion) is étale over Spec K, part of Katz–Mazur 2.3.1.

Over a separably closed field, E[n] is finite over Spec K of rank n² (EllipticCurveGeom.finrank_torsion_hom) and has n² points with values in Spec K (EllipticCurveGeom.natCard_torsion). A finite scheme over a field with as many rational points as its rank is étale (AlgebraicGeometry.Scheme.Hom.etale_of_finrank_le_natCard). Over an arbitrary field K, the n-torsion of the base change of E to an algebraic closure of K is the base change of E[n] (EllipticCurveGeom.isPullback_torsionMap), and étaleness descends along the faithfully flat morphism Spec (AlgebraicClosure K) ⟶ Spec K.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.etale_torsion_hom: over a field in which n is invertible, the n-torsion E[n] is étale.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.3.1.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.etale_torsion_hom {K : Type u} [Field K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) {n : ℤ} (hn : ↑n ≠ 0) : AlgebraicGeometry.Etale (E.torsion n).X.hom

The n-torsion of an elliptic curve over a field is étale when n is invertible (Katz–Mazur 2.3.1). For an elliptic curve E over a field K and an integer n with (n : K) ≠ 0, the n-torsion E[n] is étale over Spec K.