Base change of elliptic curves over a scheme

Let E be an elliptic curve over a scheme S, in the sense of EllipticCurveGeom, and f : T ⟶ S a morphism of schemes. The base change E.baseChange f is the elliptic curve over T whose total space is the pullback of the structure morphism of E along f, with the second projection as structure morphism and the section induced by f ≫ E.zero as zero section. Smoothness of relative dimension one, properness and the local-model condition IsLocallyWeierstrass for a morphism with a section are stable under base change.

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChange E f: the base change of an elliptic curve E over S along f : T ⟶ S.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeIso E f: the identification of the total space of E.baseChange f with the pullback of E.structureMap along f, compatible with the structure morphisms (baseChangeIso_hom_snd) and the zero sections (zero_baseChangeIso_hom).
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap E k hk: the canonical morphism between base changes induced by a morphism k of bases over S.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift hg₁ hg₂ hh: for a base change square hg₁ of E along u : T₁ ⟶ S, a morphism from an elliptic curve E₂ to E over v : T₂ ⟶ S and h : T₂ ⟶ T₁ with h ≫ u = v, the induced morphism E₂ ⟶ E₁ over h; it is a base change square when g₂ also exhibits a base change (isPullback_baseChangeLift), and preserves zero sections when both g₁ and g₂ preserve them (zero_baseChangeLift).
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.carrierMap hg hh and TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelMap hg hh: for a base change square hg of a morphism with a section, and charts k and c of its two sides whose bases are related by a morphism over the base change, the induced morphism between the restrictions to the chart bases, and the same morphism between the projective models of their equations.

Main results

• TauCeti.AlgebraicGeometry.IsLocallyWeierstrass.baseChange: the local-model condition for a morphism with a section is stable under base change.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_baseChange: the base change of E along f is a pullback of the structure morphism of E along f.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_id and TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_comp: the canonical morphisms between base changes preserve identities and composition.
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_modelMap and TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_modelMap: the morphism modelMap hg hh is a base change square of projective models carrying the zero section to the zero section. Statements about the projective models of Weierstrass equations which are compatible with such squares therefore pass to elliptic curves along base change squares.
• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_modelMap_of_comp_eq: if an endomorphism of X over S fixes a section, the induced endomorphism of the projective model of a chart fixes its model point.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_chart_comp_baseMap: for elliptic curves over S and S' and a morphism f : S' ⟶ S, the charts of the curve over S' whose bases map over f into bases of charts of the curve over S cover S'.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a. IsLocallyWeierstrass.baseChange is ModularCurves.LocallyWeierstrass.baseChange in projects/ModularCurves/ModularCurves/EllipticCurve/Basic.lean; the fields of EllipticCurveGeom.baseChange are those of ModularCurves.EllipticCurve.baseChange in projects/ModularCurves/ModularCurves/EllipticCurve/GroupLaw.lean, without the group structure. AINTLIB's Weierstrass model over V extends coefficients along an Algebra instance built from g.appLE U V _; here it is W.map (g.appLE U V _).hom.

The local-model condition under base change

theorem TauCeti.AlgebraicGeometry.IsLocallyWeierstrass.baseChange {X S T : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {hzero : CategoryTheory.CategoryStruct.comp zero π = CategoryTheory.CategoryStruct.id S} (h : IsLocallyWeierstrass π zero hzero) (g : T ⟶ S) : IsLocallyWeierstrass (CategoryTheory.Limits.pullback.snd π g) (CategoryTheory.Limits.pullbackSection π g (CategoryTheory.CategoryStruct.comp g zero) ⋯) ⋯

The local-model condition is stable under base change: if a morphism π : X ⟶ S with the section zero satisfies IsLocallyWeierstrass, then so does its base change pullback.snd π g along any g : T ⟶ S, with the section induced by g ≫ zero.

Base change of elliptic curves

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChange {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) : EllipticCurveGeom T

The base change of an elliptic curve E over S along a morphism f : T ⟶ S: the total space is the pullback of E.structureMap along f, the structure morphism is the second projection, and the zero section is the section induced by f ≫ E.zero (see baseChangeIso).

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeIso {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) : (E.baseChange f).carrier ≅ CategoryTheory.Limits.pullback E.structureMap f

The isomorphism identifying the total space of E.baseChange f with the pullback of E.structureMap along f. Under it, the structure morphism of E.baseChange f is the second projection (baseChangeIso_hom_snd) and its zero section is the section induced by f ≫ E.zero (zero_baseChangeIso_hom).

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeIso_hom_snd {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.Limits.pullback.snd E.structureMap f) = (E.baseChange f).structureMap

Under baseChangeIso, the structure morphism of E.baseChange f is the second projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeIso_hom_snd_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) {Z : AlgebraicGeometry.Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd E.structureMap f) h) = CategoryTheory.CategoryStruct.comp (E.baseChange f).structureMap h

Under baseChangeIso, the structure morphism of E.baseChange f is the second projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeIso_hom {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (E.baseChange f).zero (E.baseChangeIso f).hom = CategoryTheory.Limits.pullbackSection E.structureMap f (CategoryTheory.CategoryStruct.comp f E.zero) ⋯

Under baseChangeIso, the zero section of E.baseChange f is the section of the pullback induced by f ≫ E.zero.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeIso_hom_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback E.structureMap f ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChange f).zero (CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSection E.structureMap f (CategoryTheory.CategoryStruct.comp f E.zero) ⋯) h

Under baseChangeIso, the zero section of E.baseChange f is the section of the pullback induced by f ≫ E.zero.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_baseChange {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (f : T ⟶ S) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.Limits.pullback.fst E.structureMap f)) (E.baseChange f).structureMap E.structureMap f

The base change E.baseChange f is a pullback of the structure morphism of E along f: the square formed by the projection (E.baseChangeIso f).hom ≫ pullback.fst _ _ to E, the two structure morphisms and f is a pullback square.

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') : (E.baseChange f').carrier ⟶ (E.baseChange f).carrier

The canonical morphism between base changes of E induced by a morphism k : T' ⟶ T over S. On the pullback models it is the identity on E.carrier and k on the bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_baseChangeIso_hom {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') : CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) (E.baseChangeIso f).hom = CategoryTheory.CategoryStruct.comp (E.baseChangeIso f').hom (CategoryTheory.Limits.pullback.mapSnd E.structureMap f f' k hk)

On the pullback models, baseChangeMap is pullback.mapSnd: it is the identity on the elliptic curve and the given morphism on the bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_baseChangeIso_hom_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback E.structureMap f ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) (CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom h) = CategoryTheory.CategoryStruct.comp (E.baseChangeIso f').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.mapSnd E.structureMap f f' k hk) h)

On the pullback models, baseChangeMap is pullback.mapSnd: it is the identity on the elliptic curve and the given morphism on the bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_structureMap {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') : CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) (E.baseChange f).structureMap = CategoryTheory.CategoryStruct.comp (E.baseChange f').structureMap k

The canonical morphism between base changes lies over the given morphism of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_structureMap_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') {Z : AlgebraicGeometry.Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) (CategoryTheory.CategoryStruct.comp (E.baseChange f).structureMap h) = CategoryTheory.CategoryStruct.comp (E.baseChange f').structureMap (CategoryTheory.CategoryStruct.comp k h)

The canonical morphism between base changes lies over the given morphism of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeMap {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') : CategoryTheory.CategoryStruct.comp (E.baseChange f').zero (E.baseChangeMap k hk) = CategoryTheory.CategoryStruct.comp k (E.baseChange f).zero

The canonical morphism between base changes carries the pulled-back zero section to the pulled-back zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeMap_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') {Z : AlgebraicGeometry.Scheme} (h : (E.baseChange f).carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChange f').zero (CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) h) = CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp (E.baseChange f).zero h)

The canonical morphism between base changes carries the pulled-back zero section to the pulled-back zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_id {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {f : T ⟶ S} : E.baseChangeMap (CategoryTheory.CategoryStruct.id T) ⋯ = CategoryTheory.CategoryStruct.id (E.baseChange f).carrier

Base change along the identity morphism induces the identity morphism of the base-changed elliptic curve.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_comp {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' T'' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} {f'' : T'' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') (l : T'' ⟶ T') (hl : CategoryTheory.CategoryStruct.comp l f' = f'') : CategoryTheory.CategoryStruct.comp (E.baseChangeMap l hl) (E.baseChangeMap k hk) = E.baseChangeMap (CategoryTheory.CategoryStruct.comp l k) ⋯

The canonical morphisms between base changes are compatible with composition of morphisms of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeMap_comp_assoc {S T : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {T' T'' : AlgebraicGeometry.Scheme} {f : T ⟶ S} {f' : T' ⟶ S} {f'' : T'' ⟶ S} (k : T' ⟶ T) (hk : CategoryTheory.CategoryStruct.comp k f = f') (l : T'' ⟶ T') (hl : CategoryTheory.CategoryStruct.comp l f' = f'') {Z : AlgebraicGeometry.Scheme} (h : (E.baseChange f).carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.baseChangeMap l hl) (CategoryTheory.CategoryStruct.comp (E.baseChangeMap k hk) h) = CategoryTheory.CategoryStruct.comp (E.baseChangeMap (CategoryTheory.CategoryStruct.comp l k) ⋯) h

The canonical morphisms between base changes are compatible with composition of morphisms of bases.

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) : E₂.carrier ⟶ E₁.carrier

Let g₁ : E₁ ⟶ E exhibit the elliptic curve E₁ over T₁ as a base change of E along u : T₁ ⟶ S, and let g₂ : E₂ ⟶ E be a morphism from an elliptic curve E₂ over T₂ lying over v : T₂ ⟶ S. Given h : T₂ ⟶ T₁ with h ≫ u = v, this is the induced morphism E₂ ⟶ E₁ lying over h, compatibly with g₁ and g₂. When g₂ is also a base change square, so is this morphism (isPullback_baseChangeLift), and it preserves zero sections when g₁ and g₂ do (zero_baseChangeLift).

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift_fst {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) : CategoryTheory.CategoryStruct.comp (baseChangeLift hg₁ hg₂ hh) g₁ = g₂

The morphism baseChangeLift hg₁ hg₂ hh is compatible with the morphisms g₁ and g₂ to E.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift_fst_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) {Z : AlgebraicGeometry.Scheme} (h✝ : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeLift hg₁ hg₂ hh) (CategoryTheory.CategoryStruct.comp g₁ h✝) = CategoryTheory.CategoryStruct.comp g₂ h✝

The morphism baseChangeLift hg₁ hg₂ hh is compatible with the morphisms g₁ and g₂ to E.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift_structureMap {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) : CategoryTheory.CategoryStruct.comp (baseChangeLift hg₁ hg₂ hh) E₁.structureMap = CategoryTheory.CategoryStruct.comp E₂.structureMap h

The morphism baseChangeLift hg₁ hg₂ hh lies over the morphism h of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseChangeLift_structureMap_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) {Z : AlgebraicGeometry.Scheme} (h✝ : T₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeLift hg₁ hg₂ hh) (CategoryTheory.CategoryStruct.comp E₁.structureMap h✝) = CategoryTheory.CategoryStruct.comp E₂.structureMap (CategoryTheory.CategoryStruct.comp h h✝)

The morphism baseChangeLift hg₁ hg₂ hh lies over the morphism h of bases.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_baseChangeLift {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.IsPullback g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) : CategoryTheory.IsPullback (baseChangeLift hg₁ ⋯ hh) E₂.structureMap E₁.structureMap h

If g₂ exhibits E₂ as a base change of E, then baseChangeLift exhibits E₂ as the base change of E₁ along h.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeLift {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) (h0₁ : CategoryTheory.CategoryStruct.comp E₁.zero g₁ = CategoryTheory.CategoryStruct.comp u E.zero) (h0₂ : CategoryTheory.CategoryStruct.comp E₂.zero g₂ = CategoryTheory.CategoryStruct.comp v E.zero) : CategoryTheory.CategoryStruct.comp E₂.zero (baseChangeLift hg₁ hg₂ hh) = CategoryTheory.CategoryStruct.comp h E₁.zero

If g₁ and g₂ carry the zero sections of E₁ and E₂ to that of E, then baseChangeLift hg₁ hg₂ hh carries the zero section of E₂ to that of E₁.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_baseChangeLift_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {T₁ T₂ : AlgebraicGeometry.Scheme} {E₁ : EllipticCurveGeom T₁} {E₂ : EllipticCurveGeom T₂} {g₁ : E₁.carrier ⟶ E.carrier} {u : T₁ ⟶ S} (hg₁ : CategoryTheory.IsPullback g₁ E₁.structureMap E.structureMap u) {g₂ : E₂.carrier ⟶ E.carrier} {v : T₂ ⟶ S} {h : T₂ ⟶ T₁} (hg₂ : CategoryTheory.CommSq g₂ E₂.structureMap E.structureMap v) (hh : CategoryTheory.CategoryStruct.comp h u = v) (h0₁ : CategoryTheory.CategoryStruct.comp E₁.zero g₁ = CategoryTheory.CategoryStruct.comp u E.zero) (h0₂ : CategoryTheory.CategoryStruct.comp E₂.zero g₂ = CategoryTheory.CategoryStruct.comp v E.zero) {Z : AlgebraicGeometry.Scheme} (h✝ : E₁.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp E₂.zero (CategoryTheory.CategoryStruct.comp (baseChangeLift hg₁ hg₂ hh) h✝) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp E₁.zero h✝)

If g₁ and g₂ carry the zero sections of E₁ and E₂ to that of E, then baseChangeLift hg₁ hg₂ hh carries the zero section of E₂ to that of E₁.

Charts over a base change square

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

Let g : X' ⟶ X be the base change of π : X ⟶ S along f : S' ⟶ S, and let k and c be pointed Weierstrass charts of π' and π whose bases are related by h : k.base ⟶ c.base over f. This is the morphism from the restriction of X' to the base of k to the restriction of X to the base of c induced by g, lying over h. It generalizes pullbackCarrierMap, the case f = 𝟙 S and g = 𝟙 X.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.carrierMap_toTotal {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) : CategoryTheory.CategoryStruct.comp (carrierMap hg hh) c.toTotal = CategoryTheory.CategoryStruct.comp k.toTotal g

The morphism carrierMap hg hh lies over g.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.carrierMap_toTotal_assoc {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) {Z : AlgebraicGeometry.Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (carrierMap hg hh) (CategoryTheory.CategoryStruct.comp c.toTotal h✝) = CategoryTheory.CategoryStruct.comp k.toTotal (CategoryTheory.CategoryStruct.comp g h✝)

The morphism carrierMap hg hh lies over g.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.carrierMap_toBase {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) : CategoryTheory.CategoryStruct.comp (carrierMap hg hh) c.toBase = CategoryTheory.CategoryStruct.comp k.toBase h

The morphism carrierMap hg hh lies over the morphism h of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.carrierMap_toBase_assoc {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) {Z : AlgebraicGeometry.Scheme} (h✝ : c.base ⟶ Z) : CategoryTheory.CategoryStruct.comp (carrierMap hg hh) (CategoryTheory.CategoryStruct.comp c.toBase h✝) = CategoryTheory.CategoryStruct.comp k.toBase (CategoryTheory.CategoryStruct.comp h h✝)

The morphism carrierMap hg hh lies over the morphism h of bases.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_carrierMap {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) : CategoryTheory.IsPullback (carrierMap hg hh) k.toBase c.toBase h

The restriction of X' to the base of k is the base change along h of the restriction of X to the base of c, through carrierMap hg hh.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_carrierMap {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) (h0 : CategoryTheory.CategoryStruct.comp zero' g = CategoryTheory.CategoryStruct.comp f zero) : CategoryTheory.CategoryStruct.comp k.pulledZero (carrierMap hg hh) = CategoryTheory.CategoryStruct.comp h c.pulledZero

If g carries the section zero' to zero, then carrierMap hg hh carries the section of k induced by zero' to the section of c induced by zero.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_carrierMap_assoc {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) (h0 : CategoryTheory.CategoryStruct.comp zero' g = CategoryTheory.CategoryStruct.comp f zero) {Z : AlgebraicGeometry.Scheme} (h✝ : c.pullbackCarrier ⟶ Z) : CategoryTheory.CategoryStruct.comp k.pulledZero (CategoryTheory.CategoryStruct.comp (carrierMap hg hh) h✝) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp c.pulledZero h✝)

If g carries the section zero' to zero, then carrierMap hg hh carries the section of k induced by zero' to the section of c induced by zero.

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

The morphism carrierMap hg hh between the restrictions of X' and X to the bases of k and c, read through the isomorphisms of these restrictions with the projective models of the equations of k and c (modelIso_hom_modelMap). It is a base change square of projective models (isPullback_modelMap) and, when g preserves the sections, carries the zero section to the zero section (projModelZero_modelMap).

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_hom_modelMap {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) : CategoryTheory.CategoryStruct.comp k.modelIso.hom (modelMap hg hh) = CategoryTheory.CategoryStruct.comp (carrierMap hg hh) c.modelIso.hom

Through the isomorphisms with the projective models, modelMap hg hh is carrierMap hg hh.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelIso_hom_modelMap_assoc {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) {Z : AlgebraicGeometry.Scheme} (h✝ : c.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp k.modelIso.hom (CategoryTheory.CategoryStruct.comp (modelMap hg hh) h✝) = CategoryTheory.CategoryStruct.comp (carrierMap hg hh) (CategoryTheory.CategoryStruct.comp c.modelIso.hom h✝)

Through the isomorphisms with the projective models, modelMap hg hh is carrierMap hg hh.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.isPullback_modelMap {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) : CategoryTheory.IsPullback (modelMap hg 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 modelMap hg hh.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.projModelZero_modelMap {S X S' X' : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {π' : X' ⟶ S'} {zero' : S' ⟶ X'} {g : X' ⟶ X} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g π' π f) {k : PointedWeierstrassChart π' zero'} {c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f) (h0 : CategoryTheory.CategoryStruct.comp zero' g = CategoryTheory.CategoryStruct.comp f zero) : CategoryTheory.CategoryStruct.comp k.equation.projModelZero (modelMap hg hh) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k.baseIso.inv (CategoryTheory.CategoryStruct.comp h c.baseIso.hom)) c.equation.projModelZero

If g carries the section zero' to zero, then modelMap hg hh carries the zero section of the projective model of the equation of k to that of c.

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.modelPoint_modelMap_of_comp_eq {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {P : S ⟶ X} (hP : CategoryTheory.CategoryStruct.comp P π = CategoryTheory.CategoryStruct.id S) {σ : X ⟶ X} (hσ : CategoryTheory.IsPullback σ π π (CategoryTheory.CategoryStruct.id S)) (hσP : CategoryTheory.CategoryStruct.comp P σ = P) : CategoryTheory.CategoryStruct.comp (c.modelPoint hP) (modelMap hσ ⋯) = c.modelPoint hP

If an endomorphism σ of X over S, cartesian over the identity, fixes a section P, then the induced endomorphism of the projective model of the chart fixes the model point of P.

Charts compatible with a morphism of bases

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_chart_comp_baseMap {S S' : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (E' : EllipticCurveGeom S') (f : S' ⟶ S) (s : ↥S') : ∃ (k : PointedWeierstrassChart E'.structureMap E'.zero) (c : PointedWeierstrassChart E.structureMap E.zero) (h : k.base ⟶ c.base), CategoryTheory.CategoryStruct.comp h c.baseMap = CategoryTheory.CategoryStruct.comp k.baseMap f ∧ s ∈ Set.range ⇑k.baseMap

Charts compatible with a morphism of bases. For elliptic curves E over S and E' over S' and a morphism f : S' ⟶ S, every point of S' lies in the base of a pointed Weierstrass chart k of E' whose base maps over f into the base of a pointed Weierstrass chart c of E. The chart k can be taken to be the restriction of any chart of E' around the point to an affine open.