English
There is a natural additive map from the space of cusp forms of weight k for Γ into the space of functions on the upper half-plane with complex values; this map sends each cusp form f to the function z ↦ f(z) and preserves addition (and sends the zero cusp form to the zero function).
Русский
Существует естественное добавочно-однородное отображение между пространством cusp-форм весa k относительно Γ и пространством функций на верхней полуплоскости с комплексными значениями; отображение отправляет cusp-form f в функцию z ↦ f(z) и сохраняет сложение (нулевая cusp-form соответствует нулевой функции).
LaTeX
$$$coeHom: \mathrm{CuspForm}(\Gamma,k) \to^+ (\mathbb{H} \to \mathbb{C}),\quad f \mapsto (z \mapsto f(z)).$$$
Lean4
/-- Additive coercion from `CuspForm` to `ℍ → ℂ`. -/
@[simps]
def coeHom : CuspForm Γ k →+ ℍ → ℂ where
toFun f := f
map_zero' := CuspForm.coe_zero
map_add' _ _ := rfl
