English
Translating a SlashInvariantForm by g ∈ GL2(ℝ) yields a new SlashInvariantForm on the conjugated level g⁻¹ Γ g with the same weight k, defined by the action f ∣[k] g.
Русский
Сдвиг SlashInvariantForm по g ∈ GL2(ℝ) даёт новую SlashInvariantForm на сопряжённом уровне g⁻¹ Γ g той же весовой характеристики k, определяемую действием f ∣[k] g.
LaTeX
$$$\text{translate}(f,g) : \mathrm{SlashInvariantForm}(g^{-1} \!Γ g, k)\text{ и } (\text{translate}(f,g))(\tau) = (f ∣[k] g)(\tau).$$$
Lean4
/-- Translating a `SlashInvariantForm` by `g : GL (Fin 2) ℝ`, to obtain a new
`SlashInvariantForm` of level `g⁻¹ Γ g`. -/
noncomputable def translate [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) :
SlashInvariantForm (toConjAct g⁻¹ • Γ) k where
toFun := f ∣[k] g
slash_action_eq' j
hj := by
rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj
simpa [← SlashAction.slash_mul] using congr_arg (· ∣[k] g) (slash_action_eqn f _ hj)
