noncomputable def ComplexLattice.ellipticCurveEL (L : ComplexLattice) : WeierstrassCurve ℂ

The Weierstrass curve E_L : y^2 = 4x^3 - g₂(L)·x - g₃(L) associated to a lattice L, presented in long Weierstrass form with coefficients (a₁, a₂, a₃, a₄, a₆) = (0, 0, 0, -g₂/4, -g₃/4).

noncomputable def ComplexLattice.ellipticCurveEL_affine (L : ComplexLattice) : WeierstrassCurve.Affine ℂ

The affine model of ellipticCurveEL L, used to talk about its affine Point type.

@[reducible, inline]

abbrev ComplexLattice.ELPoint (L : ComplexLattice) : Type

The type of points on the elliptic curve E_L associated to the lattice L.

@[implicit_reducible]

noncomputable instance ComplexLattice.instAddCommGroupELPoint (L : ComplexLattice) : AddCommGroup L.ELPoint

The additive group structure on E_L(ℂ) from the chord-tangent law on a Weierstrass curve.

theorem ComplexLattice.ellipticCurveEL_Δ_eq (L : ComplexLattice) : WeierstrassCurve.Δ L.ellipticCurveEL_affine = L.discriminantLattice

The discriminant of the affine elliptic curve E_L equals the lattice discriminant Δ(L) = g₂³ - 27 g₃² (up to the normalization built into discriminantLattice).

theorem ComplexLattice.ellipticCurveEL_Δ_ne_zero (L : ComplexLattice) : WeierstrassCurve.Δ L.ellipticCurveEL_affine ≠ 0

The discriminant of E_L is nonzero, so E_L really is an elliptic curve (this is Lemma 14.33 applied to E_L).

theorem ComplexLattice.weierstrassP_point_equation (L : ComplexLattice) (z : ℂ) (hz : z ∉ ↑(PeriodPair.lattice L)) : L.ellipticCurveEL_affine.Equation (L.weierstrassPFun z) (L.derivWeierstrassPFun z / 2)

For any non-lattice point z, the pair (℘(z), ℘'(z)/2) satisfies the Weierstrass equation of E_L, i.e. lies on the affine curve. This is the key calculation behind the uniformization map of Theorem 15.1.

theorem ComplexLattice.weierstrassP_point_nonsingular (L : ComplexLattice) (z : ℂ) (hz : z ∉ ↑(PeriodPair.lattice L)) : L.ellipticCurveEL_affine.Nonsingular (L.weierstrassPFun z) (L.derivWeierstrassPFun z / 2)

For any non-lattice point z, the point (℘(z), ℘'(z)/2) is a nonsingular point of E_L, since E_L has nonzero discriminant.

noncomputable def ComplexLattice.PhiAux (L : ComplexLattice) (z : ℂ) (hz : z ∉ ↑(PeriodPair.lattice L)) : L.ELPoint

The uniformization map on a non-lattice point: send z ∉ L to the affine point (℘(z), ℘'(z)/2) of E_L.

@[reducible, inline]

abbrev ComplexLattice.complexTorus (L : ComplexLattice) : Type

The complex torus ℂ / L for the lattice L.

@[implicit_reducible]

noncomputable instance ComplexLattice.instAddCommGroupComplexTorus (L : ComplexLattice) : AddCommGroup L.complexTorus

The complex torus inherits the additive group structure from the quotient of ℂ by L.

noncomputable def ComplexLattice.PhiLift (L : ComplexLattice) (z : ℂ) : L.ELPoint

The set-theoretic uniformization lift ℂ → E_L(ℂ) underlying Φ: lattice points are sent to the identity, and any other z to (℘(z), ℘'(z)/2).

theorem ComplexLattice.PhiLift_add_lattice (L : ComplexLattice) (z ω : ℂ) (hω : ω ∈ PeriodPair.lattice L) : L.PhiLift (z + ω) = L.PhiLift z

The lift PhiLift is L-periodic: shifting z by a lattice element does not change its image, which is what allows it to descend to ℂ / L.

noncomputable def ComplexLattice.PhiFun (L : ComplexLattice) : L.complexTorus → L.ELPoint

The uniformization map Φ : ℂ/L → E_L(ℂ) as a function, obtained by descending PhiLift to the quotient using its L-periodicity.

theorem ComplexLattice.PhiFun_zero (L : ComplexLattice) : L.PhiFun 0 = 0

The uniformization map sends the identity of ℂ/L (the class of 0) to the identity (point at infinity) of E_L.

theorem ComplexLattice.PhiFun_mk (L : ComplexLattice) (z : ℂ) (hz : z ∉ ↑(PeriodPair.lattice L)) : L.PhiFun ↑z = L.PhiAux z hz

Computational rule for PhiFun: on the class of a non-lattice point z, the map agrees with PhiAux z, i.e. evaluates to (℘(z), ℘'(z)/2).

theorem ComplexLattice.PhiFun_map_add (L : ComplexLattice) (a b : L.complexTorus) : L.PhiFun (a + b) = L.PhiFun a + L.PhiFun b

Additivity of the uniformization map: Φ(a + b) = Φ(a) + Φ(b) on the complex torus. This is the group-homomorphism content of Theorem 15.1, the classical addition law for the Weierstrass ℘ function.

noncomputable def ComplexLattice.complexTorusToEL (L : ComplexLattice) : L.complexTorus →+ L.ELPoint

The uniformization map Φ : ℂ/L → E_L(ℂ) packaged as a group homomorphism, using PhiFun_zero and PhiFun_map_add.

theorem ComplexLattice.Phi_injective (L : ComplexLattice) : Function.Injective ⇑L.complexTorusToEL

Injectivity of Φ: relying on the parity/duplication properties of ℘ and ℘', two torus classes mapping to the same point of E_L must agree. This is the injectivity half of Theorem 15.1.

theorem ComplexLattice.Phi_surjective (L : ComplexLattice) : Function.Surjective ⇑L.complexTorusToEL

Surjectivity of Φ: every point of E_L(ℂ) is the image of some torus class. This is the surjectivity half of Theorem 15.1.

theorem ComplexLattice.Phi_bijective (L : ComplexLattice) : Function.Bijective ⇑L.complexTorusToEL

The uniformization map Φ : ℂ/L → E_L(ℂ) is bijective, combining injectivity and surjectivity.

noncomputable def ComplexLattice.uniformization_iso (L : ComplexLattice) : L.complexTorus ≃+ L.ELPoint

Theorem 15.1: the map Φ : ℂ/L → E_L(ℂ) is a group isomorphism between the complex torus and the complex points of the elliptic curve E_L.