Algebraic discriminant criterion: if the cubic 4x^3 - g₂ x - g₃ has three
distinct roots e₁, e₂, e₃, then the discriminant g₂^3 - 27 g₃^2 of the
corresponding elliptic curve is nonzero.
The half-sum (ω₁ + ω₂)/2 of the two fundamental periods does not lie in
the lattice L.
The derivative of the Weierstrass ℘-function vanishes at the half period
ω₁ / 2.
The derivative of the Weierstrass ℘-function vanishes at the half period
ω₂ / 2.
The derivative of the Weierstrass ℘-function vanishes at the half period
(ω₁ + ω₂) / 2.
The value e₁ = ℘(ω₁/2) is a root of the cubic 4x³ - g₂ x - g₃ = 0
associated to the lattice L.
The value e₂ = ℘(ω₂/2) is a root of the cubic 4x³ - g₂ x - g₃ = 0
associated to the lattice L.
The value e₃ = ℘((ω₁+ω₂)/2) is a root of the cubic
4x³ - g₂ x - g₃ = 0 associated to the lattice L.
The point (ω₁ - ω₂)/2 does not lie in the lattice.
The difference ω₁/2 - (ω₁ + ω₂)/2 = -ω₂/2 of two half periods does not
lie in the lattice.
The difference ω₂/2 - (ω₁ + ω₂)/2 = -ω₁/2 of two half periods does not
lie in the lattice.
An elliptic function of order 2 cannot have three pairwise inequivalent
zeros a, b, c (with all differences nonlattice). This is an axiomatic
ingredient used to prove the half-period injectivity statements below.
Injectivity at half periods: if z and w are nonlattice with
2z, 2w ∈ L and ℘(z) = ℘(w), then z - w ∈ L. This is a key step in the
cubic-root characterization of the half periods.
If ℘(z) = ℘(w) for nonlattice points z, w, then either z - w ∈ L or
z + w ∈ L.
The values ℘(ω₁/2), ℘(ω₂/2) and ℘((ω₁+ω₂)/2) of the Weierstrass
function at the three nontrivial half periods are pairwise distinct.
A cubic 4x³ - g₂ x - g₃ whose three roots e₁, e₂, e₃ are distinct has
no other roots: any root x must equal one of e₁, e₂, e₃.
If ℘(z) = ℘(w) for nonlattice z, w with 2w ∈ L, then z - w ∈ L.
This combines weierstrassP_eq_implies_pm with the assumption that w is a
half period.
If the derivative ℘'(z) vanishes at a nonlattice point z, then z is
congruent modulo L to one of the three nontrivial half periods ω₁/2,
ω₂/2, or (ω₁+ω₂)/2.
Characterization of the zeros of ℘': for z ∉ L, ℘'(z) = 0 if and
only if 2z ∈ L, i.e. z is a (nontrivial) half period.
Same characterization as derivWeierstrassPFun_eq_zero_iff, but with
membership phrased via L.toAddSubgroup.
The discriminant g₂(L)^3 - 27 g₃(L)^2 of any complex lattice is
nonzero, since the three half-period values of ℘ are distinct roots of the
associated cubic.
The short Weierstrass curve y² = x³ - (g₂/4) x - (g₃/4) associated to a
lattice L, obtained from y² = 4x³ - g₂ x - g₃ by the standard
substitution.
Instances For
The j-invariant of a lattice equals the j-invariant (in the sense of
short Weierstrass curves) of its associated curve y² = x³ - (g₂/4)x - (g₃/4).
Two lattices L, L' are said to give isomorphic elliptic curves over ℂ
if there is a Weierstrass variable change taking E_L to E_{L'}.
Instances For
If the elliptic curves associated to lattices L and L' are isomorphic
over ℂ, then they have the same j-invariant.
Converse to jInvariant_eq_of_ellipticCurveIsomorphic: lattices whose
short Weierstrass curves share the same j-invariant give rise to isomorphic
elliptic curves over ℂ. Splits into the j=0, j=1728, and generic cases.
If the Eisenstein invariants of two lattices L, L' are related by
g₂(L') = μ⁴ g₂(L) and g₃(L') = μ⁶ g₃(L) for some μ ≠ 0, then L and
L' are homothetic.
Two lattices with the same j-invariant (in the lattice sense) are
homothetic. This is the harder direction of the homothety/j correspondence
(Theorem 15.5 of the textbook).
Corollary 15.6 of the textbook: two lattices L, L' are homothetic if
and only if their associated elliptic curves E_L, E_{L'} are isomorphic
over ℂ.
The action of the modular generator T = [[1,1],[0,1]] on τ ∈ ℍ is
addition by 1.
The action of the modular generator S = [[0,-1],[1,0]] on τ ∈ ℍ is the
negative inverse τ ↦ -1/τ.
Invariance of the j-function under the generator S: j(-1/τ) = j(τ).
Invariance of the j-function under the generator T: j(τ + 1) = j(τ).
Invariance of j under the full modular group SL(2, ℤ): for any
γ ∈ SL(2, ℤ) and τ ∈ ℍ, j(γτ) = j(τ).
Symmetric form of jFunction_SL2_invariant: any γ-translate of τ has
the same j as τ.
One direction of Lemma 15.9: if j(τ) = j(τ'), then there exists
γ ∈ SL(2, ℤ) with τ' = γ τ.
Lemma 15.9 of the textbook: j(τ) = j(τ') if and only if τ' = γ τ for
some γ ∈ SL(2, ℤ).
The standard (closed) fundamental domain for the action of SL(2, ℤ) on
the upper half plane, as defined in mathlib via ModularGroup.fd.
Instances For
Membership in the standard fundamental domain: τ ∈ fd iff
|τ|² ≥ 1 and |Re τ| ≤ 1/2.
The open standard fundamental domain fdo for the action of SL(2, ℤ) on
ℍ.
Instances For
Membership in the open standard fundamental domain: τ ∈ fdo iff
|τ|² > 1 and |Re τ| < 1/2.
The open standard fundamental domain is contained in the closed one.
Every τ ∈ ℍ is SL(2, ℤ)-equivalent to a point of the standard closed
fundamental domain.
If both τ and γ τ lie in the open standard fundamental domain, then
τ = γ τ. (Uniqueness of the representative on the interior.)
The textbook (half-open) fundamental domain of Lemma 15.10:
{τ ∈ ℍ : -1/2 ≤ Re τ < 1/2, |τ| ≥ 1, and |τ| > 1 if Re τ > 0}.
Instances For
Membership in the textbook fundamental domain unfolded as the conjunction of its four defining inequalities.
The textbook fundamental domain is contained in the (closed) standard fundamental domain.
The open standard fundamental domain is contained in the textbook fundamental domain.
Effect of the S-action on the norm-square of τ:
|S τ|² = 1 / |τ|².
Effect of S on the real part: Re(S τ) = -Re τ / |τ|².
If Re τ = 1/2, the translation by T⁻¹ preserves the norm-square:
|T⁻¹ τ|² = |τ|².
Existence statement for Lemma 15.10: every τ ∈ ℍ is SL(2, ℤ)-equivalent
to a point of the textbook fundamental domain.
If z and g z both lie in the standard fundamental domain, then the
lower-left entry g 1 0 of g has absolute value at most one.
Uniqueness step for Lemma 15.10 in the case c = γ 1 0 = 1: if τ and
γ τ both lie in the textbook fundamental domain, then τ = γ τ.
Uniqueness statement for Lemma 15.10: if τ and γ τ both lie in the
textbook fundamental domain, then τ = γ τ.
Lemma 15.10 of the textbook: every τ ∈ ℍ has a unique
SL(2, ℤ)-translate lying in the textbook fundamental domain F.
Axiomatic input for Theorem 15.11: the image of the j-function is open
in ℂ. (Used together with closedness to show surjectivity onto ℂ.)
Axiomatic input for Theorem 15.11: the image of the j-function is closed
in ℂ. (Used together with openness to show surjectivity onto ℂ.)
The image of the j-function is an open subset of ℂ.
The image of the j-function is a closed subset of ℂ.
The j-function ℍ → ℂ is surjective: every complex number is a value of
j.
Every value of j is attained at some point of the standard fundamental
domain.
j is injective on the open standard fundamental domain.
Surjectivity of j restricted to the standard fundamental domain.
Injectivity of j restricted to the open standard fundamental domain.
Theorem 15.11 of the textbook: the restriction of the j-function to
the textbook fundamental domain F is a bijection from F to ℂ.
The short Weierstrass j-invariant of (A, B) = (-g₂/4, -g₃/4) agrees
with the lattice j-invariant jInvariantLattice L.
The discriminant 4 A³ + 27 B² of the elliptic curve associated to a
lattice with A = -g₂/4 and B = -g₃/4 is nonzero.
Two short Weierstrass curves y² = x³ + A x + B and y² = x³ + A' x + B'
with the same j-invariant are isomorphic via a Weierstrass variable change.
Handles the j = 0, j = 1728, and generic cases separately.
Uniformization up to isomorphism: every elliptic curve y² = x³ + A x + B
over ℂ is isomorphic, via a Weierstrass variable change, to the curve
y² = x³ - (g₂/4) x - (g₃/4) of some lattice L.
The lattice obtained from L by scaling by a nonzero complex number c:
its generators are c · ω₁ and c · ω₂.
Instances For
Equivalence between the scaled lattice scaleLattice c hc L and L,
implemented as multiplication by c⁻¹/c.
Instances For
The underlying value of scaleLatticeEquiv c hc L applied to a point l
of the scaled lattice equals c⁻¹ · l.
The underlying value of the inverse of scaleLatticeEquiv c hc L applied
to l of L equals c · l.
Scaling effect on g₂: g₂(cL) = c⁻⁴ · g₂(L).
Scaling effect on g₃: g₃(cL) = c⁻⁶ · g₃(L).
Corollary 15.12 (Uniformization Theorem): for every elliptic curve
y² = x³ + A x + B over ℂ there exists a lattice L such that the curve
equals E_L on the nose.