Models of Elliptic Curves over a Ring

We define elliptic curves over a ring from the Weierstrass equation. Note that not all "elliptic curves" in the literature necessarily satisfy a Weierstrass cubic globally.

Main definitions

• FooBar

def EllipticCurve.Ring.X {R : CommRingCat} : SymmetricPower (↑R) (Fin 3 → ↑R) 1

The "x-coordinate" as a section of 𝒪(1) on ℙ².

Equations

• EllipticCurve.Ring.X = (SymmetricPower.tprod ↑R) ![Pi.single 0 1]

def EllipticCurve.Ring.Y {R : CommRingCat} : SymmetricPower (↑R) (Fin 3 → ↑R) 1

Equations

• EllipticCurve.Ring.Y = (SymmetricPower.tprod ↑R) ![Pi.single 1 1]

def EllipticCurve.Ring.Z {R : CommRingCat} : SymmetricPower (↑R) (Fin 3 → ↑R) 1

Equations

• EllipticCurve.Ring.Z = (SymmetricPower.tprod ↑R) ![Pi.single 2 1]

@[simp]

theorem EllipticCurve.Ring.map_X {R : CommRingCat} {M : Type u_1} [AddCommGroup M] [Module (↑R) M] (f : (Fin 3 → ↑R) →ₗ[↑R] M) : (SymmetricPower.map 1 f) X = (SymmetricPower.tprod ↑R) ![f (Pi.single 0 1)]

@[simp]

theorem EllipticCurve.Ring.map_Y {R : CommRingCat} {M : Type u_1} [AddCommGroup M] [Module (↑R) M] (f : (Fin 3 → ↑R) →ₗ[↑R] M) : (SymmetricPower.map 1 f) Y = (SymmetricPower.tprod ↑R) ![f (Pi.single 1 1)]

@[simp]

theorem EllipticCurve.Ring.map_Z {R : CommRingCat} {M : Type u_1} [AddCommGroup M] [Module (↑R) M] (f : (Fin 3 → ↑R) →ₗ[↑R] M) : (SymmetricPower.map 1 f) Z = (SymmetricPower.tprod ↑R) ![f (Pi.single 2 1)]

def WeierstrassCurve.Affine.asSym {R : CommRingCat} (W : Affine ↑R) : SymmetricPower (↑R) (Fin 3 → ↑R) 3

Equations

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

def EllipticCurve.Ring.model {R : CommRingCat} (W : WeierstrassCurve.Affine ↑R) : CategoryTheory.Functor (CategoryTheory.Under R) (Type u)

We don't have the scheme yet, so we just use the functor R-Alg ⥤ Type.

Equations

• EllipticCurve.Ring.model W = Module.ProjectiveSpace.zerosFunctor R (ModuleCat.of (↑R) (Fin 3 → ↑R)) W.asSym

def EllipticCurve.Ring.infinity {R : CommRingCat} (W : WeierstrassCurve.Affine ↑R) : ↑(Module.ProjectiveSpace.zeros W.asSym)

The point at infinity

Equations

• EllipticCurve.Ring.infinity W = Module.ProjectiveSpace.zerosOfCoordinates W.asSym ![0, 1, 0] ⋯ ⋯