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.PointedWeierstrassChart.restrict c V: the restriction of a chart to an affine open V of its base, with equation the coefficient extension of the equation of c to Γ(base, V); its base is included in that of c by restrictι.
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap: the morphism between the restrictions of the curve to the bases of two charts induced by a morphism of bases over S, a base change square (isPullback_pullbackCarrierMap); projModelMap is the same morphism between the projective models of the equations of the two charts.
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint and TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint: the sections of the restriction of the curve to the base of a chart, and of the projective model of its equation, induced by a section of the curve.
• 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 morphism to S with a map from S 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.PointedWeierstrassAtlas.of_projModelOver: a property of morphisms that is Zariski-local on the target and holds for projective Weierstrass models holds for a morphism with a pointed Weierstrass atlas; hence such a morphism is proper and smooth of relative dimension one, and its point is a section (PointedWeierstrassAtlas.isProper, PointedWeierstrassAtlas.smoothOfRelativeDimension, PointedWeierstrassAtlas.zero_comp).
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.smooth, EllipticCurveGeom.proper and EllipticCurveGeom.zero_comp: the structure morphism of an elliptic curve is smooth of relative dimension one and proper, and the zero section is a section of it.
• 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.

• EllipticCurveGeom.isClosed_setOf_left_apply_eq_zero: for any over-morphism into an elliptic curve, meeting its zero section is a closed condition.

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_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.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.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.

@[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.

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.

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).

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.restrict {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : PointedWeierstrassChart π zero

The restriction of a pointed Weierstrass chart c to an affine open V of its base: the chart with base V, coefficient ring Γ(base, V) and, as equation, the coefficient extension of the equation of c along ring ⟶ Γ(base, V). Its base is included in that of c by restrictι.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.restrictι {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : (c.restrict V).base ⟶ c.base

The inclusion of the base of the restriction c.restrict V into the base of c, an open immersion with image V (opensRange_restrictι).

instance TauCeti.AlgebraicGeometry.PointedWeierstrassChart.instIsOpenImmersionRestrictι {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : AlgebraicGeometry.IsOpenImmersion (c.restrictι V)

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.restrictι_baseMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : CategoryTheory.CategoryStruct.comp (c.restrictι V) c.baseMap = (c.restrict V).baseMap

The base of the restriction c.restrict V lies over the base of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.restrictι_baseMap_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.restrictι V) (CategoryTheory.CategoryStruct.comp c.baseMap h) = CategoryTheory.CategoryStruct.comp (c.restrict V).baseMap h

The base of the restriction c.restrict V lies over the base of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.opensRange_restrictι {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : AlgebraicGeometry.Scheme.Hom.opensRange (c.restrictι V) = ↑V

The image of the base of the restriction c.restrict V in the base of c is V.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.range_restrictι {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (V : ↑c.base.affineOpens) : Set.range ⇑(c.restrictι V) = ↑↑V

The image of the base of the restriction c.restrict V in the base of c is V, as a set of points.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : k.pullbackCarrier ⟶ c.pullbackCarrier

The morphism from the restriction of the curve to the base of a chart k to its restriction to the base of a chart c, induced by a morphism h of bases over S.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap_toTotal {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) c.toTotal = k.toTotal

The morphism pullbackCarrierMap lies over the inclusions into the curve.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap_toTotal_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) (CategoryTheory.CategoryStruct.comp c.toTotal h✝) = CategoryTheory.CategoryStruct.comp k.toTotal h✝

The morphism pullbackCarrierMap lies over the inclusions into the curve.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap_toBase {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) c.toBase = CategoryTheory.CategoryStruct.comp k.toBase h

The morphism pullbackCarrierMap lies over the morphism of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pullbackCarrierMap_toBase_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : c.base ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) (CategoryTheory.CategoryStruct.comp c.toBase h✝) = CategoryTheory.CategoryStruct.comp k.toBase (CategoryTheory.CategoryStruct.comp h h✝)

The morphism pullbackCarrierMap lies over the morphism of bases.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_pullbackCarrierMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.IsPullback (pullbackCarrierMap hh) k.toBase c.toBase h

The restriction of the curve to the base of k is the base change along h of its restriction to the base of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_pullbackCarrierMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp k.pulledZero (pullbackCarrierMap hh) = CategoryTheory.CategoryStruct.comp h c.pulledZero

The morphism pullbackCarrierMap carries the section induced by the zero section to the section induced by the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_pullbackCarrierMap_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : c.pullbackCarrier ⟶ Z) : CategoryTheory.CategoryStruct.comp k.pulledZero (CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) h✝) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp c.pulledZero h✝)

The morphism pullbackCarrierMap carries the section induced by the zero section to the section induced by the zero section.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : k.equation.projModel ⟶ c.equation.projModel

The morphism between the projective models of the equations of two charts k and c induced by a morphism h of bases over S: pullbackCarrierMap hh, read through the isomorphisms of the restrictions of the curve with the projective models (modelIso_hom_projModelMap). It lies over Spec k.ring ≅ k.base ⟶ c.base ≅ Spec c.ring, as a base change square (isPullback_projModelMap), and carries the zero section to the zero section (projModelZero_projModelMap).

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_hom_projModelMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp k.modelIso.hom (projModelMap hh) = CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) c.modelIso.hom

Through the isomorphisms with the projective models, projModelMap hh is pullbackCarrierMap hh.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_hom_projModelMap_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : c.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp k.modelIso.hom (CategoryTheory.CategoryStruct.comp (projModelMap hh) h✝) = CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) (CategoryTheory.CategoryStruct.comp c.modelIso.hom h✝)

Through the isomorphisms with the projective models, projModelMap hh is pullbackCarrierMap hh.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_projModelMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.IsPullback (projModelMap hh) k.equation.projModelOver c.equation.projModelOver (CategoryTheory.CategoryStruct.comp k.baseIso.inv (CategoryTheory.CategoryStruct.comp h c.baseIso.hom))

The projective model of the equation of k is the base change of that of c along Spec k.ring ≅ k.base ⟶ c.base ≅ Spec c.ring, through projModelMap hh.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_projModelMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp k.equation.projModelZero (projModelMap hh) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k.baseIso.inv (CategoryTheory.CategoryStruct.comp h c.baseIso.hom)) c.equation.projModelZero

The morphism projModelMap hh carries the zero section to the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_projModelMap_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : c.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp k.equation.projModelZero (CategoryTheory.CategoryStruct.comp (projModelMap hh) h✝) = CategoryTheory.CategoryStruct.comp k.baseIso.inv (CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp c.baseIso.hom (CategoryTheory.CategoryStruct.comp c.equation.projModelZero h✝)))

The morphism projModelMap hh carries the zero section to the zero section.

Sections on a chart

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : c.base ⟶ c.pullbackCarrier

The section of the restriction of X to the base of a chart c induced by a section P of π.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_toTotal {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) c.toTotal = CategoryTheory.CategoryStruct.comp c.baseMap P

The section chartPoint lies over the restriction of P to the base of the chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_toTotal_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) (CategoryTheory.CategoryStruct.comp c.toTotal h) = CategoryTheory.CategoryStruct.comp c.baseMap (CategoryTheory.CategoryStruct.comp P h)

The section chartPoint lies over the restriction of P to the base of the chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_toBase {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) c.toBase = CategoryTheory.CategoryStruct.id c.base

The morphism chartPoint is a section of the restriction of π.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_toBase_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Z : AlgebraicGeometry.Scheme} (h : c.base ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) (CategoryTheory.CategoryStruct.comp c.toBase h) = h

The morphism chartPoint is a section of the restriction of π.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_zero {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) : c.chartPoint hzero = c.pulledZero

The section induced by zero on a chart is the section pulledZero of the chart.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : AlgebraicGeometry.Spec c.ring ⟶ c.equation.projModel

The section of the projective model of the equation of a chart c induced by a section P of π: the section chartPoint read through Spec c.ring ≅ c.base and the isomorphism modelIso with the projective model.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_def {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : c.modelPoint hP = CategoryTheory.CategoryStruct.comp c.baseIso.inv (CategoryTheory.CategoryStruct.comp (c.chartPoint hP) c.modelIso.hom)

The model point is chartPoint, read through baseIso and modelIso.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_modelIso_hom {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) c.modelIso.hom = CategoryTheory.CategoryStruct.comp c.baseIso.hom (c.modelPoint hP)

Through the isomorphisms baseIso and modelIso, modelPoint is chartPoint.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.chartPoint_modelIso_hom_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Z : AlgebraicGeometry.Scheme} (h : c.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.chartPoint hP) (CategoryTheory.CategoryStruct.comp c.modelIso.hom h) = CategoryTheory.CategoryStruct.comp c.baseIso.hom (CategoryTheory.CategoryStruct.comp (c.modelPoint hP) h)

Through the isomorphisms baseIso and modelIso, modelPoint is chartPoint.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_projModelOver {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : CategoryTheory.CategoryStruct.comp (c.modelPoint hP) c.equation.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec c.ring)

The model point of a section is a section of the projective model.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_projModelOver_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↑c.ring ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.modelPoint hP) (CategoryTheory.CategoryStruct.comp c.equation.projModelOver h) = h

The model point of a section is a section of the projective model.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_modelIso_inv_toTotal {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) : CategoryTheory.CategoryStruct.comp (c.modelPoint hP) (CategoryTheory.CategoryStruct.comp c.modelIso.inv c.toTotal) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp c.baseIso.inv c.baseMap) P

The model point of a section P, carried back to X, is the restriction of P to the base of the chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_modelIso_inv_toTotal_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.modelPoint hP) (CategoryTheory.CategoryStruct.comp c.modelIso.inv (CategoryTheory.CategoryStruct.comp c.toTotal h)) = CategoryTheory.CategoryStruct.comp c.baseIso.inv (CategoryTheory.CategoryStruct.comp c.baseMap (CategoryTheory.CategoryStruct.comp P h))

The model point of a section P, carried back to X, is the restriction of P to the base of the chart.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_modelIso_inv_toTotal {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp c.modelIso.inv c.toTotal) c.equation.projModelOver π (CategoryTheory.CategoryStruct.comp c.baseIso.inv c.baseMap)

The projective model of the equation of a chart, mapped to X through modelIso and toTotal, is the base change of π along Spec c.ring ≅ c.base ⟶ S.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_modelIso_inv_toTotal {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.equation.projModelZero (CategoryTheory.CategoryStruct.comp c.modelIso.inv c.toTotal) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp c.baseIso.inv c.baseMap) zero

The zero section of the projective model, carried back to X, is the restriction of the section zero to the base of the chart.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_modelIso_inv_toTotal_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp c.equation.projModelZero (CategoryTheory.CategoryStruct.comp c.modelIso.inv (CategoryTheory.CategoryStruct.comp c.toTotal h)) = CategoryTheory.CategoryStruct.comp c.baseIso.inv (CategoryTheory.CategoryStruct.comp c.baseMap (CategoryTheory.CategoryStruct.comp zero h))

The zero section of the projective model, carried back to X, is the restriction of the section zero to the base of the chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_zero {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) (hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S) : c.modelPoint hzero = c.equation.projModelZero

The model point of the section zero is the zero section of the projective model.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_apply_ne_modelPoint {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {Q : S ⟶ X} (hQ : CategoryTheory.CategoryStruct.comp Q π = CategoryTheory.CategoryStruct.id S) (h : ∀ (s : ↥S), Q s ≠ P s) (s : ↥(AlgebraicGeometry.Spec c.ring)) : (c.modelPoint hQ) s ≠ (c.modelPoint hP) s

The model point of a section Q that differs from a section P at every point differs from the model point of P at every point.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_apply_ne {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) (h : ∀ (s : ↥S), P s ≠ zero s) (s : ↥(AlgebraicGeometry.Spec c.ring)) : (c.modelPoint hP) s ≠ c.equation.projModelZero s

The model point of a section P missing the section zero at every point misses the zero section of the projective model at every point.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_projModelMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {c : PointedWeierstrassChart π zero} {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {k : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp (k.modelPoint hP) (projModelMap hh) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k.baseIso.inv (CategoryTheory.CategoryStruct.comp h c.baseIso.hom)) (c.modelPoint hP)

Model points are compatible with the morphisms projModelMap between charts.

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.

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.openCover {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) : S.OpenCover

The bases of the charts of an atlas, as an open cover of S.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.openCover_I₀ {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) : A.openCover.I₀ = A.index

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.openCover_X {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) (i : A.openCover.I₀) : A.openCover.X i = (A.chart i).base

The scheme of A.openCover at an index is the base of the corresponding chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.openCover_f {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) (i : A.openCover.I₀) : A.openCover.f i = (A.chart i).baseMap

The map of A.openCover at an index is the base map of the corresponding chart.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.of_projModelOver {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P] (hP : ∀ (i : A.index), P (A.chart i).equation.projModelOver) : P π

A property of morphisms that is local on the target and holds for the projective models of the equations of the charts of an atlas holds for π.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.isProper {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) : AlgebraicGeometry.IsProper π

A morphism with a pointed Weierstrass atlas is proper.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.smoothOfRelativeDimension {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) : AlgebraicGeometry.SmoothOfRelativeDimension 1 π

A morphism with a pointed Weierstrass atlas is smooth of relative dimension one.

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

The point of a pointed Weierstrass atlas is a section.

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 with a map zero from S, 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. It implies that structureMap is smooth of relative dimension one and proper and that zero is a section of it (EllipticCurveGeom.smooth, EllipticCurveGeom.proper, EllipticCurveGeom.zero_comp).

• carrier : AlgebraicGeometry.Scheme

  The total space.

• structureMap : self.carrier ⟶ S

  The structure morphism.

• zero : S ⟶ self.carrier

  The zero section.

• 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 {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.zero E.structureMap = CategoryTheory.CategoryStruct.id S

The zero section is a section of the structure morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_comp_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 is a section of the structure morphism.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.smooth {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : AlgebraicGeometry.SmoothOfRelativeDimension 1 E.structureMap

The structure morphism is smooth of relative dimension one.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.proper {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : AlgebraicGeometry.IsProper E.structureMap

The structure morphism is proper.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClosedImmersion_zero {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : AlgebraicGeometry.IsClosedImmersion E.zero

The zero section of an elliptic curve is a closed immersion, being a section of the separated structure morphism.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.left_apply_mem_range_zero_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) (z : ↥Z.left) : (CategoryTheory.Over.Hom.left x) z ∈ Set.range ⇑E.zero ↔ (CategoryTheory.Over.Hom.left x) z = E.zero (Z.hom z)

A point x of E with values in a scheme Z over S takes a value in the image of the zero section at a point z of Z exactly when it agrees there with the zero section over the image of z in S.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClosed_setOf_left_apply_eq_zero {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) : IsClosed {z : ↥Z.left | (CategoryTheory.Over.Hom.left x) z = E.zero (Z.hom z)}

Meeting the zero section is a closed condition. For an over-morphism x from a scheme Z over S to an elliptic curve E, the points of Z at which x meets the zero section form a closed set: it is the preimage of the image of the zero section, a closed immersion.

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.