Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Geom.Glue

Gluing morphisms along the pointed Weierstrass charts of an elliptic curve #

Let E be an elliptic curve over a scheme S and q : Y ⟶ S a morphism of schemes. The bases of the pointed Weierstrass charts of E are affine opens of S covering S, so their preimages Y ×_S U cover Y. This file glues morphisms out of Y along this cover: a family of morphisms Y ×_S U ⟶ Z, one for each chart, glues to a morphism Y ⟶ Z as soon as it is compatible with the morphisms of chart bases over S.

Compatibility is only required along morphisms of bases, not on the overlaps of the cover. Two charts c and d agree near every point of U_c ∩ U_d because, around each such point, the restriction of c to an affine open of its base mapping into U_d is again a chart, whose base maps both to U_c and to U_d.

This is how the morphisms of the group law of E, defined on each chart through its Weierstrass equation, become morphisms over the whole of S: for the addition E ×_S E ⟶ E, Y = E ×_S E; for the negation E ⟶ E, Y = E.

The same gluing turns a universal property over affine bases into one over arbitrary bases. Let p : U ⟶ B be a family of curves with sections, such as a universal Weierstrass normal form. If the projective model of every chart of E, with the sections induced by given sections of E, is the base change of p along a unique morphism, compatibly with the sections, then so is E (TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_isPullback_of_forall_chart).

Main definitions #

Main results #

source
theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.hom_ext {S Y Z : AlgebraicGeometry.Scheme} (q : Y ⟶ S) {X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) (f g : Y ⟶ Z) (h : ∀ (i : A.index), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst q (A.chart i).baseMap) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst q (A.chart i).baseMap) g) :
f = g

Morphisms are determined on the charts of an atlas. Two morphisms out of Y that agree on the preimages Y ×_S U of the bases U of the charts of a pointed Weierstrass atlas of π are equal.

source
theorem TauCeti.AlgebraicGeometry.PointedWeierstrassAtlas.hom_ext_of_toTotal {S Z X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (A : PointedWeierstrassAtlas π zero) (f g : X ⟶ Z) (h : ∀ (i : A.index), CategoryTheory.CategoryStruct.comp (A.chart i).toTotal f = CategoryTheory.CategoryStruct.comp (A.chart i).toTotal g) :
f = g

Morphisms out of X are determined on the charts of an atlas. Two morphisms out of X that agree on the restrictions of X to the bases of the charts of a pointed Weierstrass atlas of π are equal.

source
noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.glueMorphisms {S Y Z : AlgebraicGeometry.Scheme} {q : Y ⟶ S} {E : EllipticCurveGeom S} (g : (c : PointedWeierstrassChart E.structureMap E.zero) → CategoryTheory.Limits.pullback q c.baseMap ⟶ Z) (hg : ∀ {k c : PointedWeierstrassChart E.structureMap E.zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map q k.baseMap q c.baseMap (CategoryTheory.CategoryStruct.id Y) h (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (g c) = g k) :
Y ⟶ Z

Gluing along the charts of an elliptic curve. The morphism Y ⟶ Z glued from a family g of morphisms Y ×_S U ⟶ Z, one over the base U of each pointed Weierstrass chart of E, that is compatible with the morphisms of chart bases over S: if the base of a chart k maps to the base of a chart c, then g c restricts to g k. Its restriction to every chart is the given morphism (fst_glueMorphisms).

Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.fst_glueMorphisms {S Y Z : AlgebraicGeometry.Scheme} {q : Y ⟶ S} {E : EllipticCurveGeom S} (g : (c : PointedWeierstrassChart E.structureMap E.zero) → CategoryTheory.Limits.pullback q c.baseMap ⟶ Z) (hg : ∀ {k c : PointedWeierstrassChart E.structureMap E.zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map q k.baseMap q c.baseMap (CategoryTheory.CategoryStruct.id Y) h (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (g c) = g k) (c : PointedWeierstrassChart E.structureMap E.zero) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst q c.baseMap) (glueMorphisms g ⋯) = g c

    On the preimage of the base of a chart c, the morphism glued from a compatible family g is g c.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.fst_glueMorphisms_assoc {S Y Z : AlgebraicGeometry.Scheme} {q : Y ⟶ S} {E : EllipticCurveGeom S} (g : (c : PointedWeierstrassChart E.structureMap E.zero) → CategoryTheory.Limits.pullback q c.baseMap ⟶ Z) (hg : ∀ {k c : PointedWeierstrassChart E.structureMap E.zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map q k.baseMap q c.baseMap (CategoryTheory.CategoryStruct.id Y) h (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (g c) = g k) (c : PointedWeierstrassChart E.structureMap E.zero) {Z✝ : AlgebraicGeometry.Scheme} (h : Z ⟶ Z✝) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst q c.baseMap) (CategoryTheory.CategoryStruct.comp (glueMorphisms g ⋯) h) = CategoryTheory.CategoryStruct.comp (g c) h

    On the preimage of the base of a chart c, the morphism glued from a compatible family g is g c.

    Classifying pairs #

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_isPullback_of_forall_chart {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {B U : AlgebraicGeometry.Scheme} {p : U ⟶ B} {t₀ : B ⟶ U} {ι : Type u_1} {t : ι → (B ⟶ U)} {σ : ι → (S ⟶ E.carrier)} (hσ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (σ i) E.structureMap = CategoryTheory.CategoryStruct.id S) (hc : ∀ (c : PointedWeierstrassChart E.structureMap E.zero), ∃! fg : (AlgebraicGeometry.Spec c.ring ⟶ B) × (c.equation.projModel ⟶ U), CategoryTheory.IsPullback fg.2 c.equation.projModelOver p fg.1 ∧ CategoryTheory.CategoryStruct.comp c.equation.projModelZero fg.2 = CategoryTheory.CategoryStruct.comp fg.1 t₀ ∧ ∀ (i : ι), CategoryTheory.CategoryStruct.comp (c.modelPoint ⋯) fg.2 = CategoryTheory.CategoryStruct.comp fg.1 (t i)) :
    ∃! fg : (S ⟶ B) × (E.carrier ⟶ U), CategoryTheory.IsPullback fg.2 E.structureMap p fg.1 ∧ CategoryTheory.CategoryStruct.comp E.zero fg.2 = CategoryTheory.CategoryStruct.comp fg.1 t₀ ∧ ∀ (i : ι), CategoryTheory.CategoryStruct.comp (σ i) fg.2 = CategoryTheory.CategoryStruct.comp fg.1 (t i)

    Classifying pairs glue along the charts. Let p : U ⟶ B be a morphism of schemes with sections t₀ and t i, and let E be an elliptic curve over S with sections σ i. Suppose that over the base of every pointed Weierstrass chart c of E there is a unique pair of a morphism f : Spec c.ring ⟶ B and a morphism g from the projective model of the equation of c to U such that g exhibits the model as the base change of p along f, carrying the zero section to t₀ and the model point of each σ i to t i. Then there is a unique such pair for E itself.

    This is how a universal family over B, such as a universal Weierstrass normal form, becomes a fine moduli space over arbitrary bases once its universal property is known over affine bases.