English
If a and b are integers and Γ is a subgroup with det ±1, then casting a modular form of weight a to weight b along an equality a = b yields a modular form of weight b; more generally, mcast transports modular forms along equal weights.
Русский
Если a и b — целые числа и Γ — подгруппа с детерминантом ±1, то отображение mcast, при равенстве весов a = b, переводит модульную форму веса a в вес b; в общем случае mcast переносит модульные формы вдоль равных весов.
LaTeX
$$$\mathrm{mcast}: a,b,Γ \text{ with } a=b \to \mathrm{ModularForm}(\Gamma,b)\;\text{from } \mathrm{ModularForm}(\Gamma,a).$$$
Lean4
/-- Cast for modular forms, which is useful for avoiding `Heq`s. -/
def mcast {a b : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a) : ModularForm Γ b
where
toFun := (f : ℍ → ℂ)
slash_action_eq' A := h ▸ f.slash_action_eq' A
holo' := f.holo'
bdd_at_cusps' A := h ▸ f.bdd_at_cusps' A
