The formal point of the projective Weierstrass model along the zero section

Let W be a Weierstrass curve over a commutative ring R. On the standard affine chart D₊(Y) of the projective Weierstrass model projModel W, the functions z = -X / Y and w = -Z / Y vanish on the zero section [0 : 1 : 0], and the Weierstrass equation reads

w = z ^ 3 + a₁ z w + a₂ z ^ 2 w + a₃ w ^ 2 + a₄ z w ^ 2 + a₆ w ^ 3.

It has a unique solution w(z) in R⟦z⟧ with zero constant coefficient, the w-expansion formalW W, so that z is a formal parameter of projModel W along the zero section. This file defines the corresponding point [z : -1 : w(z)] of projModel W with values in R⟦z⟧, the formal point, and shows that every point of projModel W with values in R⟦z⟧, lying over Spec R, that restricts to the zero section at z = 0 is the formal point reparametrised by a substitution z ↦ s(z), that is, the point [s : -1 : w(s)] for a power series s with zero constant coefficient. In the statements, z is the variable X of R⟦X⟧.

Let x be such a point. The zero section lies on the chart D₊(Y), so the preimage of D₊(Y) under x is an open subset of Spec R⟦z⟧ containing the locus z = 0. As z lies in the Jacobson radical of R⟦z⟧, every nonempty closed subset of Spec R⟦z⟧ meets the locus z = 0, so this open subset is all of Spec R⟦z⟧, although R⟦z⟧ need not be a local ring. Hence x factors through D₊(Y) and is the point [s : -1 : t] for power series s and t, which have zero constant coefficient because x restricts to [0 : 1 : 0] at z = 0. The projective Weierstrass equation at [s : -1 : t] is the w-equation at the parameter s, whose only solution with zero constant coefficient is t = w(s).

It follows that a morphism f : projModel W ⟶ projModel W' over Spec R that carries the zero section to the zero section sends the formal point of W to the formal point of W' reparametrised by a substitution z ↦ s(z): the image is a point of projModel W' with values in R⟦z⟧ that restricts to the zero section at z = 0. If f is an isomorphism, the power series s of f and s' of its inverse satisfy s'(s) = z, so s is z times a unit of R⟦z⟧.

When R is complete for the adic topology of an ideal I and t lies in I, the point of W over a field containing R that WeierstrassCurve.formalPoint (file FormalGroup/Point/Basic.lean) attaches to t, namely (t / w(t), -1 / w(t)) for t ≠ 0 and the point at infinity for t = 0, has homogeneous coordinates [t : -1 : w(t)]: the coordinates of the formal point evaluated at z = t. The two constructions are not compared in this file.

Main definitions

• WeierstrassCurve.projModelFormalPoint W: the formal point [X : -1 : w(X)] of projModel W, with values in R⟦X⟧.

Main results

• WeierstrassCurve.projModelFormalPoint_projModelOver: the formal point lies over Spec R⟦X⟧ ⟶ Spec R.
• WeierstrassCurve.SpecMap_constantCoeff_projModelFormalPoint: the formal point restricts to the zero section at X = 0.
• WeierstrassCurve.SpecMap_substAlgHom_projModelFormalPoint: the formal point reparametrised by X ↦ s is the point [s : -1 : w(s)].
• WeierstrassCurve.SpecMap_constantCoeff_comp_eq_projModelZero_iff: a point of projModel W with values in R⟦X⟧, lying over Spec R, restricts to the zero section at X = 0 exactly when it is the point [s : -1 : w(s)] for a power series s with zero constant coefficient.
• WeierstrassCurve.exists_projModelFormalPoint_comp_eq: a morphism of projective Weierstrass models over Spec R that carries the zero section to the zero section sends the formal point to the point [s : -1 : w'(s)], for a power series s with zero constant coefficient.
• WeierstrassCurve.exists_unit_projModelFormalPoint_comp_eq: for an isomorphism, s is X times a unit of R⟦X⟧.

References

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

Provenance

Not adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/, which has no formal point and does not use the w-expansion. The source proves the corresponding step of the classification of the isomorphisms of projective Weierstrass models that preserve the zero section by transporting a pole-order filtration through charts (pointedIsoCoordEquiv_filtration, file ModelVariableChange.lean).

noncomputable def WeierstrassCurve.projModelFormalPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) : AlgebraicGeometry.Spec ↧(PowerSeries R) ⟶ W.projModel

The formal point [X : -1 : w(X)] of the projective Weierstrass model along the zero section: the point of projModel W with values in the power series ring R⟦X⟧ whose homogeneous coordinates are (X, -1, w(X)), where w is the w-expansion formalW W. It restricts to the zero section at X = 0 (SpecMap_constantCoeff_projModelFormalPoint). Rewrite with projModelFormalPoint_def rather than unfolding this definition.

theorem WeierstrassCurve.projModelFormalPoint_def {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.projModelFormalPoint = W.projModelPoint (algebraMap R (PowerSeries R)) ⋯ ⋯

The formal point is the point of the projective model with homogeneous coordinates (X, -1, w(X)), along algebraMap R R⟦X⟧.

@[simp]

theorem WeierstrassCurve.projModelFormalPoint_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp W.projModelFormalPoint W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (PowerSeries R)))

The formal point lies over the morphism Spec R⟦X⟧ ⟶ Spec R induced by algebraMap R R⟦X⟧.

@[simp]

theorem WeierstrassCurve.projModelFormalPoint_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelFormalPoint (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (PowerSeries R)))) h

The formal point lies over the morphism Spec R⟦X⟧ ⟶ Spec R induced by algebraMap R R⟦X⟧.

@[simp]

theorem WeierstrassCurve.SpecMap_constantCoeff_projModelFormalPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom PowerSeries.constantCoeff)) W.projModelFormalPoint = W.projModelZero

The formal point [X : -1 : w(X)] restricts to the zero section [0 : 1 : 0] at X = 0: its composite with Spec of constantCoeff : R⟦X⟧ →+* R is the zero section.

@[simp]

theorem WeierstrassCurve.SpecMap_constantCoeff_projModelFormalPoint_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom PowerSeries.constantCoeff)) (CategoryTheory.CategoryStruct.comp W.projModelFormalPoint h) = CategoryTheory.CategoryStruct.comp W.projModelZero h

The formal point [X : -1 : w(X)] restricts to the zero section [0 : 1 : 0] at X = 0: its composite with Spec of constantCoeff : R⟦X⟧ →+* R is the zero section.

theorem WeierstrassCurve.SpecMap_substAlgHom_projModelFormalPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) {τ : Type} {s : MvPowerSeries τ R} (hs : PowerSeries.HasSubst s) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (PowerSeries.substAlgHom hs).toRingHom)) W.projModelFormalPoint = W.projModelPoint (algebraMap R (MvPowerSeries τ R)) ⋯ ⋯

The formal point reparametrised by a substitution X ↦ s, for a power series s in any set of variables that can be substituted, is the point of the projective model with homogeneous coordinates (s, -1, w(s)). The reparametrised point is its composite with Spec of substAlgHom hs : R⟦X⟧ →ₐ[R] MvPowerSeries τ R.

theorem WeierstrassCurve.SpecMap_substAlgHom_projModelFormalPoint_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {τ : Type} {s : MvPowerSeries τ R} (hs : PowerSeries.HasSubst s) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (PowerSeries.substAlgHom hs).toRingHom)) (CategoryTheory.CategoryStruct.comp W.projModelFormalPoint h) = CategoryTheory.CategoryStruct.comp (W.projModelPoint (algebraMap R (MvPowerSeries τ R)) ⋯ ⋯) h

The formal point reparametrised by a substitution X ↦ s, for a power series s in any set of variables that can be substituted, is the point of the projective model with homogeneous coordinates (s, -1, w(s)). The reparametrised point is its composite with Spec of substAlgHom hs : R⟦X⟧ →ₐ[R] MvPowerSeries τ R.

theorem WeierstrassCurve.SpecMap_constantCoeff_comp_eq_projModelZero_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x : AlgebraicGeometry.Spec ↧(PowerSeries R) ⟶ W.projModel} (hx : CategoryTheory.CategoryStruct.comp x W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (PowerSeries R)))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom PowerSeries.constantCoeff)) x = W.projModelZero ↔ ∃ (s : PowerSeries R) (_ : PowerSeries.constantCoeff s = 0) (h : (W.toProjective.map (algebraMap R (PowerSeries R))).Equation ![s, -1, PowerSeries.subst s W.formalW]), x = W.projModelPoint (algebraMap R (PowerSeries R)) h ⋯

A point x of the projective Weierstrass model with values in R⟦X⟧, lying over Spec R, restricts to the zero section at X = 0 exactly when it is the point [s : -1 : w(s)] for a power series s with zero constant coefficient, that is, the formal point reparametrised by X ↦ s (SpecMap_substAlgHom_projModelFormalPoint). Such an s is unique (projModelPoint_eq_projModelPoint_iff_of_apply_eq).

theorem WeierstrassCurve.exists_projModelFormalPoint_comp_eq {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} {f : W.projModel ⟶ W'.projModel} (hf : CategoryTheory.CategoryStruct.comp W.projModelZero f = W'.projModelZero) (hfo : CategoryTheory.CategoryStruct.comp f W'.projModelOver = W.projModelOver) : ∃ (s : PowerSeries R) (_ : PowerSeries.constantCoeff s = 0) (h : (W'.toProjective.map (algebraMap R (PowerSeries R))).Equation ![s, -1, PowerSeries.subst s W'.formalW]), CategoryTheory.CategoryStruct.comp W.projModelFormalPoint f = W'.projModelPoint (algebraMap R (PowerSeries R)) h ⋯

A morphism f : projModel W ⟶ projModel W' of projective Weierstrass models over Spec R that carries the zero section to the zero section sends the formal point [X : -1 : w(X)] of W to the point [s : -1 : w'(s)] of W', for a power series s with zero constant coefficient, where w' is the w-expansion of W'; that is, to the formal point of W' reparametrised by X ↦ s (SpecMap_substAlgHom_projModelFormalPoint). If f is an isomorphism, s is X times a unit of R⟦X⟧ (exists_unit_projModelFormalPoint_comp_eq).

theorem WeierstrassCurve.exists_unit_projModelFormalPoint_comp_eq {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} (e : W.projModel ≅ W'.projModel) (hz : CategoryTheory.CategoryStruct.comp W.projModelZero e.hom = W'.projModelZero) (ho : CategoryTheory.CategoryStruct.comp e.hom W'.projModelOver = W.projModelOver) : ∃ (v : (PowerSeries R)ˣ) (h : (W'.toProjective.map (algebraMap R (PowerSeries R))).Equation ![PowerSeries.X * ↑v, -1, PowerSeries.subst (PowerSeries.X * ↑v) W'.formalW]), CategoryTheory.CategoryStruct.comp W.projModelFormalPoint e.hom = W'.projModelPoint (algebraMap R (PowerSeries R)) h ⋯

An isomorphism e : projModel W ≅ projModel W' of projective Weierstrass models over Spec R that carries the zero section to the zero section sends the formal point [X : -1 : w(X)] of W to the point [s : -1 : w'(s)] of W' with s = X * v for a unit v of R⟦X⟧, where w' is the w-expansion of W'. For a morphism that need not be an isomorphism, see exists_projModelFormalPoint_comp_eq.