大学院
変換の法則は、束ねた一つの等式です:許されたγすべてに対して f ∣[k] γ = f。
規則を保つ簡単な例なら、x²はxと−xで同じ答えです。スラッシュ作用では、関数の入力を変えるだけでなく、重さによって決まる数も掛けて、規則を調べます。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
入力の変換と、指定された数を掛ける操作の両方を見ます。x²の対称性は、考え方の入口の例です。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ、その因子も操作の一部。 入力の変換と、指定された数を掛ける操作の両方を見ます。x²の対称性は、考え方の入口の例です。
c = 0、d = 1の行列——τ ↦ aτ + bという形の変換——では、重さの因子(cτ + d)^{−k}がちょうど1になるので、要求は「f(aτ + b)とf(τ)を比べること」にまで減ります。
Mathlib · db584cd · SlashInvariantForms.lean
/-- Functions `ℍ → ℂ` that are invariant under the `SlashAction`. -/structure SlashInvariantForm where/-- The underlying function `ℍ → ℂ`.Do NOT use directly. Use the coercion instead. -/toFun : ℍ → ℂslash_action_eq' : ∀ γ ∈ Γ, toFun ∣[k] γ = toFun/-- `SlashInvariantFormClass F Γ k` asserts `F` is a type of bundled functions that are invariant
表示は構造の全部で、欄は二つ。toFunのコメントは、この欄を直接使わずcoercionを通すよう警告します。二つ目の欄「∀ γ ∈ Γ, toFun ∣[k] γ = toFun」は、作者が実際に検証して渡すべきデータです。
スラッシュ作用——重さの正確な規則
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
変換の法則は、束ねた一つの等式です:許されたγすべてに対して f ∣[k] γ = f。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
c = 0、d = 1の行列——τ ↦ aτ + bという形の変換——では、重さの因子(cτ + d)^{−k}がちょうど1になるので、要求は「f(aτ + b)とf(τ)を比べること」にまで減ります。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →