English
For γ ∈ SL(2,ℤ), the slash action reduces to (f ∣[k] γ)(τ) = f(γ · τ) denom(γ, τ)^{−k} (since det γ = 1).
Русский
Для γ ∈ SL(2,ℤ) slash-операция сводится к (f ∣[k] γ)(τ) = f(γ · τ) denom(γ, τ)^{−k} (так как det γ = 1).
LaTeX
$$$ (f \lvert[k] γ)(τ) = f(γ \cdot τ) \; \mathrm{denom}(γ, τ)^{-k} $$$
Lean4
/-- A function `f : ℍ → ℂ` is slash-invariant, of weight `k ∈ ℤ` and level `Γ`,
if for every matrix `γ ∈ Γ` we have `f(γ • z)= (c*z+d)^k f(z)` where `γ= ![![a, b], ![c, d]]`,
and it acts on `ℍ` via Möbius transformations. -/
theorem slash_action_eq'_iff (k : ℤ) (f : ℍ → ℂ) (γ : SL(2, ℤ)) (z : ℍ) :
(f ∣[k] γ) z = f z ↔ f (γ • z) = ((γ 1 0 : ℂ) * z + (γ 1 1 : ℂ)) ^ k * f z :=
by
simp only [SL_slash_apply]
convert inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2
· simp only [mul_comm (f _), denom, zpow_neg]
rfl
· exact zpow_ne_zero k (denom_ne_zero γ z)
