Auxiliary theorems for the slash actions groups SL(2, ℤ) and Γ(2)

Define special generators S, T, -I (resp. α, β, -I) for SL(2,ℤ) (resp. Γ(2)) and prove that they are indeed generators. As a corollary, we only need to check the invariance under these special elements to check the invariance under the whole group. These theorems will be used to prove that 4-th powers of Jacobi theta functions Θ_2^4, Θ_3^4, Θ_4^4 are modular forms of weight 2 and level Γ(2).

def α : ↥(CongruenceSubgroup.Gamma 2)

Equations

• α = ⟨⟨!![1, 2; 0, 1], α._proof_1⟩, α._proof_2⟩

def β : ↥(CongruenceSubgroup.Gamma 2)

Equations

• β = ⟨⟨!![1, 0; 2, 1], β._proof_1⟩, β._proof_2⟩

def negI : ↥(CongruenceSubgroup.Gamma 2)

Equations

• negI = ⟨⟨!![-1, 0; 0, -1], negI._proof_1⟩, negI._proof_2⟩

theorem α_eq_T_sq : α = ⟨ModularGroup.T ^ 2, ⋯⟩

theorem β_eq_negI_mul_S_mul_α_inv_mul_S : ↑β = ↑negI * ModularGroup.S * ↑α⁻¹ * ModularGroup.S

theorem ModularGroup.modular_negI_sq : negI ^ 2 = 1

theorem ModularGroup.modular_negI_inv : negI⁻¹ = negI

theorem modular_negI_smul (z : UpperHalfPlane) : ↑negI • z = z

theorem modular_slash_negI_of_even (f : UpperHalfPlane → ℂ) (k : ℤ) (hk : Even k) : SlashAction.map ℂ k (↑negI) f = f

theorem modular_slash_S_apply (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane) : SlashAction.map ℂ k ModularGroup.S f z = f (UpperHalfPlane.mk (-↑z)⁻¹ ⋯) * ↑z ^ (-k)

theorem modular_slash_T_apply (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane) : SlashAction.map ℂ k ModularGroup.T f z = f (1 +ᵥ z)

theorem SL2Z_generate : ⊤ = Subgroup.closure {ModularGroup.S, ModularGroup.T}

theorem Γ2_generate : ⊤ = Subgroup.closure {α, β, negI}

theorem slashaction_generators (f : UpperHalfPlane → ℂ) (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (s : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hG : G = Subgroup.closure s) (k : ℤ) : (∀ (γ : ↥G), SlashAction.map ℂ k (↑γ) f = f) ↔ ∀ γ ∈ s, SlashAction.map ℂ k γ f = f

If G is generated by a set s, then the slash action by elements in G is uniquely determined by the slash action by elements in s. See slashaction_generators' for a version where s is a set of elements in G.

theorem slashaction_generators' (f : UpperHalfPlane → ℂ) {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (s : Set ↥G) (hG : ⊤ = Subgroup.closure s) (k : ℤ) : (∀ (γ : ↥G), SlashAction.map ℂ k (↑γ) f = f) ↔ ∀ γ ∈ s, SlashAction.map ℂ k (↑γ) f = f

If G is generated by a set s, then the slash action by elements in G is uniquely determined by the slash action by elements in s. See slashaction_generators for a version where s is a set of elements in SL(2, ℤ).

theorem slashaction_generators_SL2Z (f : UpperHalfPlane → ℂ) (k : ℤ) (hS : SlashAction.map ℂ k ModularGroup.S f = f) (hT : SlashAction.map ℂ k ModularGroup.T f = f) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ k γ f = f

theorem slashaction_generators_Γ2 (f : UpperHalfPlane → ℂ) (k : ℤ) (hα : SlashAction.map ℂ k (↑α) f = f) (hβ : SlashAction.map ℂ k (↑β) f = f) (hnegI : SlashAction.map ℂ k (↑negI) f = f) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ CongruenceSubgroup.Gamma 2 → SlashAction.map ℂ k γ f = f