The `j`-invariant of an elliptic curve over a scheme #

Let E be an elliptic curve over a scheme S. Zariski-locally on S, E is the projective model of an elliptic Weierstrass curve, through a pointed Weierstrass chart, and the j-invariant WeierstrassCurve.j of that equation is a function on the base of the chart. Two charts give the same function where both are defined, because a pointed isomorphism of projective Weierstrass models is a change of variables and the j-invariant is invariant under changes of variables (WeierstrassCurve.j_eq_of_isPullback). These local functions therefore glue to a global function EllipticCurveGeom.j E : Γ(S, ⊤), the j-invariant of E. Equivalently it is a morphism EllipticCurveGeom.jMap E : S ⟶ Spec ℤ[j] to the j-line, where ℤ[j] is the polynomial ring MvPolynomial PUnit (ULift ℤ) in one variable, the integral model of the affine line in Mathlib.AlgebraicGeometry.AffineSpace.

The j-invariant is compatible with every cartesian morphism of elliptic curves: if g : E' ⟶ E exhibits E' over S' as the base change of E along f : S' ⟶ S, compatibly with the zero sections, then f pulls back the j-invariant of E to that of E' (EllipticCurveGeom.appTop_j_of_isPullback). Thus E ↦ jMap E is a morphism from the moduli problem of elliptic curves to the affine line, constant on isomorphism classes (EllipticCurveGeom.j_eq_of_iso) and compatible with base change (EllipticCurveGeom.jMap_baseChange). On the projective model of an elliptic Weierstrass curve W over R it is W.j (WeierstrassCurve.j_toEllipticCurveGeom, in TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.OfWeierstrass).

Main definitions #

TauCeti.AlgebraicGeometry.EllipticCurveGeom.jMap E: the j-invariant of E as a morphism S ⟶ Spec ℤ[j].
TauCeti.AlgebraicGeometry.EllipticCurveGeom.j E: the j-invariant of E as a global function on S.

Main results #

TauCeti.AlgebraicGeometry.EllipticCurveGeom.baseMap_appTop_j: on the base of any pointed Weierstrass chart, the j-invariant is that of the equation of the chart.
TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_j_of_atlas: this characterises it, already on the charts of any one atlas.
TauCeti.AlgebraicGeometry.EllipticCurveGeom.appTop_j_of_isPullback and TauCeti.AlgebraicGeometry.EllipticCurveGeom.comp_jMap_of_isPullback: compatibility with cartesian morphisms of elliptic curves, in particular with base change (TauCeti.AlgebraicGeometry.EllipticCurveGeom.j_baseChange and TauCeti.AlgebraicGeometry.EllipticCurveGeom.jMap_baseChange) and with isomorphisms (TauCeti.AlgebraicGeometry.EllipticCurveGeom.j_eq_of_iso).

References #

N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2 and 8.2.
P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, II.1.
J. H. Silverman, The Arithmetic of Elliptic Curves, III.1.

source

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.jMap {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :

S ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial PUnit.{u + 1} (ULift.{u, 0} ℤ))

The j-invariant of an elliptic curve E over S, as a morphism S ⟶ Spec ℤ[j] to the j-line, where ℤ[j] = MvPolynomial PUnit (ULift ℤ). On the base of every pointed Weierstrass chart it is given by the j-invariant of the equation of the chart (baseMap_appTop_j); these local morphisms glue because a pointed isomorphism of projective Weierstrass models preserves the j-invariant. The corresponding global function on S is EllipticCurveGeom.j E (jMap_eq).

Instances For

source

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.j {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :

↑(S.presheaf.obj (Opposite.op ⊤))

The j-invariant of an elliptic curve E over S, as a global function on S: the coordinate of the morphism jMap E to the j-line. On the base of every pointed Weierstrass chart it is the j-invariant of the equation of the chart (baseMap_appTop_j), and it is compatible with base change (j_baseChange).

Instances For

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.jMap_eq {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :

E.jMap = (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv PUnit.{u + 1}).symm fun (x : PUnit.{u + 1}) => E.j

The morphism jMap E to the j-line is the morphism with coordinate the j-invariant EllipticCurveGeom.j E.

source

The j-invariant on a chart. On the base of a pointed Weierstrass chart c of E, the j-invariant of E is the j-invariant of the Weierstrass equation of c, read through the isomorphism of the base of c with Spec c.ring.

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_j_of_atlas {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (A : PointedWeierstrassAtlas E.structureMap E.zero) {x : ↑(S.presheaf.obj (Opposite.op ⊤))} (hx : ∀ (i : A.index), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (A.chart i).baseMap)) x = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (A.chart i).baseIso.hom)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (A.chart i).ring).inv) (A.chart i).equation.j)) :

x = E.j

The j-invariant is determined by any atlas. A global function on S which, on the base of every chart of a pointed Weierstrass atlas of E, is the j-invariant of the equation of the chart, is the j-invariant of E.

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.appTop_j_of_isPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {f : S' ⟶ S} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) :

(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) E.j = E'.j

The j-invariant commutes with base change. Let g : E' ⟶ E be a morphism of elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure morphisms is a pullback square, and carrying the zero section of E' to that of E. Then f pulls back the j-invariant of E to that of E'.

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.comp_jMap_of_isPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {f : S' ⟶ S} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) :

CategoryTheory.CategoryStruct.comp f E.jMap = E'.jMap

The morphism to the j-line commutes with base change. A morphism g : E' ⟶ E of elliptic curves over f : S' ⟶ S forming a pullback square with the structure morphisms and carrying the zero section to the zero section satisfies f ≫ jMap E = jMap E'.

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.comp_jMap_of_isPullback_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {f : S' ⟶ S} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(MvPolynomial PUnit.{u + 1} (ULift.{u, 0} ℤ)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp E.jMap h) = CategoryTheory.CategoryStruct.comp E'.jMap h

source

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.j_eq_of_iso {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (e : E'.carrier ≅ E.carrier) (he : CategoryTheory.CategoryStruct.comp e.hom E.structureMap = E'.structureMap) (h0 : CategoryTheory.CategoryStruct.comp E'.zero e.hom = E.zero) :

E'.j = E.j

The j-invariant is an isomorphism invariant. Elliptic curves over S whose total spaces are isomorphic over S, by an isomorphism carrying the zero section to the zero section, have the same j-invariant.

source

@[simp]