The cube root γ₂ of the modular invariant j

Let g₀ = g_{(0, 1/2)}, g₁ = g_{(1/2, 0)} and g₂ = g_{(1/2, 1/2)} be the three Siegel functions of level two. This file proves Weber's identity

g₀⁴ + g₁⁴ + g₂⁴ = 0,

which in Weber's notation (g₀⁴ = 𝔣₂⁸, g₁⁴ = 𝔣₁⁸, g₂⁴ = -𝔣⁸) reads 𝔣₁⁸ + 𝔣₂⁸ = 𝔣⁸, and uses it to construct the holomorphic cube root

γ₂ = (g₀¹² + 16) / g₀⁴ = (g₁¹² + 16) / g₁⁴ = (g₂¹² + 16) / g₂⁴

of j. Weber's cubic (g¹² + 16)³ = j g¹² (siegelFunction_zero_half_pow_twelve_add_sixteen_pow_three and its companions) shows that each of the three quotients is a cube root of j; Weber's identity and g₀ g₁ g₂ = 2 ζ₈ show that they are the same function. The function γ₂ is invariant under S : τ ↦ -1/τ, is multiplied by e^{-2π i / 3} under T : τ ↦ τ + 1, and has leading Fourier term q^{-1/3}: γ₂(τ) e^{2π i τ / 3} → 1 at i∞. Its values at imaginary quadratic points enter the class number one problem.

Weber's identity is proved by comparing modular functions. With ω = e^{2π i / 3}, the function F = g₀⁴ + g₁⁴ + g₂⁴ satisfies F ∘ S = F and F ∘ T = ω F, because S exchanges g₀⁴ and g₁⁴ and fixes g₂⁴, while T multiplies g₀⁴ by ω and sends g₁⁴, g₂⁴ to ω g₂⁴, ω g₁⁴. Hence F³ is a holomorphic SL₂(ℤ)-invariant function. With s = e^{π i τ} and P(s) = ∏_{n ≥ 0} (1 - s^{2n+1}), the product expansions give g₀⁴ = 16 q^{1/3} / P(q)⁸ and g₁⁴ + g₂⁴ = s^{-1/3} (P(s)⁸ - P(-s)⁸) = q^{1/3} (P(s)⁸ - P(-s)⁸) / s, so F → 0 at i∞ and F³ is the constant 0 (TauCeti.ModularForm.levelOne_eq_of_tendsto_atImInfty).

Main definitions and results

• TauCeti.ModularForm.siegelFunction_pow_four_add_add: Weber's identity g₀⁴ + g₁⁴ + g₂⁴ = 0.
• TauCeti.ModularForm.gammaTwo: the function γ₂ = (g₀¹² + 16) / g₀⁴ on the upper half-plane.
• TauCeti.ModularForm.gammaTwo_eq_siegelFunction_zero_half, TauCeti.ModularForm.gammaTwo_eq_siegelFunction_half_zero, TauCeti.ModularForm.gammaTwo_eq_siegelFunction_half_half: γ₂ = (g¹² + 16) / g⁴ for each of g = g₀, g₁, g₂.
• TauCeti.ModularForm.gammaTwo_pow_three: γ₂³ = j.
• TauCeti.ModularForm.mdifferentiable_gammaTwo: γ₂ is holomorphic on the upper half-plane.
• TauCeti.ModularForm.gammaTwo_S_smul, TauCeti.ModularForm.gammaTwo_T_smul: γ₂ ∘ S = γ₂ and γ₂ ∘ T = e^{-2π i / 3} γ₂.
• TauCeti.ModularForm.tendsto_gammaTwo_mul_qParam_atImInfty: γ₂(τ) e^{2π i τ / 3} → 1 at i∞, so the leading Fourier term of γ₂ is q^{-1/3}.

References

• H. Weber, Lehrbuch der Algebra, Band III (the identity 𝔣₁⁸ + 𝔣₂⁸ = 𝔣⁸ and the cube root of j).
• D. A. Cox, Primes of the Form x² + ny², §12 (Weber's functions and γ₂ = (𝔣²⁴ - 16) / 𝔣⁸ = (𝔣₁²⁴ + 16) / 𝔣₁⁸ = (𝔣₂²⁴ + 16) / 𝔣₂⁸).
• D. H. Shin, Generation of class fields by Siegel–Ramachandra invariants, §5.

Roots of unity

Weber's identity

theorem TauCeti.ModularForm.siegelFunction_pow_four_add_add (τ : UpperHalfPlane) : siegelFunction ![0, 1 / 2] ↑τ ^ 4 + siegelFunction ![1 / 2, 0] ↑τ ^ 4 + siegelFunction ![1 / 2, 1 / 2] ↑τ ^ 4 = 0

Weber's identity g₀⁴ + g₁⁴ + g₂⁴ = 0 for the level-two Siegel functions g₀ = g_{(0, 1/2)}, g₁ = g_{(1/2, 0)} and g₂ = g_{(1/2, 1/2)}. In Weber's notation it reads 𝔣₁⁸ + 𝔣₂⁸ = 𝔣⁸.

The cube root γ₂ of j

noncomputable def TauCeti.ModularForm.gammaTwo (τ : UpperHalfPlane) : ℂ

The cube root γ₂ of j: γ₂(τ) = (g₀(τ)¹² + 16) / g₀(τ)⁴ for g₀ = g_{(0, 1/2)}. It is holomorphic on the upper half-plane, satisfies γ₂³ = j and has leading Fourier term q^{-1/3}.

theorem TauCeti.ModularForm.gammaTwo_eq_siegelFunction_zero_half (τ : UpperHalfPlane) : gammaTwo τ = (siegelFunction ![0, 1 / 2] ↑τ ^ 12 + 16) / siegelFunction ![0, 1 / 2] ↑τ ^ 4

γ₂ = (g₀¹² + 16) / g₀⁴ for g₀ = g_{(0, 1/2)}.

theorem TauCeti.ModularForm.gammaTwo_eq_siegelFunction_half_zero (τ : UpperHalfPlane) : gammaTwo τ = (siegelFunction ![1 / 2, 0] ↑τ ^ 12 + 16) / siegelFunction ![1 / 2, 0] ↑τ ^ 4

γ₂ = (g₁¹² + 16) / g₁⁴ for g₁ = g_{(1/2, 0)}.

theorem TauCeti.ModularForm.gammaTwo_eq_siegelFunction_half_half (τ : UpperHalfPlane) : gammaTwo τ = (siegelFunction ![1 / 2, 1 / 2] ↑τ ^ 12 + 16) / siegelFunction ![1 / 2, 1 / 2] ↑τ ^ 4

γ₂ = (g₂¹² + 16) / g₂⁴ for g₂ = g_{(1/2, 1/2)}.

@[simp]

theorem TauCeti.ModularForm.gammaTwo_pow_three (τ : UpperHalfPlane) : gammaTwo τ ^ 3 = j τ

γ₂ is a cube root of j: γ₂³ = j.

theorem TauCeti.ModularForm.mdifferentiable_gammaTwo : MDiff gammaTwo

γ₂ is holomorphic on the upper half-plane.

theorem TauCeti.ModularForm.gammaTwo_S_smul (τ : UpperHalfPlane) : gammaTwo (ModularGroup.S • τ) = gammaTwo τ

γ₂ is invariant under S : τ ↦ -1/τ.

theorem TauCeti.ModularForm.gammaTwo_T_smul (τ : UpperHalfPlane) : gammaTwo (ModularGroup.T • τ) = Complex.exp (-(2 * ↑Real.pi * Complex.I / 3)) * gammaTwo τ

γ₂ is multiplied by e^{-2π i / 3} under T : τ ↦ τ + 1.

theorem TauCeti.ModularForm.tendsto_gammaTwo_mul_qParam_atImInfty : Filter.Tendsto (fun (τ : UpperHalfPlane) => gammaTwo τ * Function.Periodic.qParam 3 ↑τ) UpperHalfPlane.atImInfty (nhds 1)

The leading Fourier term of γ₂ is q^{-1/3}: γ₂(τ) e^{2π i τ / 3} → 1 as Im τ → ∞.