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

Main results

• TauCeti.AlgebraicGeometry.IsLocallyWeierstrass.baseChange: the local-model condition for a morphism with a section is stable under base change.

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

Equations

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

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

Equations

• E.baseChangeIso f = CategoryTheory.Iso.refl (E.baseChange f).carrier

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