Equivalent lattices and scaling laws

Statements from chapter 3 of Milla (arXiv:1809.00533v6, file 080_Lattices.tex):

• PeriodPair.smul : the period pair a•L with periods (a·ω₁, a·ω₂) for a ∈ ℂˣ, generating the equivalent (rotated/scaled) lattice a·L;
• PeriodPair.discr, PeriodPair.J : the discriminant Δ(L) = g₂³ - 27g₃² and Klein's absolute invariant J(L) = g₂³/(g₂³ - 27g₃²) of a lattice (paper Def. defijdelta);
• the scaling laws G_n(aL) = a⁻ⁿG_n(L), g₂(aL) = a⁻⁴g₂(L), g₃(aL) = a⁻⁶g₃(L), Δ(aL) = a⁻¹²Δ(L), J(aL) = J(L) (paper trafog23), the function scaling laws ℘(az; aL) = a⁻²℘(z; L), ζ(az; aL) = a⁻¹ζ(z; L), σ(az; aL) = a·σ(z; L), and the quasiperiod scaling η_k(aL) = a⁻¹η_k(L) (paper etatransf).

All nontrivial proofs are sorry-ed for now; this file pins the statements.

def PeriodPair.smul (a : ℂˣ) (L : PeriodPair) : PeriodPair

The period pair a•L with periods (a·ω₁, a·ω₂), generating the equivalent lattice a·L (paper ch. 3: "equivalent lattices").

Equations

• PeriodPair.smul a L = { ω₁ := ↑a * L.ω₁, ω₂ := ↑a * L.ω₂, indep := ⋯ }

@[implicit_reducible]

instance PeriodPair.instSMulUnitsPeriodPair : SMul ℂˣ PeriodPair

Equations

• PeriodPair.instSMulUnitsPeriodPair = { smul := PeriodPair.smul }

@[simp]

theorem PeriodPair.smul_ω₁ (a : ℂˣ) (L : PeriodPair) : (a • L).ω₁ = ↑a * L.ω₁

@[simp]

theorem PeriodPair.smul_ω₂ (a : ℂˣ) (L : PeriodPair) : (a • L).ω₂ = ↑a * L.ω₂

theorem PeriodPair.mem_smul_lattice_iff (a : ℂˣ) (L : PeriodPair) (z : ℂ) : z ∈ (a • L).lattice ↔ ∃ w ∈ L.lattice, z = ↑a * w

The lattice of a•L is the scaled lattice a·L (paper ch. 3).

noncomputable def PeriodPair.smulLatticeEquiv (a : ℂˣ) (L : PeriodPair) : ↥L.lattice ≃ ↥(a • L).lattice

Multiplication by a as an equivalence between the lattice of L and that of a•L.

Equations

• PeriodPair.smulLatticeEquiv a L = { toFun := fun (l : ↥L.lattice) => ⟨↑a * ↑l, ⋯⟩, invFun := fun (z : ↥(a • L).lattice) => ⟨(↑a)⁻¹ * ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PeriodPair.smulLatticeEquiv_coe (a : ℂˣ) (L : PeriodPair) (l : ↥L.lattice) : ↑((smulLatticeEquiv a L) l) = ↑a * ↑l

noncomputable def PeriodPair.smulLatticeEquiv' (a : ℂˣ) (L : PeriodPair) : { l : ↥L.lattice // l ≠ 0 } ≃ { l : ↥(a • L).lattice // l ≠ 0 }

Multiplication by a as an equivalence between the nonzero lattice points of L and those of a•L.

Equations

• PeriodPair.smulLatticeEquiv' a L = (PeriodPair.smulLatticeEquiv a L).subtypeEquiv ⋯

@[simp]

theorem PeriodPair.smulLatticeEquiv'_coe (a : ℂˣ) (L : PeriodPair) (l : { l : ↥L.lattice // l ≠ 0 }) : ↑↑((smulLatticeEquiv' a L) l) = ↑a * ↑↑l

Termwise scaling identities (helpers)

The discriminant and Klein's absolute invariant (paper Def. defijdelta)

noncomputable def PeriodPair.discr (L : PeriodPair) : ℂ

The discriminant of a lattice, Δ(L) = g₂(L)³ - 27·g₃(L)² (paper Def. defijdelta).

Equations

• L.discr = L.g₂ ^ 3 - 27 * L.g₃ ^ 2

noncomputable def PeriodPair.J (L : PeriodPair) : ℂ

Klein's absolute invariant of a lattice, J(L) = g₂(L)³ / (g₂(L)³ - 27·g₃(L)²) (paper Def. defijdelta).

Equations

• L.J = L.g₂ ^ 3 / L.discr

Scaling laws (paper trafog23, etatransf)

theorem PeriodPair.G_smul (a : ℂˣ) (L : PeriodPair) (n : ℕ) : (a • L).G n = (↑a ^ n)⁻¹ * L.G n

Scaling law for the Eisenstein series: G_n(aL) = a⁻ⁿ·G_n(L) (paper trafog23).

theorem PeriodPair.g₂_smul (a : ℂˣ) (L : PeriodPair) : (a • L).g₂ = (↑a ^ 4)⁻¹ * L.g₂

Scaling law g₂(aL) = a⁻⁴·g₂(L) (paper trafog23).

theorem PeriodPair.g₃_smul (a : ℂˣ) (L : PeriodPair) : (a • L).g₃ = (↑a ^ 6)⁻¹ * L.g₃

Scaling law g₃(aL) = a⁻⁶·g₃(L) (paper trafog23).

theorem PeriodPair.discr_smul (a : ℂˣ) (L : PeriodPair) : (a • L).discr = (↑a ^ 12)⁻¹ * L.discr

Scaling law Δ(aL) = a⁻¹²·Δ(L) (paper trafog23).

theorem PeriodPair.J_smul (a : ℂˣ) (L : PeriodPair) : (a • L).J = L.J

Klein's absolute invariant is invariant under scaling: J(aL) = J(L) (paper trafog23).

theorem PeriodPair.weierstrassP_smul (a : ℂˣ) (L : PeriodPair) (z : ℂ) : (a • L).weierstrassP (↑a * z) = (↑a ^ 2)⁻¹ * L.weierstrassP z

Scaling law for the ℘-function: ℘(az; aL) = a⁻²·℘(z; L).

theorem PeriodPair.derivWeierstrassP_smul (a : ℂˣ) (L : PeriodPair) (z : ℂ) : (a • L).derivWeierstrassP (↑a * z) = (↑a ^ 3)⁻¹ * L.derivWeierstrassP z

Scaling law for ℘′: ℘'(az; aL) = a⁻³·℘'(z; L).

theorem PeriodPair.weierstrassZeta_smul (a : ℂˣ) (L : PeriodPair) (z : ℂ) : (a • L).weierstrassZeta (↑a * z) = (↑a)⁻¹ * L.weierstrassZeta z

Scaling law for the ζ-function: ζ(az; aL) = a⁻¹·ζ(z; L) (paper etatransf).

theorem PeriodPair.weierstrassSigma_smul (a : ℂˣ) (L : PeriodPair) (z : ℂ) : (a • L).weierstrassSigma (↑a * z) = ↑a * L.weierstrassSigma z

Scaling law for the σ-function: σ(az; aL) = a·σ(z; L).

theorem PeriodPair.eta₁_smul (a : ℂˣ) (L : PeriodPair) : (a • L).eta₁ = (↑a)⁻¹ * L.eta₁

Scaling law for the first quasiperiod: η₁(aL) = a⁻¹·η₁(L) (paper etatransf).

theorem PeriodPair.eta₂_smul (a : ℂˣ) (L : PeriodPair) : (a • L).eta₂ = (↑a)⁻¹ * L.eta₂

Scaling law for the second quasiperiod: η₂(aL) = a⁻¹·η₂(L) (paper etatransf).