Multiplication by n is finite locally free of rank n²

Let E be an elliptic curve over a scheme S and let n be a nonzero integer. This file proves that multiplication by n, [n] : E ⟶ E, is finite locally free of rank n²: it is finite (EllipticCurveGeom.isFinite_mulBy_left), flat and locally of finite presentation, and its fibre over every point of E is the spectrum of an algebra of dimension n² over the residue field of that point. Consequently the n-torsion E[n], the fibre of [n] over the zero section, is finite locally free of rank n² over S, and [n] is surjective.

Over a field E is the projective model of a Weierstrass equation (TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_iso_toEllipticCurveGeom), and on that model [n] is flat of rank the degree n² of the function-field extension it induces (WeierstrassCurve.finrank_projModelMulBy). Over an arbitrary base, [n] is a morphism over S between schemes smooth over S, so it is locally of finite presentation. Its base change to the fibre of E over a point s of S is multiplication by n on the elliptic curve over the residue field of s obtained by base change, which is flat; by the fibrewise criterion for flatness (AlgebraicGeometry.Scheme.Hom.flat_of_flat_pullback_fiberι) [n] is flat. The rank of a finite flat morphism is invariant under base change, so it is n² everywhere.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_mulBy_left: multiplication by a nonzero integer is flat.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_mulBy_left: multiplication by a nonzero integer n has rank n² at every point.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_torsion_hom and TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_torsion_hom: for n ≠ 0, the n-torsion is finite locally free of rank n² over S; so is the closed subscheme of its ideal sheaf (TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_ker_torsionι_left and TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_ker_torsionι_left).
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.surjective_mulBy_left: multiplication by a nonzero integer is surjective.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.3.1.
• A. Grothendieck, Éléments de géométrie algébrique IV, troisième partie, Théorème 11.3.10, the critère de platitude par fibres.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) : AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left (E.mulBy n))

Multiplication by a nonzero integer is flat (Katz–Mazur 2.3.1), over any base S.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) (x : ↥E.carrier) : AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.Over.Hom.left (E.mulBy n)) x = n.natAbs ^ 2

Multiplication by n has rank n² (Katz–Mazur 2.3.1), over any base S. For n ≠ 0, the finite flat morphism [n] : E ⟶ E has rank n² at every point x: the fibre of [n] over x is the spectrum of an algebra of dimension n² over the residue field of x.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_torsion_hom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) : AlgebraicGeometry.Flat (E.torsion n).X.hom

The n-torsion is flat over S for n ≠ 0: E[n] is the base change of the flat morphism [n] along the zero section.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_ker_torsionι_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} [NeZero n] : AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (E.torsionι n))).subschemeι E.structureMap)

The closed subscheme of the ideal sheaf of E[n] is finite over S for n ≠ 0.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_ker_torsionι_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} [NeZero n] : AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (E.torsionι n))).subschemeι E.structureMap)

The closed subscheme of the ideal sheaf of E[n] is flat over S for n ≠ 0.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_torsion_hom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) (s : ↥S) : AlgebraicGeometry.Scheme.Hom.finrank (E.torsion n).X.hom s = n.natAbs ^ 2

The n-torsion has rank n² (Katz–Mazur 2.3.1). For an elliptic curve E over a scheme S and n ≠ 0, the n-torsion E[n] is finite, flat and locally of finite presentation over S (isFinite_torsion_hom, flat_torsion_hom, locallyOfFinitePresentation_torsion_hom), and its rank at every point s of S is n²: it is the fibre of [n] over the zero section.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.surjective_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) : AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left (E.mulBy n))

Multiplication by a nonzero integer is surjective (Katz–Mazur 2.3.1), over any base S: it is finite and flat of rank n² ≥ 1 at every point.