Concrete regression for the elliptic-curve development

This file is an end-to-end smoke test: it instantiates the generic elliptic-curve theorems on a concrete Weierstrass curve over a concrete algebraically closed field, so that instance synthesis for the whole hypothesis pack is exercised for real.

• The base field is k := AlgebraicClosure ℚ (characteristic zero, IsAlgClosed).
• The curve is y² = x³ - x, i.e. curve : WeierstrassCurve.Affine k := ⟨0, 0, 0, -1, 0⟩, whose discriminant is Δ = 64 ≠ 0, so it is elliptic.
• The fraction field K of curve.CoordinateRing is kept abstract (exactly as the general theorems are stated); a concrete FractionRing would reintroduce a Semiring instance diamond.

We assemble the full k[X] / k⟮X⟯ algebra tower via the constructors in RiemannRoch.EllipticCurve.Instances, and then check that the public targets genus_eq_one, picTorsor, and picTorsor_compat_groupLaw elaborate on this concrete input.

All declarations live in the RiemannRochTest.EllipticCurve namespace so that the generic names k, curve, … do not leak into the root environment.

@[reducible, inline]

abbrev RiemannRochTest.EllipticCurve.k : Type

The concrete algebraically closed base field: the algebraic closure of ℚ.

Equations

• RiemannRochTest.EllipticCurve.k = AlgebraicClosure ℚ

noncomputable def RiemannRochTest.EllipticCurve.curve : WeierstrassCurve.Affine k

The concrete Weierstrass curve y² = x³ - x over k = AlgebraicClosure ℚ.

Equations

• RiemannRochTest.EllipticCurve.curve = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := -1, a₆ := 0 }

theorem RiemannRochTest.EllipticCurve.curve_Δ : WeierstrassCurve.Δ curve = 64

The discriminant of curve is 64.

instance RiemannRochTest.EllipticCurve.instIsEllipticKCurve : WeierstrassCurve.IsElliptic curve

curve is an elliptic curve: its discriminant 64 is a unit over a field of characteristic zero.

theorem RiemannRochTest.EllipticCurve.curve_nonsingular : curve.Nonsingular 0 0

The affine point (0, 0) is a nonsingular point of curve (here a₆ = 0 and a₄ = -1 ≠ 0).

The instance tower on the abstract fraction field K

Each local instance is a constructor from RiemannRoch.EllipticCurve.Instances, introduced in strict dependency order so that the next one can synthesise the ones already in scope.

@[instance_reducible]

noncomputable def RiemannRochTest.EllipticCurve.instAlgPoly (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] : Algebra (Polynomial k) K

Item 1: the k[X]-algebra structure on K (X ↦ x).

Equations

• RiemannRochTest.EllipticCurve.instAlgPoly K = RiemannRochTest.EllipticCurve.curve.algebraPolynomial K

theorem RiemannRochTest.EllipticCurve.instTowerPoly (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] : IsScalarTower (Polynomial k) curve.CoordinateRing K

Item 1: compatibility of the k[X]-algebra with the coordinate-ring inclusion.

@[instance_reducible]

noncomputable def RiemannRochTest.EllipticCurve.instAlgRat (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] [IsFractionRing curve.CoordinateRing K] : Algebra (RatFunc k) K

Item 2: the k⟮X⟯-algebra structure on K.

Equations

• RiemannRochTest.EllipticCurve.instAlgRat K = RiemannRochTest.EllipticCurve.curve.algebraRatFunc K

theorem RiemannRochTest.EllipticCurve.instTowerRat (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] [IsFractionRing curve.CoordinateRing K] : IsScalarTower (Polynomial k) (RatFunc k) K

Item 2: the k[X] → k⟮X⟯ → K scalar tower.

theorem RiemannRochTest.EllipticCurve.instFunctionField (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] [IsFractionRing curve.CoordinateRing K] : FunctionField k K

Item 3: K is a function field over k.

theorem RiemannRochTest.EllipticCurve.instSeparable (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] [IsFractionRing curve.CoordinateRing K] : Algebra.IsSeparable (RatFunc k) K

Item 4: K is separable over k⟮X⟯.

@[instance_reducible]

noncomputable def RiemannRochTest.EllipticCurve.instAlgConst (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] : Algebra k K

Constant field: the k-algebra structure on K through k[X].

Equations

• RiemannRochTest.EllipticCurve.instAlgConst K = FunctionField.algebraConstants RiemannRochTest.EllipticCurve.k K

theorem RiemannRochTest.EllipticCurve.instTowerConst (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] : IsScalarTower k (Polynomial k) K

Constant field: the k → k[X] → K scalar tower.

theorem RiemannRochTest.EllipticCurve.instFullConstant (K : Type u_1) [Field K] [Algebra curve.CoordinateRing K] : FunctionField.IsFullConstantField k K

Item 5: over an algebraically closed base, the constant field is full.

The headline targets, elaborated on the concrete input