3段階で考えよう
- 作用素は関数を操作します。固有関数は、関係する作用素によって自分自身の数倍へ送られる関数です。
- このリポジトリの重さ2のカスプ形式では、IsNormalizedEigenformが必要な算術を表す係数の等式を記録します。
- 正規化で1番目の係数を1に固定します。だから0の形式は除かれます。
小さな例で確かめる
mとnが互いに素なら、定義はa(mn) = a(m)a(n)を要求します。どんな数の列でも満たすわけではありません。
順番 50 / 64
大学
正規化された固有形式
係数の列に追加の算術規則があり、最初の係数を1にそろえます。
まず、身近な例で
数の組(1, b)を、「(u, v)を(v, 2u + v)にする機械」に入れます。b = 2なら(1, 2)が(2, 4)へ。もとの組のちょうど2倍です。ほかのbでも試そう。
この入力は、模型の機械で全体が2倍になります。
この例と、本当の定義の違い
この2個の数の機械は、モジュラー形式に働くヘッケ作用素ではありません。「全体が何倍かになる」という考え方だけの模型です。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
1→2も2→4も2倍です。bを3に変えると、どの入力でもこの形になるわけではないと分かります。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
両方の数が同じ2倍になった。 1→2も2→4も2倍です。bを3に変えると、どの入力でもこの形になるわけではないと分かります。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean
structure IsNormalizedEigenform {N : ℕ} (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) :Prop whereqCoeff_one : qCoeff f 1 = 1qCoeff_mul_of_coprime : ∀ m n : ℕ, m.Coprime n →qCoeff f (m * n) = qCoeff f m * qCoeff f nqCoeff_prime_pow_of_not_dvd : ∀ p r : ℕ, p.Prime → ¬ p ∣ N →qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1)) - p * qCoeff f (p ^ r)qCoeff_prime_pow_of_dvd : ∀ p r : ℕ, p.Prime → p ∣ N →qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1))
このLeanの読み方
qCoeff_oneが正規化。その後の欄は積の規則と素数の累乗での漸化式（前の係数から次の係数を決める規則）を記録し、素数がレベルを割るかどうかで分けています。