The zero section of the projective Weierstrass model and the affine chart D₊(Z)

Let W be a Weierstrass curve over a commutative ring R. The image of the zero section [0 : 1 : 0] of the projective Weierstrass model projModel W is the complement of the standard affine chart D₊(Z).

It follows that, under a morphism f : projModel W ⟶ projModel W' between the projective models of two Weierstrass curves over R that carries the zero section to the zero section, the preimage of the chart D₊(Z) of W' is contained in the chart D₊(Z) of W, and is equal to it when f is injective on points, for instance an isomorphism. If f is injective on points and moreover a morphism over Spec R, it sends a point with homogeneous coordinates [X : Y : Z], Z a unit, with values in any commutative ring, to a point with homogeneous coordinates [X' : Y' : 1].

The zero section has homogeneous coordinates (0, 1, 0), so it misses D₊(Z). Conversely, the residue-field point at a point p off D₊(Z) has homogeneous coordinates P with P₂ = 0; the projective Weierstrass equation then reads P₀³ = 0, so P is a unit multiple of (0, 1, 0) and the residue-field point factors through the zero section.

Main results

• WeierstrassCurve.projModelZero_mem_basicOpen_iff: the zero section lies on the chart D₊(Xⱼ) exactly when j = 1.
• WeierstrassCurve.mem_range_projModelZero_iff and WeierstrassCurve.range_projModelZero: the image of the zero section is the complement of the chart D₊(Z).
• WeierstrassCurve.isClosedImmersion_projModelZero: the zero section is a closed immersion.
• WeierstrassCurve.ne_projModelZero_iff_mem_basicOpen: a section of the projective model misses the zero section over a point of the base exactly when it lies on the chart D₊(Z) there.
• WeierstrassCurve.exists_eq_projModelAffinePoint: a section missing the zero section over every point of the base is the point [x : y : 1] of a solution (x, y) of the affine equation.
• WeierstrassCurve.preimage_basicOpen_coord_two_le: under a morphism of projective Weierstrass models that carries the zero section to the zero section, the preimage of the chart D₊(Z) is contained in the chart D₊(Z).
• WeierstrassCurve.preimage_basicOpen_coord_two: if the morphism is injective on points, the preimage of the chart D₊(Z) is the chart D₊(Z).
• WeierstrassCurve.exists_projModelPoint_comp_eq_projModelPoint: if it is moreover a morphism over the base, it sends a point with homogeneous coordinates P, P₂ a unit, to a point with homogeneous coordinates Q, Q₂ = 1.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/. mem_range_projModelZero_iff combines mem_range_zero_of_not_mem_zChart and not_mem_zChart_of_mem_range_zero (file ModelVariableChange.lean), which rest on specPoint_eq_zero_of_not_inZ and projModelZero_not_preimage_zChart (file WeierstrassModel.lean); range_projModelZero corresponds to sectionAway_projModelZero_eq_zChart (file PoleSheafAwayModel.lean), which states that the open complement of the zero section is the chart D₊(Z). The source shows that a point with values in a field which does not factor through the chart D₊(Z) is the zero section by a case analysis on the chart through which it factors, solving the dehomogenised equation there (eq_infPoint_of_not_inZ), and that the zero section misses D₊(Z) by computing the preimage of D₊(Z) under it. Here both directions are read off the homogeneous coordinates of a point (projModelPoint_mem_basicOpen_iff), with Mathlib's WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero for the equation; projModelZero_mem_basicOpen_iff states the first for all three charts.

preimage_basicOpen_coord_two corresponds to pointedIso_preimage_zChart (file ModelVariableChange.lean) and, for the complement of a section of a separated morphism, to preimage_sectionAway_eq_of_pointedIso (file PoleSheafAwayModel.lean), both stated there for an isomorphism; here the inclusion preimage_basicOpen_coord_two_le is stated for every morphism carrying the zero section to the zero section, and the equality for the ones that are injective on points.

exists_projModelPoint_comp_eq_projModelPoint corresponds to ZChart.mem_specPointPointedIso (file projects/ModularCurves/ModularCurves/ModularCurve/YOneAtlasClassify.lean): under an isomorphism over the base that carries the zero section to the zero section, the image of a point with values in a commutative algebra over the base ring that factors through the chart D₊(Z) factors through the chart D₊(Z). The source deduces this from the square ZChart.PointedIso.spec_map_awayι (same file), which presents the isomorphism on the chart as Spec of its action on the sections of the structure sheaf over D₊(Z) (pointedIsoΓ, file ModelVariableChange.lean). Here the values of the image point lie on the chart by preimage_basicOpen_coord_two, for a morphism that is injective on points and a point along any ring homomorphism g : R →+* S, and the statement is in homogeneous coordinates (exists_eq_projModelPoint_of_forall_mem_basicOpen).

theorem WeierstrassCurve.projModelZero_mem_basicOpen_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) (q : ↥(AlgebraicGeometry.Spec ↧R)) (j : Fin 3) : W.projModelZero q ∈ AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord j) ↔ j = 1

The zero section [0 : 1 : 0] of the projective Weierstrass model lies on the standard chart D₊(Xⱼ) exactly when j = 1: it lies on D₊(Y) and misses D₊(X) and D₊(Z).

theorem WeierstrassCurve.mem_range_projModelZero_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) (p : ↥W.projModel) : p ∈ Set.range ⇑W.projModelZero ↔ p ∉ AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)

A point of the projective Weierstrass model lies on the zero section [0 : 1 : 0] exactly when it does not lie on the standard affine chart D₊(Z).

@[simp]

theorem WeierstrassCurve.range_projModelZero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : Set.range ⇑W.projModelZero = (↑(AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)))ᶜ

The image of the zero section [0 : 1 : 0] of the projective Weierstrass model is the complement of the standard affine chart D₊(Z).

instance WeierstrassCurve.isClosedImmersion_projModelZero {R : Type u} [CommRing R] (W : WeierstrassCurve R) : AlgebraicGeometry.IsClosedImmersion W.projModelZero

The zero section of the projective Weierstrass model is a closed immersion, as is every section of a separated morphism.

theorem WeierstrassCurve.ne_projModelZero_iff_mem_basicOpen {R : Type u} [CommRing R] {W : WeierstrassCurve R} {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (s : ↥(AlgebraicGeometry.Spec ↧R)) : P s ≠ W.projModelZero s ↔ P s ∈ AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)

A section P of the projective model meets the zero section over a point s of Spec R exactly when it does not lie on the chart D₊(Z) over s.

theorem WeierstrassCurve.exists_eq_projModelAffinePoint {R : Type u} [CommRing R] {W : WeierstrassCurve R} {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (hP0 : ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), P s ≠ W.projModelZero s) : ∃ (x : R) (y : R) (h : W.toAffine.Equation x y), P = W.projModelAffinePoint h

A section missing the zero section is a point [x : y : 1]. A section of the projective model over Spec R which meets the zero section over no point of Spec R is the point [x : y : 1] of a solution (x, y) of the affine Weierstrass equation over R.

theorem WeierstrassCurve.preimage_basicOpen_coord_two_le {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} {f : W.projModel ⟶ W'.projModel} (hf : CategoryTheory.CategoryStruct.comp W.projModelZero f = W'.projModelZero) : (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Proj.basicOpen W'.toProjective.grading (W'.toProjective.coord 2)) ≤ AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)

Under a morphism f : projModel W ⟶ projModel W' of projective Weierstrass models that carries the zero section to the zero section, the preimage of the standard affine chart D₊(Z) of W' is contained in the standard affine chart D₊(Z) of W.

theorem WeierstrassCurve.preimage_basicOpen_coord_two {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} {f : W.projModel ⟶ W'.projModel} (hf : CategoryTheory.CategoryStruct.comp W.projModelZero f = W'.projModelZero) (hinj : Function.Injective ⇑f) : (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Proj.basicOpen W'.toProjective.grading (W'.toProjective.coord 2)) = AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)

Under a morphism f : projModel W ⟶ projModel W' of projective Weierstrass models that carries the zero section to the zero section and is injective on points, for instance an isomorphism, the preimage of the standard affine chart D₊(Z) of W' is the standard affine chart D₊(Z) of W.

theorem WeierstrassCurve.exists_projModelPoint_comp_eq_projModelPoint {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} {f : W.projModel ⟶ W'.projModel} (hf : CategoryTheory.CategoryStruct.comp W.projModelZero f = W'.projModelZero) (hinj : Function.Injective ⇑f) (hfo : CategoryTheory.CategoryStruct.comp f W'.projModelOver = W.projModelOver) {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} (hP : (W.toProjective.map g).Equation P) (h2 : IsUnit (P 2)) : ∃ (Q : Fin 3 → S) (hQ : (W'.toProjective.map g).Equation Q) (hQ2 : Q 2 = 1), CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP h2) f = W'.projModelPoint g hQ ⋯

Let f : projModel W ⟶ projModel W' be a morphism of projective Weierstrass models over Spec R that carries the zero section to the zero section and is injective on points, for instance an isomorphism. For a ring homomorphism g : R →+* S and a solution P of the projective Weierstrass equation of W.map g whose third coordinate is a unit, f sends the point with homogeneous coordinates P to the point with homogeneous coordinates Q, along g, for some solution Q of the projective Weierstrass equation of W'.map g whose third coordinate is 1. Such a Q is unique (projModelPoint_eq_projModelPoint_iff_of_apply_eq).