Torsion points of an elliptic curve agree on an open and closed subscheme

Let E be an elliptic curve over a scheme S and n an integer invertible in every residue field of S. Two points x y : Z ⟶ E with values in some Z over S, both killed by multiplication by n, agree on an open and closed subscheme of Z. The equalizer of x and y is closed in Z because E is separated over S (Mathlib's isClosedImmersion_equalizer_ι_left). It is open because x and y factor through the torsion scheme E[n], which is formally unramified and locally of finite type over S (EllipticCurveGeom.formallyUnramified_torsion_hom), and the equalizer of two morphisms into such a scheme is open (isOpenImmersion_equalizer_ι_left).

Applied to [d]x and the zero point, this makes each condition [d]x = 0 open and closed inside the closed locus where [n]x = 0. So the locus where a point is killed by n, and at no point of Z by a proper divisor d of n, is open and closed in the locus where it is killed by n. This is how the points of exact order n in every fibre are cut out of a family of elliptic curves with a point, such as the universal Tate normal form, once n is inverted. Without the invertibility of n the equalizer need not be open: over a field of characteristic p, the zero section of E[p] is the equalizer of the inclusion E[p] ⟶ E and the zero point, and it is not an open immersion, as the local ring of E[p] at the origin is not a field.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.range_equalizer_ι_left_one: the equalizer of a point and the zero point is the set where the point meets the zero section.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOpenImmersion_equalizer_ι_left_of_mulBy_eq_one: two points killed by n agree on an open subscheme.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClopen_range_equalizer_ι_left_of_mulBy_eq_one: the set where they agree is open and closed.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOpenImmersion_equalizer_ι_comp_mulBy_left: for any point x, the locus where [d]x = 0 is open in the locus where [n]x = 0.

References

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

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.range_equalizer_ι_left_one {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) : Set.range ⇑(CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι x 1)) = {z : ↥Z.left | (CategoryTheory.Over.Hom.left x) z = E.zero (Z.hom z)}

Where a point meets the zero section. For a point x of E with values in Z, the image of the equalizer of x and the zero point is the set of points of Z at which x meets the zero section.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOpenImmersion_equalizer_ι_left_of_mulBy_eq_one {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} {Z : CategoryTheory.Over S} (hn : ∀ (s : ↥S), ↑n ≠ 0) {x y : Z ⟶ CategoryTheory.Over.mk E.structureMap} (hx : CategoryTheory.CategoryStruct.comp x (E.mulBy n) = 1) (hy : CategoryTheory.CategoryStruct.comp y (E.mulBy n) = 1) : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι x y))

Torsion points agree on an open subscheme. If the integer n is invertible in every residue field of S, two points of E with values in Z which are killed by multiplication by n agree on an open subscheme of Z: their equalizer is an open immersion into Z. It is also a closed immersion, as for any two points of the separated scheme E over S.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClopen_range_equalizer_ι_left_of_mulBy_eq_one {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} {Z : CategoryTheory.Over S} (hn : ∀ (s : ↥S), ↑n ≠ 0) {x y : Z ⟶ CategoryTheory.Over.mk E.structureMap} (hx : CategoryTheory.CategoryStruct.comp x (E.mulBy n) = 1) (hy : CategoryTheory.CategoryStruct.comp y (E.mulBy n) = 1) : IsClopen (Set.range ⇑(CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι x y)))

Torsion points agree on an open and closed set. If the integer n is invertible in every residue field of S, the set of points of Z over which two points of E with values in Z, both killed by multiplication by n, agree is open and closed.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOpenImmersion_equalizer_ι_comp_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} {Z : CategoryTheory.Over S} (hn : ∀ (s : ↥S), ↑n ≠ 0) (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) (d : ℤ) : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.CategoryStruct.comp x (E.mulBy n)) 1) (CategoryTheory.CategoryStruct.comp x (E.mulBy d))) 1))

The killed-by-d locus is open in the killed-by-n locus. Let x be any point of E with values in Z, and let the integer n be invertible in every residue field of S. Inside the closed subscheme of Z on which [n]x = 0, the closed subscheme on which moreover [d]x = 0 is open, for every integer d.