The elliptic curve of a Weierstrass equation

Let W be an elliptic Weierstrass curve over a commutative ring R. Its projective model W.projModel, with structure morphism W.projModelOver and zero section [0 : 1 : 0], is smooth of relative dimension one and proper over Spec R, and it is its own pointed Weierstrass chart over the whole base. It is therefore an elliptic curve over Spec R in the sense of EllipticCurveGeom: W.toEllipticCurveGeom. By definition, every elliptic curve over a scheme is, Zariski-locally on the base, isomorphic to one of these. Over a local ring, the only open neighbourhood of the closed point is the whole spectrum, so every elliptic curve over a local ring is globally isomorphic to one of these (exists_iso_toEllipticCurveGeom).

The total space of toEllipticCurveGeom W is identified with W.projModel by toEllipticCurveGeomIso, compatibly with the structure morphisms and the zero sections. Base change along Spec φ : Spec R' ⟶ Spec R for a ring homomorphism φ : R →+* R' corresponds to extending the coefficients of W along φ: the total space of (toEllipticCurveGeom W).baseChange (Spec φ) is identified with (W.map φ).projModel by toEllipticCurveGeomBaseChangeIso, again compatibly with the structure morphisms and the zero sections, and with the projections to W.projModel.

The group law of the elliptic curve toEllipticCurveGeom W, glued from the Bosma–Lenstra addition morphisms of its local Weierstrass equations, is the group law of the projective model of W itself: toEllipticCurveGeomIso is an isomorphism of group schemes over Spec R (isMonHom_toEllipticCurveGeomOverIso_hom).

Main definitions

• WeierstrassCurve.toEllipticCurveGeom W: the projective model of an elliptic Weierstrass curve W over R, as an elliptic curve over Spec R.
• WeierstrassCurve.toEllipticCurveGeomIso W: the identification of the total space of toEllipticCurveGeom W with W.projModel.
• WeierstrassCurve.toEllipticCurveGeomOverIso W: the same identification, as an isomorphism of objects of Over (Spec R).
• WeierstrassCurve.toEllipticCurveGeomBaseChangeIso W φ: the identification of the total space of the base change of toEllipticCurveGeom W along Spec φ with (W.map φ).projModel.

Main results

• WeierstrassCurve.addition_toEllipticCurveGeomIso_hom and WeierstrassCurve.neg_toEllipticCurveGeomIso_hom: the addition and negation morphisms of toEllipticCurveGeom W are those of the projective model of W.
• WeierstrassCurve.isMonHom_toEllipticCurveGeomOverIso_hom: toEllipticCurveGeomOverIso W is an isomorphism of group schemes over Spec R.
• WeierstrassCurve.j_toEllipticCurveGeom: the j-invariant of toEllipticCurveGeom W is the j-invariant W.j of the equation.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_iso_toEllipticCurveGeom: every elliptic curve over a local ring R is isomorphic, over Spec R and compatibly with the zero sections, to toEllipticCurveGeom W for an elliptic Weierstrass curve W over R.

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.

The projective model as an elliptic curve

noncomputable def WeierstrassCurve.toEllipticCurveGeom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : TauCeti.AlgebraicGeometry.EllipticCurveGeom (AlgebraicGeometry.Spec ↧R)

The elliptic curve over Spec R of an elliptic Weierstrass curve W over R: the projective model W.projModel, with structure morphism W.projModelOver and zero section the point [0 : 1 : 0] (W.projModelZero). Its pointed Weierstrass atlas consists of a single chart over the whole base, whose isomorphism with the projective model is the identity. The total space is identified with W.projModel by toEllipticCurveGeomIso.

noncomputable def WeierstrassCurve.toEllipticCurveGeomIso {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : W.toEllipticCurveGeom.carrier ≅ W.projModel

The isomorphism identifying the total space of toEllipticCurveGeom W with the projective model W.projModel. Under it, the structure morphism of toEllipticCurveGeom W is W.projModelOver (toEllipticCurveGeomIso_hom_projModelOver) and its zero section is W.projModelZero (zero_toEllipticCurveGeomIso_hom).

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomIso_hom_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom W.projModelOver = W.toEllipticCurveGeom.structureMap

Under toEllipticCurveGeomIso, the structure morphism of toEllipticCurveGeom W is W.projModelOver.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomIso_hom_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.structureMap h

Under toEllipticCurveGeomIso, the structure morphism of toEllipticCurveGeom W is W.projModelOver.

@[simp]

theorem WeierstrassCurve.zero_toEllipticCurveGeomIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.zero W.toEllipticCurveGeomIso.hom = W.projModelZero

Under toEllipticCurveGeomIso, the zero section of toEllipticCurveGeom W is the zero section [0 : 1 : 0] of the projective model.

@[simp]

theorem WeierstrassCurve.zero_toEllipticCurveGeomIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.zero (CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom h) = CategoryTheory.CategoryStruct.comp W.projModelZero h

Under toEllipticCurveGeomIso, the zero section of toEllipticCurveGeom W is the zero section [0 : 1 : 0] of the projective model.

The group law

noncomputable def WeierstrassCurve.toEllipticCurveGeomOverIso {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap ≅ CategoryTheory.Over.mk W.projModelOver

The identification toEllipticCurveGeomIso of the total space of toEllipticCurveGeom W with the projective model W.projModel, as an isomorphism of objects of Over (Spec R). It is an isomorphism of group schemes over Spec R, for the group law EllipticCurveGeom.grpObj of toEllipticCurveGeom W and the group law grpObjProjModel of the projective model (isMonHom_toEllipticCurveGeomOverIso_hom).

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomOverIso_hom_left {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.Hom.left W.toEllipticCurveGeomOverIso.hom = W.toEllipticCurveGeomIso.hom

On total spaces, toEllipticCurveGeomOverIso is toEllipticCurveGeomIso.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomOverIso_inv_left {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.Hom.left W.toEllipticCurveGeomOverIso.inv = W.toEllipticCurveGeomIso.inv

On total spaces, the inverse of toEllipticCurveGeomOverIso is that of toEllipticCurveGeomIso.

@[simp]

theorem WeierstrassCurve.addition_toEllipticCurveGeomIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.addition W.toEllipticCurveGeomIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map W.toEllipticCurveGeom.structureMap W.toEllipticCurveGeom.structureMap W.projModelOver W.projModelOver W.toEllipticCurveGeomIso.hom W.toEllipticCurveGeomIso.hom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) ⋯ ⋯) W.additionMorphism

Under toEllipticCurveGeomIso, the addition morphism of toEllipticCurveGeom W is the Bosma–Lenstra addition morphism of W.

@[simp]

theorem WeierstrassCurve.addition_toEllipticCurveGeomIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.addition (CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map W.toEllipticCurveGeom.structureMap W.toEllipticCurveGeom.structureMap W.projModelOver W.projModelOver W.toEllipticCurveGeomIso.hom W.toEllipticCurveGeomIso.hom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h)

Under toEllipticCurveGeomIso, the addition morphism of toEllipticCurveGeom W is the Bosma–Lenstra addition morphism of W.

@[simp]

theorem WeierstrassCurve.neg_toEllipticCurveGeomIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.neg W.toEllipticCurveGeomIso.hom = CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom W.projModelNeg

Under toEllipticCurveGeomIso, the negation morphism of toEllipticCurveGeom W is the negation morphism of the projective model of W.

@[simp]

theorem WeierstrassCurve.neg_toEllipticCurveGeomIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.neg (CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom h) = CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom (CategoryTheory.CategoryStruct.comp W.projModelNeg h)

Under toEllipticCurveGeomIso, the negation morphism of toEllipticCurveGeom W is the negation morphism of the projective model of W.

instance WeierstrassCurve.isMonHom_toEllipticCurveGeomOverIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.IsMonHom W.toEllipticCurveGeomOverIso.hom

The projective model of W is the group scheme toEllipticCurveGeom W: the identification toEllipticCurveGeomOverIso is a homomorphism from the group law EllipticCurveGeom.grpObj of the elliptic curve toEllipticCurveGeom W to the group law grpObjProjModel of the projective model.

The j-invariant

@[simp]

theorem WeierstrassCurve.j_toEllipticCurveGeom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : W.toEllipticCurveGeom.j = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) W.j

The j-invariant of a Weierstrass model. The j-invariant of the elliptic curve toEllipticCurveGeom W over Spec R is the j-invariant W.j of the equation, as a global function on Spec R.

Base change along a ring homomorphism

noncomputable def WeierstrassCurve.toEllipticCurveGeomBaseChangeIso {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') : (W.toEllipticCurveGeom.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).carrier ≅ (W.map φ).projModel

The isomorphism identifying the total space of the base change of toEllipticCurveGeom W along Spec φ : Spec R' ⟶ Spec R with the projective model of W.map φ. Under it, the structure morphism of the base change is (W.map φ).projModelOver (toEllipticCurveGeomBaseChangeIso_hom_projModelOver), its zero section is (W.map φ).projModelZero (zero_toEllipticCurveGeomBaseChangeIso_hom), and its projection to toEllipticCurveGeom W is the base change morphism W.projModelBaseChange φ (toEllipticCurveGeomBaseChangeIso_hom_projModelBaseChange).

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomBaseChangeIso_hom_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeomBaseChangeIso φ).hom (W.map φ).projModelOver = (W.toEllipticCurveGeom.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).structureMap

Under toEllipticCurveGeomBaseChangeIso, the structure morphism of the base change of toEllipticCurveGeom W along Spec φ is (W.map φ).projModelOver.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomBaseChangeIso_hom_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R' ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeomBaseChangeIso φ).hom (CategoryTheory.CategoryStruct.comp (W.map φ).projModelOver h) = CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeom.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).structureMap h

Under toEllipticCurveGeomBaseChangeIso, the structure morphism of the base change of toEllipticCurveGeom W along Spec φ is (W.map φ).projModelOver.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomBaseChangeIso_hom_projModelBaseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeomBaseChangeIso φ).hom (W.projModelBaseChange φ) = CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeom.baseChangeIso (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst W.toEllipticCurveGeom.structureMap (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))) W.toEllipticCurveGeomIso.hom)

Under toEllipticCurveGeomBaseChangeIso and toEllipticCurveGeomIso, the projection from the base change of toEllipticCurveGeom W along Spec φ to toEllipticCurveGeom W is the base change morphism W.projModelBaseChange φ : (W.map φ).projModel ⟶ W.projModel.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomBaseChangeIso_hom_projModelBaseChange_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeomBaseChangeIso φ).hom (CategoryTheory.CategoryStruct.comp (W.projModelBaseChange φ) h) = CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeom.baseChangeIso (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst W.toEllipticCurveGeom.structureMap (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))) (CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.hom h))

Under toEllipticCurveGeomBaseChangeIso and toEllipticCurveGeomIso, the projection from the base change of toEllipticCurveGeom W along Spec φ to toEllipticCurveGeom W is the base change morphism W.projModelBaseChange φ : (W.map φ).projModel ⟶ W.projModel.

@[simp]

theorem WeierstrassCurve.zero_toEllipticCurveGeomBaseChangeIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeom.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).zero (W.toEllipticCurveGeomBaseChangeIso φ).hom = (W.map φ).projModelZero

Under toEllipticCurveGeomBaseChangeIso, the zero section of the base change of toEllipticCurveGeom W along Spec φ is the zero section [0 : 1 : 0] of the projective model of W.map φ.

@[simp]

theorem WeierstrassCurve.zero_toEllipticCurveGeomBaseChangeIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {R' : Type u} [CommRing R'] (φ : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : (W.map φ).projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeom.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ))).zero (CategoryTheory.CategoryStruct.comp (W.toEllipticCurveGeomBaseChangeIso φ).hom h) = CategoryTheory.CategoryStruct.comp (W.map φ).projModelZero h

Under toEllipticCurveGeomBaseChangeIso, the zero section of the base change of toEllipticCurveGeom W along Spec φ is the zero section [0 : 1 : 0] of the projective model of W.map φ.

Elliptic curves over a local ring

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_iso_toEllipticCurveGeom {R : Type u} [CommRing R] [IsLocalRing R] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧R)) : ∃ (W : WeierstrassCurve R) (x : W.IsElliptic) (e : W.toEllipticCurveGeom.carrier ≅ E.carrier), CategoryTheory.CategoryStruct.comp e.hom E.structureMap = W.toEllipticCurveGeom.structureMap ∧ CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeom.zero e.hom = E.zero

An elliptic curve over a local ring is the projective model of a Weierstrass equation. For an elliptic curve E over Spec R, with R a local ring, there are an elliptic Weierstrass curve W over R and an isomorphism of the total space of toEllipticCurveGeom W with that of E over Spec R, carrying the zero section [0 : 1 : 0] to the zero section of E.