The Bosma–Lenstra chart cover of `E ×_S E` #

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its projective model and let S = Spec R. The products D₊(Xᵢ) ×_S D₊(Xⱼ) of the standard affine charts of E cover E ×_S E, and D₊(Xᵢ) ×_S D₊(Xⱼ) is the spectrum of ChartRing i ⊗[R] ChartRing j (WeierstrassCurve.chartPairι). This ring carries two universal points of the curve: P, coming from the first factor, with i-th coordinate 1, and Q, coming from the second factor, with j-th coordinate 1.

The six coordinates of the two Bosma–Lenstra addition laws addXYZ P Q and dblAddXYZ P Q generate the unit ideal of ChartRing i ⊗[R] ChartRing j (WeierstrassCurve.Projective.span_range_addXYZ_union_range_dblAddXYZ_eq_top), so the loci where one of them is a unit cover D₊(Xᵢ) ×_S D₊(Xⱼ). On such a locus, the corresponding law is a triple with a unit coordinate. This file assembles these loci, nine chart products with six loci each, into a finite affine open cover of E ×_S E.

Main definitions #

WeierstrassCurve.chartPairLaw W i j: the six coordinates of addXYZ P Q and dblAddXYZ P Q at the universal points P and Q of ChartRing i ⊗[R] ChartRing j.
WeierstrassCurve.additionCover W: the affine open cover of E ×_S E by the spectra of the localizations of the rings ChartRing i ⊗[R] ChartRing j away from the coordinates chartPairLaw W i j k.

Main results #

WeierstrassCurve.comp_chartPairLaw: pushed along a homomorphism out of a product of two charts, the six law coordinates are the two laws at the images of the universal points.
WeierstrassCurve.span_range_chartPairLaw_eq_top: the six law coordinates generate the unit ideal.
WeierstrassCurve.exists_mem_range_specMap_comp_chartPairι: every point of E ×_S E lies on the locus, in some product of two charts, where some law coordinate is a unit.

References #

W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.

Provenance #

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/:

from AdditionChartRing.lean: biChartPointFst, biChartPointSnd, lawOneTriple and lawTwoTriple, as chartPairLaw. The universal points of a product of two charts are the images of WeierstrassCurve.Projective.chartPoint in the tensor product of TauCeti's chart rings ChartRing, in place of the source's presented ring in four variables.
from AdditionChartSpec.lean: chartProductCover, as exists_mem_range_specMap_comp_chartPairι.
from AdditionSpecPoints.lean: ringHom_lawOneTriple and ringHom_lawTwoTriple, as comp_chartPairLaw.
from AdditionChartDomain.lean: span_lawOneTriple_union_lawTwoTriple_eq_top, as span_range_chartPairLaw_eq_top.

source

noncomputable def WeierstrassCurve.chartPairLaw {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) :

Fin 3 ⊕ Fin 3 → TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)

The six coordinates of the two Bosma–Lenstra addition laws addXYZ P Q (indexed by inl) and dblAddXYZ P Q (indexed by inr) at the universal points P = chartPoint i ⊗ 1 and Q = 1 ⊗ chartPoint j of the product ChartRing i ⊗[R] ChartRing j of two charts.

Equations

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

Instances For

source

@[simp]

theorem WeierstrassCurve.chartPairLaw_inl {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j k : Fin 3) :

W.chartPairLaw i j (Sum.inl k) = (W.toProjective.baseChange (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j))).addXYZ (⇑Algebra.TensorProduct.includeLeft ∘ W.toProjective.chartPoint i) (⇑Algebra.TensorProduct.includeRight ∘ W.toProjective.chartPoint j) k

The coordinates of chartPairLaw indexed by inl are those of addXYZ P Q.

source

@[simp]

theorem WeierstrassCurve.chartPairLaw_inr {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j k : Fin 3) :

W.chartPairLaw i j (Sum.inr k) = (W.toProjective.baseChange (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j))).dblAddXYZ (⇑Algebra.TensorProduct.includeLeft ∘ W.toProjective.chartPoint i) (⇑Algebra.TensorProduct.includeRight ∘ W.toProjective.chartPoint j) k

The coordinates of chartPairLaw indexed by inr are those of dblAddXYZ P Q.

source

theorem WeierstrassCurve.comp_chartPairLaw {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : CommRingCat} {i j : Fin 3} (φ : ↧(TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)) ⟶ A) :

Pushed along a homomorphism φ out of the product ChartRing i ⊗[R] ChartRing j of two charts, the six coordinates chartPairLaw W i j of the two laws are the laws addXYZ and dblAddXYZ, for the curve W mapped along the composite structure map R → A, at the images under φ of the universal points P and Q of the two charts.

source

theorem WeierstrassCurve.span_range_chartPairLaw_eq_top {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (i j : Fin 3) :

Ideal.span (Set.range (W.chartPairLaw i j)) = ⊤

On an elliptic curve, the six coordinates of the two addition laws at the universal points of the product ChartRing i ⊗[R] ChartRing j of two charts generate the unit ideal.

source

theorem WeierstrassCurve.exists_mem_range_specMap_comp_chartPairι {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (x : ↥(CategoryTheory.Limits.pullback W.projModelOver W.projModelOver)) :

∃ (a : (Fin 3 × Fin 3) × (Fin 3 ⊕ Fin 3)), x ∈ Set.range ⇑(CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (TensorProduct R (W.toProjective.ChartRing a.1.1) (W.toProjective.ChartRing a.1.2)) (Localization.Away (W.chartPairLaw a.1.1 a.1.2 a.2))))) (W.chartPairι a.1.1 a.1.2))

Every point of E ×_S E lies on the product D₊(Xᵢ) ×_S D₊(Xⱼ) of two charts, at a point where some coordinate chartPairLaw W i j k of one of the two addition laws is a unit: it is in the image of Spec of the localization of ChartRing i ⊗[R] ChartRing j away from that coordinate.

source

@[reducible]

noncomputable def WeierstrassCurve.additionCover {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] :

(CategoryTheory.Limits.pullback W.projModelOver W.projModelOver).AffineOpenCover

The Bosma–Lenstra chart cover of E ×_S E, for E = projModel W and S = Spec R: the affine open cover by the loci, in the products D₊(Xᵢ) ×_S D₊(Xⱼ) of two charts, where one of the six coordinates chartPairLaw W i j k of the two addition laws is a unit. It has 54 pieces, indexed by ((i, j), k) in (Fin 3 × Fin 3) × (Fin 3 ⊕ Fin 3); the piece indexed by ((i, j), k) is Spec of the localization of ChartRing i ⊗[R] ChartRing j away from chartPairLaw W i j k. The definition is reducible, so its pieces and their maps to E ×_S E unfold by simp.