ピップ
「二つの工房、違う仕事。ぼくはお茶係。急に身近な数学です。」
専門分野いろいろ物語 → 証明二つの工房は変形のデータとヘッケ側のデータ。比較する写像が、行き先のすべての要素に届くことを求めます。
すべての注文に届くFunction.Surjective φ「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
モジュラー性、3–5の切り替え、つながる部品。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
持ち上げの二つの側面と、その間をつなぐ写像の役割を知ろう。
元の原文 ↗ · L7–9固定版 aa2d8b3
theorem solution {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] {ρbar : ResidualGaloisRep (IsLocalRing.ResidueField 𝒪)} {𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop} (D : GaloisRep.DeformationRingData 𝒪 ρbar 𝒟) {N : ℕ} [NeZero N] {S : Set ℕ} {θ : CuspForm.heckeAlgebra N 2 S →+* IsLocalRing.ResidueField 𝒪} {T : Type} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [Algebra 𝒪 T] [IsLocalHom (algebraMap 𝒪 T)] [Module.Finite 𝒪 T] [Module.Free 𝒪 T] (H : CuspForm.HeckeGaloisRepDatum N S 𝒪 θ T) (hS : ∀ q : ℕ, q.Prime → q ∣ N → q ∈ S) (h𝒟 : 𝒟 H.ρ) (hres : H.ρ.residual.IsEquiv (ρbar.baseChangeAlong (IsLocalRing.ResidueField.map (algebraMap 𝒪 T)))) : ∃ φ : D.R →ₐ[𝒪] T, Function.Surjective φ ∧ ∃ hφ : IsLocalHom (φ : D.R →+* T), (D.ρ.baseChangeAlong (φ : D.R →+* T) hφ).IsEquiv H.ρ := by
obtain ⟨φ, ⟨hφ, he⟩, -⟩ := D.universal T H.residue_surjective H.ρ h𝒟 hres
exact ⟨φ, H.surjective_of_isEquiv_baseChangeAlong hS D.ρ φ hφ he, hφ, he⟩
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
一つ目の工房は、同じ余りの情報から認められる持ち上げを整理します。二つ目は、形式に対する算術の操作を整理します。普遍的な注文書から、二つを比べる写像が得られます。この抜粋は、行き先のすべてに届くことを示します。逆に戻れるところまでは、まだ主張しません。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 足し算とかけ算の仕組み足し算とかけ算の規則をそろえると、別の数の世界を同じ言葉で比べられます。
- 変形環と普遍性条件に合う持ち上げを、一つの代数的な対象からの写像で整理します。
- ヘッケ環カスプ形式への特別な操作と、それが持つ算術の情報を集めます。
- R = T——二つの工房をつなぐ等式持ち上げから作る環と、ヘッケ作用素から作る環を、一つの全射の写像で結びます。
- 全射と同型の違い全射はすべての出力先に届く写像。同型には、構造を保つ対応と逆対応があります。
物語 → 証明注文書は普遍性のたとえ。条件を満たす持ち上げから比較写像が決まり、好きな配線を選ぶわけではありません。
普遍性という注文書D.universalピップ
「比べる写像は、相手の工房のどんな注文にも届くの？ 面倒な注文にも？」
どの注文にも届く物語 → 証明すべて埋まるトレーの枠は全射性。どの注文にも届く理由は、ここで使う定理が与えます。
すべてに届く理由H.surjective_of_isEquiv_baseChangeAlong物語 → 証明橋と保証書は写像と整合性の証拠。全射だけで、同型まで保証されるわけではありません。
写像と整合性をそろえるhφ, he物語の向こうにある考え方
一つ目の工房は、同じ余りの情報から認められる持ち上げを整理します。二つ目は、形式に対する算術の操作を整理します。普遍的な注文書から、二つを比べる写像が得られます。この抜粋は、行き先のすべてに届くことを示します。逆に戻れるところまでは、まだ主張しません。
行き先すべてに届く写像なら、出発点も必ず一つずつ？
- いいえ。同じ行き先に複数から届くかもしれない。
- はい。全射なら一対一。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…