Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Addition.Chart

The Bosma–Lenstra addition morphisms on the chart cover #

Let W be a Weierstrass curve over a commutative ring R, let E = projModel W be its projective model and let S = Spec R. The pieces of the Bosma–Lenstra chart cover WeierstrassCurve.additionCover of E ×_S E are the spectra of the localizations of ChartRing i ⊗[R] ChartRing j away from the six coordinates chartPairLaw W i j k of the two addition laws addXYZ P Q (for k = inl _) and dblAddXYZ P Q (for k = inr _) at the universal points P and Q of ChartRing i ⊗[R] ChartRing j. On such a piece, the law selected by k is a solution of the projective Weierstrass equation (WeierstrassCurve.Projective.Equation.addXYZ, WeierstrassCurve.Projective.Equation.dblAddXYZ) with a unit coordinate, so it gives a point of E (WeierstrassCurve.projModelPoint). This file defines the addition morphisms on the pieces of the cover as these points, and shows that they lie over S. No ellipticity is needed.

Main definitions #

Main results #

References #

Provenance #

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

Here the two laws are indexed together by Fin 3 ⊕ Fin 3, as in chartPairLaw. The morphism on a piece is the point WeierstrassCurve.projModelPoint of the law, which evaluates the homogeneous coordinate ring, in place of the source's chart homomorphism chartHomOfTriple (file AdditionChartHom.lean) out of a dehomogenised chart ring. The laws solve the equation over every ring, so the source's hypotheses that R is a Jacobson ring, that the product of two charts is a domain and that the discriminant is a unit are dropped.

source
theorem WeierstrassCurve.equation_chartPairLaw_comp_inl {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) :
(W.toProjective.baseChange (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j))).Equation (W.chartPairLaw i j ∘ Sum.inl)

The law addXYZ P Q at the universal points P and Q of ChartRing i ⊗[R] ChartRing j, that is chartPairLaw W i j ∘ inl, is a solution of the Weierstrass equation over that ring.

source
theorem WeierstrassCurve.equation_chartPairLaw_comp_inr {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) :
(W.toProjective.baseChange (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j))).Equation (W.chartPairLaw i j ∘ Sum.inr)

The law dblAddXYZ P Q at the universal points P and Q of ChartRing i ⊗[R] ChartRing j, that is chartPairLaw W i j ∘ inr, is a solution of the Weierstrass equation over that ring.

source
noncomputable def WeierstrassCurve.additionOnPiece {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) (k : Fin 3 ⊕ Fin 3) :
AlgebraicGeometry.Spec ↧(Localization.Away (W.chartPairLaw i j k)) ⟶ W.projModel

The Bosma–Lenstra addition morphism on a piece of the chart cover additionCover W of E ×_S E, for E = projModel W and S = Spec R. Let P and Q be the universal points of ChartRing i ⊗[R] ChartRing j. For k = inl m (resp. k = inr m), the coordinate of index m of the law addXYZ P Q (resp. dblAddXYZ P Q) is chartPairLaw W i j k, a unit in the localization away from it, and additionOnPiece W i j k is the point of E with homogeneous coordinates the image of that law, read on the chart D₊(Xₘ) (additionOnPiece_inl, additionOnPiece_inr). It lies over S (additionOnPiece_projModelOver).

Equations
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.additionOnPiece_inl {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j k : Fin 3) :
    W.additionOnPiece i j (Sum.inl k) = W.projModelPoint (algebraMap R (Localization.Away (W.chartPairLaw i j (Sum.inl k)))) ⋯ ⋯

    On the piece of additionCover W indexed by inl k, the addition morphism is the point of projModel W whose homogeneous coordinates are the image of the law addXYZ P Q at the universal points P and Q, that is of chartPairLaw W i j ∘ inl, read on the chart D₊(Xₖ).

    source
    @[simp]
    theorem WeierstrassCurve.additionOnPiece_inr {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j k : Fin 3) :
    W.additionOnPiece i j (Sum.inr k) = W.projModelPoint (algebraMap R (Localization.Away (W.chartPairLaw i j (Sum.inr k)))) ⋯ ⋯

    On the piece of additionCover W indexed by inr k, the addition morphism is the point of projModel W whose homogeneous coordinates are the image of the law dblAddXYZ P Q at the universal points P and Q, that is of chartPairLaw W i j ∘ inr, read on the chart D₊(Xₖ).

    source
    theorem WeierstrassCurve.exists_SpecMap_additionOnPiece {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : CommRingCat} {i j : Fin 3} (k : Fin 3 ⊕ Fin 3) (φ : ↧(Localization.Away (W.chartPairLaw i j k)) ⟶ A) :
    ∃ (hP : (W.toProjective.map (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R (Localization.Away (W.chartPairLaw i j k)))) φ))).Equation fun (m : Fin 3) => (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)) (Localization.Away (W.chartPairLaw i j k)))) φ)) (W.chartPairLaw i j (Sum.map (fun (x : Fin 3) => m) (fun (x : Fin 3) => m) k))) (hm : IsUnit ((CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (TensorProduct R (W.toProjective.ChartRing i) (W.toProjective.ChartRing j)) (Localization.Away (W.chartPairLaw i j k)))) φ)) (W.chartPairLaw i j (Sum.map (fun (x : Fin 3) => Sum.elim id id k) (fun (x : Fin 3) => Sum.elim id id k) k)))), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) (W.additionOnPiece i j k) = W.projModelPoint (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R (Localization.Away (W.chartPairLaw i j k)))) φ)) hP hm

    Let φ be a homomorphism to A from Localization.Away (chartPairLaw W i j k), the ring of the piece of the chart cover indexed by (i, j, k). The image under φ of the law selected by k at the universal points, addXYZ for k = inl m and dblAddXYZ for k = inr m, is a solution of the Weierstrass equation over A whose coordinate of index m is a unit, and the composite of Spec φ with the addition morphism on the piece is the point of projModel W with these homogeneous coordinates, read on the chart D₊(Xₘ).

    source
    @[simp]
    theorem WeierstrassCurve.additionOnPiece_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) (k : Fin 3 ⊕ Fin 3) :
    CategoryTheory.CategoryStruct.comp (W.additionOnPiece i j k) W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away (W.chartPairLaw i j k))))

    The addition morphism on each piece of additionCover W lies over Spec R: its composite with the structure morphism of projModel W is Spec of the structure map R → Localization.Away (chartPairLaw W i j k).

    source
    @[simp]
    theorem WeierstrassCurve.additionOnPiece_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i j : Fin 3) (k : Fin 3 ⊕ Fin 3) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (W.additionOnPiece i j k) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away (W.chartPairLaw i j k))))) h

    The addition morphism on each piece of additionCover W lies over Spec R: its composite with the structure morphism of projModel W is Spec of the structure map R → Localization.Away (chartPairLaw W i j k).