Unramified elliptic torsion over an arbitrary base #
For an elliptic curve E/S and an integer n invertible in every residue field of S,
the torsion scheme E[n] is formally unramified over S. Together with local finite type,
this is unramifiedness; combined with flatness and local finite presentation, it gives étaleness.
The field-valued fibres are the torsion schemes of the base-changed elliptic curves, by
EllipticCurveGeom.isPullback_torsionMap. They are étale by the field-level theorem
EllipticCurveGeom.etale_torsion_hom. The relative conclusion uses
Scheme.Hom.formallyUnramified_of_formallyUnramified_baseChange_field.
References #
- N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.3.1.
theorem
TauCeti.AlgebraicGeometry.EllipticCurveGeom.formallyUnramified_torsion_hom
{S : AlgebraicGeometry.Scheme}
(E : EllipticCurveGeom S)
{n : ℤ}
(hn : ∀ (s : ↥S), ↑n ≠ 0)
:
The torsion scheme E[n] is formally unramified over any base on which the integer n
is invertible in every residue field.