The projective Weierstrass model

For a Weierstrass curve W over a commutative ring R, the projective Weierstrass model is the scheme over R cut out by the cubic

Y²Z + a₁XYZ + a₃YZ² = X³ + a₂X²Z + a₄XZ² + a₆Z³

in homogeneous coordinates [X : Y : Z]. It is constructed here as the Proj of the graded homogeneous coordinate ring WeierstrassCurve.Projective.CoordinateRing W. No ellipticity hypothesis is needed for the construction, for properness, or for the zero section [0 : 1 : 0]; ellipticity enters only for smoothness.

The zero section is defined on the standard affine chart D₊(Y), where it is the point X/Y = Z/Y = 0.

An admissible change of variables C induces an isomorphism projModel (C • W) ≅ projModel W over Spec R carrying the zero section to the zero section: Proj of the graded isomorphism of homogeneous coordinate rings WeierstrassCurve.Projective.variableChangeEquiv W C.

Main definitions

• WeierstrassCurve.projModel W: the projective Weierstrass model, a scheme.
• WeierstrassCurve.projModelOver W: its structure morphism to Spec R.
• WeierstrassCurve.projModelZero W: the zero section [0 : 1 : 0], a morphism Spec R ⟶ projModel W, defined on the standard affine chart D₊(Y).
• WeierstrassCurve.projModelVariableChangeIso W C: the isomorphism projModel (C • W) ≅ projModel W induced by a change of variables C.

Main results

• WeierstrassCurve.isProper_projModelOver: the projective Weierstrass model is proper over the base.
• WeierstrassCurve.compactSpace_projModel: the projective Weierstrass model is quasi-compact.
• WeierstrassCurve.isNoetherian_projModel: over a Noetherian ring, the projective Weierstrass model is a Noetherian scheme.
• WeierstrassCurve.projModelZero_projModelOver: the zero section is a section of the structure morphism.
• WeierstrassCurve.awayι_projModelOver: on a standard affine chart, the structure morphism is Spec of the structure map of the chart.
• WeierstrassCurve.projModelZero_map: Proj.map F of a graded ring homomorphism F of homogeneous coordinate rings carries the zero section to the zero section, over Spec φ, when evaluating F a at [0 : 1 : 0] gives cⁿ times φ of the value of a for a of degree n.
• WeierstrassCurve.projModelVariableChangeIso_one and WeierstrassCurve.projModelVariableChangeIso_mul: the isomorphisms induced by changes of variables are compatible with the identity and with products.
• WeierstrassCurve.projModelVariableChangeIso_hom_projModelOver and WeierstrassCurve.projModelZero_projModelVariableChangeIso_hom: the isomorphism induced by a change of variables lies over Spec R and preserves the zero section.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.
• P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, II.1.

Provenance

isNoetherian_projModel is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/: the unnamed instance IsLocallyNoetherian universalCurve in PointsDictionary.lean and its universe-polymorphic counterpart IsLocallyNoetherian (projModel universalWeierstrassLocU) in GroupLawAxioms.lean. The source proves that the universal Weierstrass curve over ℤ[a₁, a₂, a₃, a₄, a₆][Δ⁻¹] is locally Noetherian. Here every Weierstrass curve over every Noetherian ring is treated, and the model is shown to be a Noetherian scheme: it is also quasi-compact, by compactSpace_projModel.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.projModel {R : Type u} [CommRing R] (W : WeierstrassCurve R) : AlgebraicGeometry.Scheme

The projective Weierstrass model of W: the projective cubic Y²Z + a₁XYZ + a₃YZ² = X³ + a₂X²Z + a₄XZ² + a₆Z³ over R, as the Proj of the homogeneous coordinate ring R[X, Y, Z] ⧸ (W(X, Y, Z)) graded by total degree.

Equations

• W.projModel = AlgebraicGeometry.Proj W.toProjective.grading

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

The structure morphism projModel W ⟶ Spec R of the projective Weierstrass model: the structure morphism of Proj to the spectrum of the degree-zero part, which is R.

Equations

• One or more equations did not get rendered due to their size.

instance WeierstrassCurve.isProper_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) : AlgebraicGeometry.IsProper W.projModelOver

The projective Weierstrass model is proper over its base.

instance WeierstrassCurve.compactSpace_projModel {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CompactSpace ↥W.projModel

The projective Weierstrass model is quasi-compact.

instance WeierstrassCurve.isNoetherian_projModel {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsNoetherianRing R] : AlgebraicGeometry.IsNoetherian W.projModel

Over a Noetherian ring, the projective Weierstrass model is a Noetherian scheme.

theorem WeierstrassCurve.awayι_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) {f : W.toProjective.CoordinateRing} {m : ℕ} (f_deg : f ∈ W.toProjective.grading m) (hm : 0 < m) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι W.toProjective.grading f f_deg hm) W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom W.toProjective.grading (Submonoid.powers f)).comp (algebraMap R ↥(W.toProjective.grading 0))))

On a standard affine chart D₊(f), the structure morphism of the projective model is Spec of the structure map R → A_(f), through the degree-zero part of the homogeneous coordinate ring.

theorem WeierstrassCurve.awayι_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {f : W.toProjective.CoordinateRing} {m : ℕ} (f_deg : f ∈ W.toProjective.grading m) (hm : 0 < m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι W.toProjective.grading f f_deg hm) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom W.toProjective.grading (Submonoid.powers f)).comp (algebraMap R ↥(W.toProjective.grading 0))))) h

On a standard affine chart D₊(f), the structure morphism of the projective model is Spec of the structure map R → A_(f), through the degree-zero part of the homogeneous coordinate ring.

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

The zero section [0 : 1 : 0] of the projective Weierstrass model, a morphism Spec R ⟶ projModel W through the standard affine chart D₊(Y).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.projModelZero_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp W.projModelZero W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)

The zero section is a section of the structure morphism.

@[simp]

theorem WeierstrassCurve.projModelZero_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelZero (CategoryTheory.CategoryStruct.comp W.projModelOver h) = h

The zero section is a section of the structure morphism.

theorem WeierstrassCurve.projModelZero_map {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] {W' : WeierstrassCurve R'} (F : W.toProjective.grading →+*ᵍ W'.toProjective.grading) (hF : HomogeneousIdeal.irrelevant W'.toProjective.grading ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant W.toProjective.grading)) (φ : R →+* R') (c : R'ˣ) (h : ∀ (n : ℕ), ∀ a ∈ W.toProjective.grading n, W'.toProjective.evalZero (F a) = ↑c ^ n * φ (W.toProjective.evalZero a)) : CategoryTheory.CategoryStruct.comp W'.projModelZero (AlgebraicGeometry.Proj.map F hF) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ)) W.projModelZero

Let F be a graded ring homomorphism from the homogeneous coordinate ring of W over R to that of W' over R', and φ : R →+* R'. If, for a unit c of R' and every homogeneous a of degree n, the value of F a at [0 : 1 : 0] is cⁿ times φ of the value of a there, then Proj.map F carries the zero section of projModel W' to the zero section of projModel W, over Spec φ : Spec R' ⟶ Spec R.

theorem WeierstrassCurve.projModelZero_map_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] {W' : WeierstrassCurve R'} (F : W.toProjective.grading →+*ᵍ W'.toProjective.grading) (hF : HomogeneousIdeal.irrelevant W'.toProjective.grading ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant W.toProjective.grading)) (φ : R →+* R') (c : R'ˣ) (h : ∀ (n : ℕ), ∀ a ∈ W.toProjective.grading n, W'.toProjective.evalZero (F a) = ↑c ^ n * φ (W.toProjective.evalZero a)) {Z : AlgebraicGeometry.Scheme} (h✝ : AlgebraicGeometry.Proj W.toProjective.grading ⟶ Z) : CategoryTheory.CategoryStruct.comp W'.projModelZero (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.map F hF) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ)) (CategoryTheory.CategoryStruct.comp W.projModelZero h✝)

Let F be a graded ring homomorphism from the homogeneous coordinate ring of W over R to that of W' over R', and φ : R →+* R'. If, for a unit c of R' and every homogeneous a of degree n, the value of F a at [0 : 1 : 0] is cⁿ times φ of the value of a there, then Proj.map F carries the zero section of projModel W' to the zero section of projModel W, over Spec φ : Spec R' ⟶ Spec R.

noncomputable def WeierstrassCurve.projModelVariableChangeIso {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).projModel ≅ W.projModel

The isomorphism projModel (C • W) ≅ projModel W of projective Weierstrass models induced by the change of variables C. On homogeneous coordinates it is [X : Y : Z] ↦ [u²X + rZ : u²sX + u³Y + tZ : Z], so on the affine part it is (x, y) ↦ (u²x + r, u³y + u²sx + t).

Equations

• W.projModelVariableChangeIso C = AlgebraicGeometry.Proj.mapIso (WeierstrassCurve.variableChangeGradedHom✝ W C) (WeierstrassCurve.variableChangeGradedHomSymm✝ W C) ⋯ ⋯

theorem WeierstrassCurve.ProjMap_eq_eqToHom_comp_ProjMap {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] {W₁ W₂ : WeierstrassCurve S} (h : W₁ = W₂) (g₁ : W.toProjective.grading →+*ᵍ W₁.toProjective.grading) (g₂ : W.toProjective.grading →+*ᵍ W₂.toProjective.grading) (q : MvPolynomial (Fin 3) R → MvPolynomial (Fin 3) S) (hg₁ : ∀ (p : MvPolynomial (Fin 3) R), g₁ ((Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) p) = (Ideal.Quotient.mk (Ideal.span {W₁.toProjective.polynomial})) (q p)) (hg₂ : ∀ (p : MvPolynomial (Fin 3) R), g₂ ((Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) p) = (Ideal.Quotient.mk (Ideal.span {W₂.toProjective.polynomial})) (q p)) (hf₁ : HomogeneousIdeal.irrelevant W₁.toProjective.grading ≤ HomogeneousIdeal.map g₁ (HomogeneousIdeal.irrelevant W.toProjective.grading)) (hf₂ : HomogeneousIdeal.irrelevant W₂.toProjective.grading ≤ HomogeneousIdeal.map g₂ (HomogeneousIdeal.irrelevant W.toProjective.grading)) : AlgebraicGeometry.Proj.map g₁ hf₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Proj.map g₂ hf₂)

Let g₁ and g₂ be graded ring homomorphisms from the homogeneous coordinate ring of W to those of equal Weierstrass curves W₁ = W₂ over S. If both send the class of each polynomial p to the class of the same polynomial q p, then Proj.map g₁ is Proj.map g₂ preceded by the eqToHom identifying the projective models of W₁ and W₂.

@[simp]

theorem WeierstrassCurve.projModelVariableChangeIso_one {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.projModelVariableChangeIso 1 = CategoryTheory.eqToIso ⋯

The identity change of variables induces the identity of the projective Weierstrass model, up to 1 • W = W.

@[simp]

theorem WeierstrassCurve.projModelVariableChangeIso_mul {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C C' : VariableChange R) : W.projModelVariableChangeIso (C * C') = CategoryTheory.eqToIso ⋯ ≪≫ (C' • W).projModelVariableChangeIso C ≪≫ W.projModelVariableChangeIso C'

The isomorphism induced by a product C * C' is the isomorphism induced by C followed by the one induced by C', up to (C * C') • W = C • C' • W.

@[simp]

theorem WeierstrassCurve.projModelVariableChangeIso_hom_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom W.projModelOver = (C • W).projModelOver

The isomorphism induced by a change of variables lies over the base.

@[simp]

theorem WeierstrassCurve.projModelVariableChangeIso_hom_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (C • W).projModelOver h

The isomorphism induced by a change of variables lies over the base.

@[simp]

theorem WeierstrassCurve.projModelZero_projModelVariableChangeIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : CategoryTheory.CategoryStruct.comp (C • W).projModelZero (W.projModelVariableChangeIso C).hom = W.projModelZero

The isomorphism induced by a change of variables carries the zero section to the zero section: [0 : 1 : 0] ↦ [0 : u³ : 0] = [0 : 1 : 0].

@[simp]

theorem WeierstrassCurve.projModelZero_projModelVariableChangeIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (C • W).projModelZero (CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom h) = CategoryTheory.CategoryStruct.comp W.projModelZero h

The isomorphism induced by a change of variables carries the zero section to the zero section: [0 : 1 : 0] ↦ [0 : u³ : 0] = [0 : 1 : 0].