Elliptic curves over a scheme

An elliptic curve over a scheme S is recorded here as a geometric object: a smooth proper morphism X ⟶ S of relative dimension one with a section, which Zariski-locally on S is the projective Weierstrass model WeierstrassCurve.projModel of an elliptic Weierstrass curve, compatibly with the structure morphisms and with the zero section [0 : 1 : 0].

The local-model condition is given in two forms. A pointed Weierstrass chart of π : X ⟶ S pointed by zero : S ⟶ X consists of an open immersion base ⟶ S from a scheme isomorphic to Spec R, an elliptic Weierstrass curve W over R, a pullback square of π along the open immersion, and an isomorphism of its apex with projModel W over Spec R carrying the section induced by zero to the zero section; a pointed Weierstrass atlas is a family of charts whose images cover S. The predicate IsLocallyWeierstrass states the condition pointwise instead, on affine opens U of S with Weierstrass curves over Γ(S, U) and the chosen pullback of π along U ⟶ S. The two forms agree: nonempty_pointedWeierstrassAtlas_iff.

Main definitions

• TauCeti.AlgebraicGeometry.PointedWeierstrassChart π zero: a pointed Weierstrass chart of π with section zero.
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.ofAffineOpen: the pointed Weierstrass chart on an affine open of the base given by the data of the local-model condition there.
• TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas π zero: a family of pointed Weierstrass charts whose images cover the base.
• TauCeti.AlgebraicGeometry.IsLocallyWeierstrass π zero hzero: every point of the base has an affine open neighbourhood over which π is the projective model of an elliptic Weierstrass curve, compatibly with the section.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom S: an elliptic curve over S, a smooth proper morphism of relative dimension one with a section admitting a pointed Weierstrass atlas.

Main results

• TauCeti.AlgebraicGeometry.isLocallyWeierstrass_iff: the local-model condition in terms of affine opens, Weierstrass curves and isomorphisms with projective models.
• TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.isLocallyWeierstrass: a pointed Weierstrass atlas gives the local-model condition.
• TauCeti.AlgebraicGeometry.nonempty_pointedWeierstrassAtlas_iff: a pointed Weierstrass atlas exists if and only if the local-model condition holds.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isLocallyWeierstrass: an elliptic curve over S satisfies the local-model condition.

Implementation notes

The coefficient ring of a chart is only isomorphic to the ring of sections over the image of its base. Comparing a chart with the local-model condition therefore moves its Weierstrass curve along a ring isomorphism φ with WeierstrassCurve.map, and identifies projModel (W.map φ) with projModel W by WeierstrassCurve.projModelMapIso, the base change morphism along φ.

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

IsLocallyWeierstrass and EllipticCurveGeom are adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/Basic.lean, declarations ModularCurves.LocallyWeierstrass and ModularCurves.EllipticCurveGeom. Here the projective model is WeierstrassCurve.projModel, and the local model of EllipticCurveGeom is a nonempty pointed Weierstrass atlas, which is equivalent to IsLocallyWeierstrass by nonempty_pointedWeierstrassAtlas_iff.

Pointed Weierstrass charts and atlases

structure TauCeti.AlgebraicGeometry.PointedWeierstrassChart {S X : AlgebraicGeometry.Scheme} (π : X ⟶ S) (zero : S ⟶ X) : Type (u + 1)

A pointed Weierstrass chart of a morphism π : X ⟶ S pointed by zero : S ⟶ X: an open immersion baseMap : base ⟶ S from a scheme base ≅ Spec ring, an elliptic Weierstrass curve equation over ring, a pullback square of π along baseMap with apex pullbackCarrier, and an isomorphism modelIso of pullbackCarrier with the projective model of equation, lying over Spec ring and carrying the section pulledZero induced by zero to the zero section [0 : 1 : 0]. A chart presents X over the open subscheme of S that is the image of baseMap, and its fields make zero a section of π over that image.

• base : AlgebraicGeometry.Scheme

  The base of the chart.

• baseMap : self.base ⟶ S

  The inclusion of the base of the chart into S.

• baseMap_open : AlgebraicGeometry.IsOpenImmersion self.baseMap

  The base of the chart is an open subscheme of S.

• ring : CommRingCat

  The coefficient ring of the chart.

• baseIso : self.base ≅ AlgebraicGeometry.Spec self.ring

  An isomorphism of the base of the chart with the spectrum of its coefficient ring.

• equation : WeierstrassCurve ↑self.ring

  The Weierstrass equation of the chart.

• equation_elliptic : self.equation.IsElliptic

  The Weierstrass equation of the chart is elliptic.

• pullbackCarrier : AlgebraicGeometry.Scheme

  The restriction of X to the base of the chart.

• toTotal : self.pullbackCarrier ⟶ X

  The inclusion of the restriction into X, the base change of baseMap along π.

• toBase : self.pullbackCarrier ⟶ self.base

  The structure morphism of the restriction.

• isPullback : CategoryTheory.IsPullback self.toTotal self.toBase π self.baseMap

  The restriction is the pullback of π along baseMap.

• modelIso : self.pullbackCarrier ≅ self.equation.projModel

  An isomorphism of the restriction with the projective model of the equation.

• modelIso_over : CategoryTheory.CategoryStruct.comp self.modelIso.hom self.equation.projModelOver = CategoryTheory.CategoryStruct.comp self.toBase self.baseIso.hom

  The isomorphism with the projective model lies over Spec ring.

• pulledZero : self.base ⟶ self.pullbackCarrier

  The section of the restriction induced by zero.

• pulledZero_toBase : CategoryTheory.CategoryStruct.comp self.pulledZero self.toBase = CategoryTheory.CategoryStruct.id self.base

  pulledZero is a section of the structure morphism of the restriction.

• pulledZero_toTotal : CategoryTheory.CategoryStruct.comp self.pulledZero self.toTotal = CategoryTheory.CategoryStruct.comp self.baseMap zero

  pulledZero lifts the restriction baseMap ≫ zero of zero along toTotal.

• modelIso_zero : CategoryTheory.CategoryStruct.comp self.pulledZero self.modelIso.hom = CategoryTheory.CategoryStruct.comp self.baseIso.hom self.equation.projModelZero

  The isomorphism with the projective model carries pulledZero to the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_over_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (self : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↑self.ring ⟶ Z) : CategoryTheory.CategoryStruct.comp self.modelIso.hom (CategoryTheory.CategoryStruct.comp self.equation.projModelOver h) = CategoryTheory.CategoryStruct.comp self.toBase (CategoryTheory.CategoryStruct.comp self.baseIso.hom h)

The isomorphism with the projective model lies over Spec ring.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_zero_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (self : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : self.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp self.pulledZero (CategoryTheory.CategoryStruct.comp self.modelIso.hom h) = CategoryTheory.CategoryStruct.comp self.baseIso.hom (CategoryTheory.CategoryStruct.comp self.equation.projModelZero h)

The isomorphism with the projective model carries pulledZero to the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_toBase_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (self : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : self.base ⟶ Z) : CategoryTheory.CategoryStruct.comp self.pulledZero (CategoryTheory.CategoryStruct.comp self.toBase h) = h

pulledZero is a section of the structure morphism of the restriction.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_toTotal_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (self : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.pulledZero (CategoryTheory.CategoryStruct.comp self.toTotal h) = CategoryTheory.CategoryStruct.comp self.baseMap (CategoryTheory.CategoryStruct.comp zero h)

pulledZero lifts the restriction baseMap ≫ zero of zero along toTotal.

structure TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas {S X : AlgebraicGeometry.Scheme} (π : X ⟶ S) (zero : S ⟶ X) : Type (u + 1)

A pointed Weierstrass atlas of a morphism π : X ⟶ S pointed by zero : S ⟶ X: a family of pointed Weierstrass charts whose images cover S. The images are open, so an atlas exhibits π Zariski-locally on S as the projective model of an elliptic Weierstrass curve with zero as its zero section.

• index : Type u

  The index type of the charts.

• chart : self.index → PointedWeierstrassChart π zero

  The charts.

• covers (s : ↥S) : ∃ (i : self.index) (x : ↥(self.chart i).base), (self.chart i).baseMap x = s

  The images of the charts cover S.

def TauCeti.AlgebraicGeometry.IsLocallyWeierstrass {X S : AlgebraicGeometry.Scheme} (π : X ⟶ S) (zero : S ⟶ X) (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) : Prop

The local-model condition for a morphism π : X ⟶ S with a section zero: every point of S has an affine open neighbourhood U with an elliptic Weierstrass curve W over Γ(S, U) and an isomorphism of the restriction pullback π U.ι of X to U with the projective model of W, lying over U ≅ Spec Γ(S, U) and carrying the section induced by zero to the zero section of the model. It holds if and only if a PointedWeierstrassAtlas exists: nonempty_pointedWeierstrassAtlas_iff.

Equations

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

theorem TauCeti.AlgebraicGeometry.isLocallyWeierstrass_iff {X S : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) : IsLocallyWeierstrass π zero hzero ↔ ∀ (s : ↥S), ∃ (U : ↑S.affineOpens) (_ : s ∈ ↑U) (W : WeierstrassCurve ↑(S.presheaf.obj (Opposite.op ↑U))), W.IsElliptic ∧ ∃ (e : CategoryTheory.Limits.pullback π (↑U).ι ≅ W.projModel), CategoryTheory.CategoryStruct.comp e.hom W.projModelOver = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (↑U).ι) (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).hom ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (↑U).ι zero) (CategoryTheory.CategoryStruct.id ↑↑U) ⋯)) e.hom = W.projModelZero

The local-model condition IsLocallyWeierstrass π zero hzero holds if and only if every point of S has an affine open neighbourhood U with an elliptic Weierstrass curve W over Γ(S, U) and an isomorphism of pullback π U.ι with the projective model of W, lying over U ≅ Spec Γ(S, U) and carrying the section induced by zero to the zero section of the model.

instance TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isAffine_base {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : AlgebraicGeometry.IsAffine c.base

The base of a pointed Weierstrass chart is affine: it is isomorphic to Spec ring.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.ofAffineOpen {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) (U : ↑S.affineOpens) (W : WeierstrassCurve ↑(S.presheaf.obj (Opposite.op ↑U))) (hW : W.IsElliptic) (e : CategoryTheory.Limits.pullback π (↑U).ι ≅ W.projModel) (hover : CategoryTheory.CategoryStruct.comp e.hom W.projModelOver = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (↑U).ι) (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).hom) (hzero' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (↑U).ι zero) (CategoryTheory.CategoryStruct.id ↑↑U) ⋯)) e.hom = W.projModelZero) : PointedWeierstrassChart π zero

The pointed Weierstrass chart on an affine open U of S given by an elliptic Weierstrass curve W over Γ(S, U) and an isomorphism e of the chosen pullback pullback π U.ι with the projective model of W, lying over U ≅ Spec Γ(S, U) and carrying the section induced by zero to the zero section. Its base is U, its coefficient ring is Γ(S, U) and its section is pullback.lift (U.ι ≫ zero) (𝟙 U).

Equations

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

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.isLocallyWeierstrass {X S : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) (A : PointedWeierstrassAtlas π zero) : IsLocallyWeierstrass π zero hzero

A morphism π with a section zero that admits a pointed Weierstrass atlas satisfies the local-model condition IsLocallyWeierstrass π zero hzero. The converse also holds: nonempty_pointedWeierstrassAtlas_iff.

theorem TauCeti.AlgebraicGeometry.nonempty_pointedWeierstrassAtlas_iff {X S : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) : Nonempty (PointedWeierstrassAtlas π zero) ↔ IsLocallyWeierstrass π zero hzero

A morphism with a section admits a pointed Weierstrass atlas if and only if it satisfies the local-model condition IsLocallyWeierstrass.

Elliptic curves over a scheme

structure TauCeti.AlgebraicGeometry.EllipticCurveGeom (S : AlgebraicGeometry.Scheme) : Type (u + 1)

An elliptic curve over a scheme S, as a geometric object: a morphism structureMap : carrier ⟶ S, smooth of relative dimension one and proper, with a section zero, such that structureMap and zero admit a pointed Weierstrass atlas, so that Zariski-locally on S the curve is the projective model of an elliptic Weierstrass curve with zero the zero section [0 : 1 : 0]. The atlas appears under Nonempty, so no local equation is part of the data.

• carrier : AlgebraicGeometry.Scheme

  The total space.

• structureMap : self.carrier ⟶ S

  The structure morphism.

• zero : S ⟶ self.carrier

  The zero section.

• zero_comp : CategoryTheory.CategoryStruct.comp self.zero self.structureMap = CategoryTheory.CategoryStruct.id S

  The zero section is a section of the structure morphism.

• smooth : AlgebraicGeometry.SmoothOfRelativeDimension 1 self.structureMap

  The structure morphism is smooth of relative dimension one.

• proper : AlgebraicGeometry.IsProper self.structureMap

  The structure morphism is proper.

• localModel : Nonempty (PointedWeierstrassAtlas self.structureMap self.zero)

  A pointed Weierstrass atlas exists: Zariski-locally on S, the curve is the projective model of an elliptic Weierstrass curve, compatibly with the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_comp_structureMap {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.zero E.structureMap = CategoryTheory.CategoryStruct.id S

The zero section of an elliptic curve is a section of its structure morphism: the field zero_comp, as a simp lemma.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_comp_structureMap_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp E.zero (CategoryTheory.CategoryStruct.comp E.structureMap h) = h

The zero section of an elliptic curve is a section of its structure morphism: the field zero_comp, as a simp lemma.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isLocallyWeierstrass {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : IsLocallyWeierstrass E.structureMap E.zero ⋯

An elliptic curve over S satisfies the local-model condition IsLocallyWeierstrass for its structure morphism and zero section: the pointwise form of the atlas condition localModel.