Charts of the projective Weierstrass model

Let W be a Weierstrass curve over a commutative ring R, let E = projModel W be its projective model and let S = Spec R. This file presents the standard affine chart D₊(Xᵢ) of E as an open immersion from the spectrum of the chart ring ChartRing i = R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1), and the product D₊(Xᵢ) ×_S D₊(Xⱼ) of two charts as an open immersion from the spectrum of ChartRing i ⊗[R] ChartRing j into E ×_S E.

Main definitions

• WeierstrassCurve.chartι W i: the chart D₊(Xᵢ), an open immersion Spec (ChartRing i) ⟶ projModel W.
• WeierstrassCurve.chartPairι W i j: the product of the charts D₊(Xᵢ) and D₊(Xⱼ), an open immersion Spec (ChartRing i ⊗[R] ChartRing j) ⟶ E ×_S E.

Main results

• WeierstrassCurve.exists_mem_range_chartι: the three charts cover the projective model.
• WeierstrassCurve.chartι_projModelOver: on the chart D₊(Xᵢ), the structure morphism of the projective model is Spec of the structure map R → ChartRing i.
• WeierstrassCurve.chartPairι_fst and WeierstrassCurve.chartPairι_snd: the two projections of E ×_S E on the product of two charts.
• WeierstrassCurve.SpecMap_desc_chartPairι: the point of the product of two charts given by two homomorphisms out of the chart rings that agree on R is the point of E ×_S E with the corresponding points of the two charts as components.
• WeierstrassCurve.range_chartPairι: the product of two charts is the locus in E ×_S E whose projections lie on the two charts.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/AdditionChartSpec.lean: chartι, chartι_projModelπ, and chartPieceTensorIso with its _inv_fst and _inv_snd lemmas, as chartι, chartι_projModelOver, chartPairι, chartPairι_fst and chartPairι_snd. Here the chart is read through WeierstrassCurve.Projective.awayEquivChartRing, and the product of two charts is an open immersion into E ×_S E rather than an isomorphism with a pullback. From the file AdditionSpecPoints.lean of the same directory: specMap_pieceAwayZι_fst, specMap_pieceAwayZι_snd, specMap_pieceAwayι_fst and specMap_pieceAwayι_snd, as SpecMap_desc_chartPairι. The source computes the two projections of a point of a piece of its cover through the left and right inclusions of the tensor product; here a point of the product of two charts is built from its two components through the pushout property of the tensor product.

noncomputable def WeierstrassCurve.chartι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : AlgebraicGeometry.Spec ↧(W.toProjective.ChartRing i) ⟶ W.projModel

The standard affine chart D₊(Xᵢ) of the projective Weierstrass model, as a morphism Spec (ChartRing i) ⟶ projModel W from the spectrum of R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1).

Equations

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

theorem WeierstrassCurve.chartι_def {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : W.chartι i = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(W.toProjective.awayEquivChartRing i))) (AlgebraicGeometry.Proj.awayι W.toProjective.grading (W.toProjective.coord i) ⋯ ⋯)

The chart D₊(Xᵢ) is Spec of the isomorphism awayEquivChartRing from the degree-zero part A_(Xᵢ) of the localization away from Xᵢ to the chart ring, followed by the inclusion Proj.awayι of D₊(Xᵢ) into the projective model. The body of chartι is not exposed; this lemma unfolds it.

instance WeierstrassCurve.isOpenImmersion_chartι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : AlgebraicGeometry.IsOpenImmersion (W.chartι i)

The chart D₊(Xᵢ) of the projective model is an open immersion.

theorem WeierstrassCurve.exists_mem_range_chartι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (y : ↥W.projModel) : ∃ (i : Fin 3), y ∈ Set.range ⇑(W.chartι i)

The charts D₊(X₀), D₊(X₁) and D₊(X₂) cover the projective model.

@[simp]

theorem WeierstrassCurve.chartι_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : CategoryTheory.CategoryStruct.comp (W.chartι i) W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (W.toProjective.ChartRing i)))

On the chart D₊(Xᵢ), the structure morphism of the projective model is Spec of the structure map R → ChartRing i.

@[simp]

theorem WeierstrassCurve.chartι_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.chartι i) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (W.toProjective.ChartRing i)))) h

On the chart D₊(Xᵢ), the structure morphism of the projective model is Spec of the structure map R → ChartRing i.

noncomputable def WeierstrassCurve.chartPairι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) : AlgebraicGeometry.Spec ↧(TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)) ⟶ CategoryTheory.Limits.pullback W.projModelOver W.projModelOver

The product D₊(Xᵢ) ×_S D₊(Xⱼ) of two standard affine charts of E = projModel W over S = Spec R, as a morphism Spec (ChartRing i ⊗[R] ChartRing j) ⟶ E ×_S E. It is an open immersion (isOpenImmersion_chartPairι), and its composites with the two projections of E ×_S E are given by chartPairι_fst and chartPairι_snd.

Equations

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

instance WeierstrassCurve.isOpenImmersion_chartPairι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) : AlgebraicGeometry.IsOpenImmersion (W.chartPairι i j)

The product of two charts is an open immersion into E ×_S E.

@[simp]

theorem WeierstrassCurve.chartPairι_fst {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) : CategoryTheory.CategoryStruct.comp (W.chartPairι i j) (CategoryTheory.Limits.pullback.fst W.projModelOver W.projModelOver) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (W.chartι i)

Composing the product chartPairι W i j of the charts D₊(Xᵢ) and D₊(Xⱼ) with the first projection E ×_S E ⟶ E gives Spec of the inclusion a ↦ a ⊗ₜ 1 of ChartRing i into ChartRing i ⊗[R] ChartRing j, followed by the chart D₊(Xᵢ).

@[simp]

theorem WeierstrassCurve.chartPairι_fst_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.chartPairι i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst W.projModelOver W.projModelOver) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (CategoryTheory.CategoryStruct.comp (W.chartι i) h)

Composing the product chartPairι W i j of the charts D₊(Xᵢ) and D₊(Xⱼ) with the first projection E ×_S E ⟶ E gives Spec of the inclusion a ↦ a ⊗ₜ 1 of ChartRing i into ChartRing i ⊗[R] ChartRing j, followed by the chart D₊(Xᵢ).

@[simp]

theorem WeierstrassCurve.chartPairι_snd {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) : CategoryTheory.CategoryStruct.comp (W.chartPairι i j) (CategoryTheory.Limits.pullback.snd W.projModelOver W.projModelOver) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)) (W.chartι j)

Composing the product chartPairι W i j of the charts D₊(Xᵢ) and D₊(Xⱼ) with the second projection E ×_S E ⟶ E gives Spec of the inclusion b ↦ 1 ⊗ₜ b of ChartRing j into ChartRing i ⊗[R] ChartRing j, followed by the chart D₊(Xⱼ).

@[simp]

theorem WeierstrassCurve.chartPairι_snd_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.chartPairι i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd W.projModelOver W.projModelOver) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)) (CategoryTheory.CategoryStruct.comp (W.chartι j) h)

Composing the product chartPairι W i j of the charts D₊(Xᵢ) and D₊(Xⱼ) with the second projection E ×_S E ⟶ E gives Spec of the inclusion b ↦ 1 ⊗ₜ b of ChartRing j into ChartRing i ⊗[R] ChartRing j, followed by the chart D₊(Xⱼ).

theorem WeierstrassCurve.SpecMap_desc_chartPairι {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : CommRingCat} {i j : Fin 3} (α : ↧(W.toProjective.ChartRing i) ⟶ A) (β : ↧(W.toProjective.ChartRing j) ⟶ A) (h : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R (W.toProjective.ChartRing i))) α = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R (W.toProjective.ChartRing j))) β) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (⋯.desc α β h)) (W.chartPairι i j) = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map α) (W.chartι i)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map β) (W.chartι j)) ⋯

If the homomorphisms α and β from the chart rings ChartRing i and ChartRing j to A agree on R, then Spec of the homomorphism a ⊗ₜ b ↦ α a * β b they induce on ChartRing i ⊗[R] ChartRing j, followed by the product chartPairι W i j of the charts, is the morphism to E ×_S E with components Spec α ≫ chartι W i and Spec β ≫ chartι W j.

theorem WeierstrassCurve.range_chartPairι {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) : Set.range ⇑(W.chartPairι i j) = ⇑(CategoryTheory.Limits.pullback.fst W.projModelOver W.projModelOver) ⁻¹' Set.range ⇑(W.chartι i) ∩ ⇑(CategoryTheory.Limits.pullback.snd W.projModelOver W.projModelOver) ⁻¹' Set.range ⇑(W.chartι j)

A point of E ×_S E lies on the product of the charts D₊(Xᵢ) and D₊(Xⱼ) exactly when its two projections lie on D₊(Xᵢ) and D₊(Xⱼ).