Base change of the projective Weierstrass model

Let W be a Weierstrass curve over a commutative ring R and f : R →+* R' a ring homomorphism. Extending the coefficients of homogeneous polynomials along f is a graded ring homomorphism from the homogeneous coordinate ring of W to that of W.map f; its Proj is a morphism projModel (W.map f) ⟶ projModel W of projective Weierstrass models. This file shows that it lies over Spec f : Spec R' ⟶ Spec R, that the resulting square is cartesian, so that projModel (W.map f) is the base change of projModel W along Spec f, and that it carries the zero section to the zero section. No ellipticity or flatness hypothesis is needed.

Base change along the identity is the identity, and base change along a composite is the composite of the base changes, up to W.map (RingHom.id R) = W and W.map (g.comp f) = (W.map f).map g. Along a ring isomorphism φ : R ≃+* R' the base change morphism is an isomorphism projModel (W.map φ) ≅ projModel W, since Spec φ is one.

Main definitions

• WeierstrassCurve.projModelBaseChange W f: the morphism projModel (W.map f) ⟶ projModel W induced by extending coefficients along f.
• WeierstrassCurve.projModelMapIso W φ: for a ring isomorphism φ : R ≃+* R', the base change morphism along φ as an isomorphism projModel (W.map φ) ≅ projModel W.

Main results

• WeierstrassCurve.projModelBaseChange_projModelOver: the base change morphism lies over Spec f.
• WeierstrassCurve.isPullback_projModelBaseChange: the square formed by the base change morphism, the structure morphisms and Spec f is a pullback square.
• WeierstrassCurve.projModelZero_projModelBaseChange: the base change morphism carries the zero section to the zero section.
• WeierstrassCurve.projModelBaseChange_id and WeierstrassCurve.projModelBaseChange_comp: base change is compatible with the identity and with composition of ring homomorphisms.
• WeierstrassCurve.isIso_projModelBaseChange: base change along a ring isomorphism is an isomorphism.
• WeierstrassCurve.inv_projModelBaseChange_projModelOver and WeierstrassCurve.projModelZero_inv_projModelBaseChange: the inverse of the base change morphism along a ring isomorphism φ lies over Spec φ.symm and carries the zero section to the zero section.
• WeierstrassCurve.projModelMapIso_refl and WeierstrassCurve.projModelMapIso_trans: the isomorphisms induced by ring isomorphisms are compatible with the identity and with composition.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.
• The Stacks Project, Lemma 27.11.6

Provenance

projModelBaseChange, isPullback_projModelBaseChange and projModelZero_projModelBaseChange are adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/WeierstrassModel.lean, sections BaseChangeGraded and TensorComparison (declarations mvMapGraded, baseChangeGradedHom, projModelBaseChange, projModelBaseChange_π, sChartTensorEquiv, isPullback_sChart_spec, isPullback_projModelBaseChange_chart, projModelBaseChangeLift_isIso and isPullback_projModelBaseChange) and the zero-section compatibility projModelZero_baseChange. AINTLIB states the cartesian square for an R-algebra R'; here f is an arbitrary ring homomorphism and the model is the Proj of WeierstrassCurve.Projective.CoordinateRing.

noncomputable def WeierstrassCurve.projModelBaseChange {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') : (W.map f).projModel ⟶ W.projModel

The base change morphism projModel (W.map f) ⟶ projModel W of projective Weierstrass models along a ring homomorphism f : R →+* R': Proj of the graded ring homomorphism of homogeneous coordinate rings induced by MvPolynomial.map f. It exhibits projModel (W.map f) as the base change of projModel W along Spec f (isPullback_projModelBaseChange).

Equations

• W.projModelBaseChange f = AlgebraicGeometry.Proj.map (WeierstrassCurve.baseChangeGradedHom✝ W f) ⋯

The cartesian square

theorem WeierstrassCurve.isPullback_projModelBaseChange {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') : CategoryTheory.IsPullback (W.projModelBaseChange f) (W.map f).projModelOver W.projModelOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))

The projective Weierstrass model of W.map f is the base change of the projective Weierstrass model of W along Spec f : Spec R' ⟶ Spec R: the square formed by the base change morphism, the two structure morphisms and Spec f is a pullback square.

@[simp]

theorem WeierstrassCurve.projModelBaseChange_projModelOver {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') : CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) W.projModelOver = CategoryTheory.CategoryStruct.comp (W.map f).projModelOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))

The base change morphism lies over Spec f : Spec R' ⟶ Spec R.

@[simp]

theorem WeierstrassCurve.projModelBaseChange_projModelOver_assoc {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (W.map f).projModelOver (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) h)

The base change morphism lies over Spec f : Spec R' ⟶ Spec R.

The zero section

@[simp]

theorem WeierstrassCurve.projModelZero_projModelBaseChange {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') : CategoryTheory.CategoryStruct.comp (W.map f).projModelZero (W.projModelBaseChange f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) W.projModelZero

The base change morphism carries the zero section [0 : 1 : 0] of projModel (W.map f) to the zero section of projModel W.

@[simp]

theorem WeierstrassCurve.projModelZero_projModelBaseChange_assoc {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.map f).projModelZero (CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) (CategoryTheory.CategoryStruct.comp W.projModelZero h)

The base change morphism carries the zero section [0 : 1 : 0] of projModel (W.map f) to the zero section of projModel W.

Identity and composition

@[simp]

theorem WeierstrassCurve.projModelBaseChange_id {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.projModelBaseChange (RingHom.id R) = CategoryTheory.eqToHom ⋯

Base change along the identity of R is the identity of the projective Weierstrass model, up to W.map (RingHom.id R) = W.

@[simp]

theorem WeierstrassCurve.projModelBaseChange_comp {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (f : R →+* R') {R'' : Type u} [CommRing R''] (g : R' →+* R'') : W.projModelBaseChange (g.comp f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((W.map f).projModelBaseChange g) (W.projModelBaseChange f))

Base change along a composite g.comp f is base change along g followed by base change along f, up to W.map (g.comp f) = (W.map f).map g.

Base change along a ring isomorphism

instance WeierstrassCurve.isIso_projModelBaseChange {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : CategoryTheory.IsIso (W.projModelBaseChange ↑φ)

Base change along a ring isomorphism is an isomorphism of projective Weierstrass models: it is the base change of Spec φ, an isomorphism, in the pullback square isPullback_projModelBaseChange.

noncomputable def WeierstrassCurve.projModelMapIso {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : (W.map ↑φ).projModel ≅ W.projModel

The isomorphism projModel (W.map φ) ≅ projModel W of projective Weierstrass models induced by a ring isomorphism φ : R ≃+* R': the base change morphism along φ.

Equations

• W.projModelMapIso φ = CategoryTheory.asIso (W.projModelBaseChange ↑φ)

@[simp]

theorem WeierstrassCurve.projModelMapIso_hom {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : (W.projModelMapIso φ).hom = W.projModelBaseChange ↑φ

The forward map of projModelMapIso W φ is the base change morphism along φ.

@[simp]

theorem WeierstrassCurve.projModelMapIso_inv {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : (W.projModelMapIso φ).inv = CategoryTheory.inv (W.projModelBaseChange ↑φ)

The inverse of projModelMapIso W φ is the inverse of the base change morphism along φ.

@[simp]

theorem WeierstrassCurve.inv_projModelBaseChange_projModelOver {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (W.projModelBaseChange ↑φ)) (W.map ↑φ).projModelOver = CategoryTheory.CategoryStruct.comp W.projModelOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑φ.symm))

The inverse of the base change morphism along a ring isomorphism φ : R ≃+* R' lies over Spec φ.symm : Spec R ⟶ Spec R'.

@[simp]

theorem WeierstrassCurve.inv_projModelBaseChange_projModelOver_assoc {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (W.projModelBaseChange ↑φ)) (CategoryTheory.CategoryStruct.comp (W.map ↑φ).projModelOver h) = CategoryTheory.CategoryStruct.comp W.projModelOver (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑φ.symm)) h)

The inverse of the base change morphism along a ring isomorphism φ : R ≃+* R' lies over Spec φ.symm : Spec R ⟶ Spec R'.

@[simp]

theorem WeierstrassCurve.projModelZero_inv_projModelBaseChange {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') : CategoryTheory.CategoryStruct.comp W.projModelZero (CategoryTheory.inv (W.projModelBaseChange ↑φ)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑φ.symm)) (W.map ↑φ).projModelZero

The inverse of the base change morphism along a ring isomorphism φ : R ≃+* R' carries the zero section to the zero section, over Spec φ.symm : Spec R ⟶ Spec R'.

@[simp]

theorem WeierstrassCurve.projModelZero_inv_projModelBaseChange_assoc {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') {Z : AlgebraicGeometry.Scheme} (h : (W.map ↑φ).projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelZero (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (W.projModelBaseChange ↑φ)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑φ.symm)) (CategoryTheory.CategoryStruct.comp (W.map ↑φ).projModelZero h)

The inverse of the base change morphism along a ring isomorphism φ : R ≃+* R' carries the zero section to the zero section, over Spec φ.symm : Spec R ⟶ Spec R'.

@[simp]

theorem WeierstrassCurve.projModelMapIso_refl {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.projModelMapIso (RingEquiv.refl R) = CategoryTheory.eqToIso ⋯

The identity ring isomorphism induces the identity of the projective Weierstrass model, up to W.map (RingHom.id R) = W.

@[simp]

theorem WeierstrassCurve.projModelMapIso_trans {R R' : Type u} [CommRing R] [CommRing R'] (W : WeierstrassCurve R) (φ : R ≃+* R') {R'' : Type u} [CommRing R''] (ψ : R' ≃+* R'') : W.projModelMapIso (φ.trans ψ) = CategoryTheory.eqToIso ⋯ ≪≫ (W.map ↑φ).projModelMapIso ψ ≪≫ W.projModelMapIso φ

The isomorphism induced by a composite φ.trans ψ is the isomorphism induced by ψ followed by the one induced by φ, up to W.map (ψ.comp φ) = (W.map φ).map ψ.