Documentation

TauCeti.NumberTheory.ModularForms.SiegelFunction.Eta

The level-two Siegel functions as eta quotients #

The three Siegel functions of level two, g₀ = g_{(0, 1/2)}, g₁ = g_{(1/2, 0)} and g₂ = g_{(1/2, 1/2)}, are quotients of values of Mathlib's Dedekind eta function η = ModularForm.eta, with exact constants: g₀(τ) = 2 i (η(2τ) / η(τ))², g₁(τ) = -(η(τ/2) / η(τ))² and g₂(τ) = -e^{-π i / 3} (η((τ + 1)/2) / η(τ))². These follow from the product expansions of g₀, g₁, g₂ and the product identities for η at 2τ, τ/2 and (τ + 1)/2.

The transformation of η under S : τ ↦ -1/τ then gives the transformation of the level-two Siegel functions under S, with exact roots of unity: g₀(-1/τ) = -i g₁(τ), g₁(-1/τ) = i g₀(τ) and g₂(-1/τ) = g₂(τ); the last follows from the first two and g₀ g₁ g₂ = 2 ζ₈. Together with the translations τ ↦ τ + 1 (siegelFunction_zero_half_apply_add_one and its two companions) this shows that SL₂(ℤ) permutes the twelfth powers g₀¹², g₁¹², g₂¹²: S exchanges g₀¹² and g₁¹² and fixes g₂¹², while T fixes g₀¹² and exchanges g₁¹² and g₂¹². Equivalently, the monic cubic (X - g₀¹²)(X - g₁¹²)(X - g₂¹²) is invariant under SL₂(ℤ): its coefficients are SL₂(ℤ)-invariant holomorphic functions on the upper half-plane. This is the input for expressing the cube root γ₂ of j through the level-two Siegel functions.

Main results #

References #

Eta quotients #

source
theorem TauCeti.ModularForm.siegelFunction_zero_half_eq_eta {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![0, 1 / 2] τ = 2 * Complex.I * (ModularForm.eta (2 * τ) / ModularForm.eta τ) ^ 2

g_{(0, 1/2)}(τ) = 2 i (η(2τ) / η(τ))² on the upper half-plane.

source
theorem TauCeti.ModularForm.siegelFunction_half_zero_eq_eta {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![1 / 2, 0] τ = -(ModularForm.eta (τ / 2) / ModularForm.eta τ) ^ 2

g_{(1/2, 0)}(τ) = -(η(τ/2) / η(τ))² on the upper half-plane.

source
theorem TauCeti.ModularForm.siegelFunction_half_half_eq_eta {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![1 / 2, 1 / 2] τ = -Complex.exp (-(↑Real.pi * Complex.I / 3)) * (ModularForm.eta ((τ + 1) / 2) / ModularForm.eta τ) ^ 2

g_{(1/2, 1/2)}(τ) = -e^{-π i / 3} (η((τ + 1)/2) / η(τ))² on the upper half-plane.

The transformation τ ↦ -1/τ #

source
theorem TauCeti.ModularForm.siegelFunction_zero_half_apply_neg_one_div {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![0, 1 / 2] (-1 / τ) = -Complex.I * siegelFunction ![1 / 2, 0] τ

g₀(-1/τ) = -i g₁(τ) on the upper half-plane, where g₀ = g_{(0, 1/2)} and g₁ = g_{(1/2, 0)}.

source
theorem TauCeti.ModularForm.siegelFunction_half_zero_apply_neg_one_div {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![1 / 2, 0] (-1 / τ) = Complex.I * siegelFunction ![0, 1 / 2] τ

g₁(-1/τ) = i g₀(τ) on the upper half-plane, where g₀ = g_{(0, 1/2)} and g₁ = g_{(1/2, 0)}.

source
theorem TauCeti.ModularForm.siegelFunction_half_half_apply_neg_one_div {τ : ℂ} (hτ : 0 < τ.im) :
siegelFunction ![1 / 2, 1 / 2] (-1 / τ) = siegelFunction ![1 / 2, 1 / 2] τ

g₂(-1/τ) = g₂(τ) on the upper half-plane, where g₂ = g_{(1/2, 1/2)}.

The action of SL₂(ℤ) on the twelfth powers #

source
theorem TauCeti.ModularForm.prod_X_sub_C_siegelFunction_pow_twelve_smul (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) :
(Polynomial.X - Polynomial.C (siegelFunction ![0, 1 / 2] ↑(γ • τ) ^ 12)) * (Polynomial.X - Polynomial.C (siegelFunction ![1 / 2, 0] ↑(γ • τ) ^ 12)) * (Polynomial.X - Polynomial.C (siegelFunction ![1 / 2, 1 / 2] ↑(γ • τ) ^ 12)) = (Polynomial.X - Polynomial.C (siegelFunction ![0, 1 / 2] ↑τ ^ 12)) * (Polynomial.X - Polynomial.C (siegelFunction ![1 / 2, 0] ↑τ ^ 12)) * (Polynomial.X - Polynomial.C (siegelFunction ![1 / 2, 1 / 2] ↑τ ^ 12))

SL₂(ℤ) permutes the twelfth powers of the level-two Siegel functions: for every γ ∈ SL₂(ℤ) and τ in the upper half-plane, the monic cubic (X - g₀¹²)(X - g₁¹²)(X - g₂¹²) takes the same value at γ τ as at τ, where g₀ = g_{(0, 1/2)}, g₁ = g_{(1/2, 0)} and g₂ = g_{(1/2, 1/2)}.