Multiplication by a nonzero integer is finite

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 a finite morphism of schemes. It is proper, since E is proper and separated over S, so by Zariski's main theorem it suffices that [n] is locally quasi-finite, that is, that each of its fibres is finite.

The fibre of [n] over a point y of E is contained in the image of a fibre of multiplication by n on the base change of E to an algebraic closure Ω of the residue field of y, namely the fibre over the Ω-point given by y, since that multiplication by n is the base change of [n]. Over the algebraically closed field Ω, the closed points of a scheme locally of finite type are its Ω-points. The Ω-points in a fibre of [n] over an Ω-point form a coset of the group of Ω-points of E killed by n, which is finite, and a closed subset of a Jacobson space with finitely many closed points is finite.

Consequently the n-torsion E[n], the fibre of [n] over the zero section, is finite over S.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyQuasiFinite_mulBy_left: multiplication by a nonzero integer is locally quasi-finite.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_mulBy_left: multiplication by a nonzero integer is finite.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_torsion_hom: for n ≠ 0, the n-torsion E[n] is finite over S.

References

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

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

Multiplication by a nonzero integer is locally quasi-finite: every fibre of [n] : E ⟶ E is finite.

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

Multiplication by a nonzero integer is finite (Katz–Mazur 2.3.1): it is proper and locally quasi-finite.

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

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