Lean 4でエタール・コホモロジーを
セルフコンテインドに理解する。
環・スキーム・層・導来関手。

00 — GOAL

先に結論のコードを置く

このノートは長い。だから到達地点を先に見せる。最後の章で、エタール・コホモロジーはこう定義される。

/-- 定理（十分な入射的対象の存在）: すべてのアーベル層は入射的分解を持つ。 -/
theorem exists_injectiveResolution {X : Scheme} (F : AbSheaf (etaleSite X)) :
    Nonempty (InjectiveResolution F) := sorry

/-- **エタール・コホモロジー** `Hⁿ(X_ét, F)`。
入射的分解 `F → I•` を一つ選び、大域切断の複体 `Γ(X, I•)` の `n` 次コホモロジーを取る。 -/
noncomputable def etaleCohomology (X : Scheme) (F : AbSheaf (etaleSite X)) (n : Nat) : Type :=
  (globalSections (Classical.choice (exists_injectiveResolution F))).H n

数式で書けば、グロタンディークの定義そのものである。アーベル層 \(\mathcal F\) の入射的分解 \(0 \to \mathcal F \to \mathcal I^0 \to \mathcal I^1 \to \cdots\) を取り、大域切断を取ってから複体のコホモロジーを取る。

\[ H^n(X_{\mathrm{ét}}, \mathcal F) \;:=\; H^n\bigl(\Gamma(X, \mathcal I^{\bullet})\bigr) \;=\; \frac{\ker\bigl(\Gamma(X,\mathcal I^n) \to \Gamma(X,\mathcal I^{n+1})\bigr)}{\operatorname{im}\bigl(\Gamma(X,\mathcal I^{n-1}) \to \Gamma(X,\mathcal I^{n})\bigr)}. \]

たった数行である。一方で、この数行が型検査を通るためには、その手前で Scheme、etaleSite、AbSheaf、InjectiveResolution、Cocomplex.H がすべて定義されていなければならない。しかもそれぞれが、さらに手前の CommRing、Ideal、PrimeSpectrum、Sheaf、Sieve に依存している。このノートの残りは、その依存の鎖を一番下の「可換環」から順に、一つずつ自分の手で書いていく作業である。

方針: Mathlibを使わない

Lean 4には Mathlib という巨大な数学ライブラリがあり、実はスキームもエタール射もその上の層コホモロジーも、すでに定義されている（最後の章で対応表を付ける）。しかし、このノートでは Mathlib を一行も import しない。使うのは Lean 4 本体に入っている Type、Prop、Nat、Int、Fin、List、Quot だけである。理由は二つある。

1. 依存を隠さないため

   ライブラリの Scheme を呼んだ瞬間、その裏にある数千行が見えなくなる。「セルフコンテインド」とは、必要な定義がすべて一つのファイルの中に、読める順番で並んでいる状態のことである。

2. 定義の骨格だけを見るため

   Mathlibの定義は一般性と効率のために複雑になっている。教科書の定義をそのまま写した素朴な版のほうが、数学者には読みやすい。

このノートに出てくるLeanコードは、全部で一つのファイル Etale.lean（約1000行）になっていて、Lean 4.33.1 で型検査が通ることを確認している。ただし、すべてを証明したわけではない。ファイルには78個の sorry（証明の穴）がある。穴は二種類に分けてラベルを付けた。

1. 演習 定義に伴う routine な検証

   「局所化の足し算が代表元の取り方によらない」「制限写像が合成を保つ」など。数学的には自明だが、Leanで書くと数十行になる。証明の穴として残し、定義そのものの見通しを優先した。

2. 定理 本物の定理

   「エタール被覆はファイバー積で保たれる」「アーベル層の圏は十分な入射的対象を持つ」「Kummer列は完全」など。これらは教科書で数ページから数十ページの証明を要する。ノートでは「命題の型だけを正確に書き」、証明は sorry にしている。

「定義はすべて自分の手で書いてあり、定理は正確に述べられているが証明はない」。これがこのノートの到達点である。定義が正しく型検査を通るということは、少なくとも「エタール・コホモロジーとは何か」を言うために必要な概念がすべて揃っていて、依存関係に穴がないことを機械が確認したことになる。

三段階で書く

各章は同じ構成で進む。まず日常語でその概念が「何をしたいのか」を言い、次に数式で定義し、最後にLeanで書く。そして Lean の各フィールドが数式のどの部分に対応するかを読み解く。冗長に見えるかもしれないが、Lean のコードが読めるようになるのは、「この記号はあの引数」という対応が見えたときだけだからである。

01 — LEAN PRIMER

数学者のためのLean 4の基礎文法

Lean 4は、プログラミング言語であり、同時に証明支援系である。数学者向けに雑にいうと、「集合」の代わりに「型」を使う集合論の方言で、しかも命題も型の一種として扱う。この一点を飲み込めば、あとは記法の問題である。以下、このノートを読むのに必要な最小限だけを説明する。

1. すべては「項 : 型」

数学で \(x \in \mathbb N\) と書くところを、Leanでは x : ℕ と書く。コロンの右が型、左がその型の項（要素）である。関数 \(f : \mathbb N \to \mathbb N\) も f : Nat → Nat で、\(f(x)\) は括弧なしで f x と書く。二変数関数は f x y。

def double (n : Nat) : Nat := 2 * n      -- 定義。n ↦ 2n
#eval double 21                            -- 42

def compose {α β γ : Type} (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)                          -- λ記法。x ↦ g(f(x))

波括弧 {α β γ : Type} は暗黙引数で、使うときに書かなくてよい（\(g\) と \(f\) の型から推論される）。数学で「明らかな添字は省略する」のと同じ習慣を、機械にやらせている。

2. 部分集合は述語、存在は ∃

このノートでは \(X\) の部分集合を、述語 X → Prop として表す。「\(x \in U\)」は U x（\(U\) が \(x\) で真）と書く。数学では \(U \subseteq X\) と \(\chi_U : X \to \{0,1\}\) を同一視するが、それを常に後者で書く、ということである。「\(U\) を満たす \(x\) の型」は { x : X // U x }（部分型）と書く。

\[ U \subseteq X \;\leftrightarrow\; \texttt{U : X → Prop}, \qquad \{x \in X \mid U(x)\} \;\leftrightarrow\; \texttt{\{ x : X // U x \}} \]

存在命題 \(\exists x,\ P(x)\) は ∃ x, P x。証明項は ⟨x, h⟩（証人と、その証人が条件を満たす証明の組）。「ただ一つ存在する」は Lean 本体には記法がないので、このノートでは ∃ t, P t ∧ ∀ t', P t' → t' = t と展開して書く。

3. 命題は型、証明は項

ここが一番の飛躍である。Leanでは命題 \(P\) も一つの型 P : Prop であり、\(P\) の証明とは、型 P の項のことである。だから「定理」とは、ある型の項を一つ作って見せることに他ならない。

\[ \underbrace{h}_{\text{証明}} : \underbrace{\forall n : \mathbb N,\ n + 0 = n}_{\text{命題（型）}} \]

theorem add_zero' (n : Nat) : n + 0 = n := rfl
-- `rfl` は「定義により両辺が同じ」という証明項。

example : ∀ n : Nat, n + 0 = n := by
  intro n        -- ∀ を剥がして n を固定する
  rfl

theorem two_mul' (n : Nat) : 2 * n = n + n := by omega   -- 線形算術は自動

by 以下はタクティクと呼ばれる。「証明項を直接書く」のではなく、「証明項を組み立てる手順を指示する」モードである。数学の証明を口述するときの「\(n\) を任意に取る」「両辺を書き換える」「仮定を適用する」が、そのまま intro、rw、exact に対応する。このノートで使うものだけ表にしておく。

4. 構造と型クラス: 「\(R\) を可換環とする」の書き方

数学の教科書は「\(R\) を可換環とする」と一行で言う。Leanでこれに当たるのが structure と class である。structure は「データの束」で、フィールドを持つ。たとえば「点 \(x\) の近傍で定義された切断」は、開集合 \(U\)、\(x \in U\) の証明、\(U\) 上の切断 \(s\) の三つ組であり、これを三つのフィールドを持つ構造体として書く。

class は「型に載せる構造」で、角括弧 [CommRing R] で引数に書くと、Leanはその構造を勝手に探して持ち回ってくれる。これを型クラスのインスタンス解決と呼ぶ。「\(a + b\)」と書いたとき、どの足し算かをいちいち書かなくてよいのはこの仕組みのおかげである。

-- 「三つ組」を表す構造体。フィールドは `.U` `.mem` `.s` で取り出す。
structure Triple (X : Type) (P : X → Prop) where
  U   : X
  mem : P U
  s   : Nat

-- 型クラス。`[Foo α]` と書けば、Lean が `Foo α` のインスタンスを探す。
class Foo (α : Type) where
  op : α → α → α

instance : Foo Nat := ⟨fun a b => a + b⟩     -- Nat に Foo 構造を与える

example {α : Type} [Foo α] (a : α) : α := Foo.op a a

命題だけからなる構造体は Prop 値になる。「\(P\) が素イデアルである」のような性質は、フィールドがすべて命題の構造体か、単に def ... : Prop で書く。

5. 商: Quot

数学では同値関係で割る操作を日常的に使う。局所化 \(S^{-1}R\)、茎 \(\mathcal F_x\)、コホモロジー \(Z^n/B^n\) はすべて商である。Lean 4 本体には Quot r がある。r : α → α → Prop を関係とするとき、Quot r は「\(\alpha\) を \(r\) の生成する同値関係で割った型」で、次の三つの操作を持つ。

1. Quot.mk r a

   \(a\) の同値類 \([a]\)。

2. Quot.sound : r a b → Quot.mk r a = Quot.mk r b

   関係している元は同じ類になる。

3. Quot.lift f h : Quot r → β

   「代表元によらない」写像 \(f\)（証明 h : ∀ a b, r a b → f a = f b 付き）を商から定義する。数学で「well-defined」を確認する作業がここに対応する。

6. 宇宙: Type と Type 1

「すべてのスキームの型」は集合ではない。Leanでは、Type の要素（普通の型）を集めた型は一つ上の Type 1 に住む。このノートでは、可換環や位相空間の台は Type、「スキーム全体」や「\(X\) 上エタールなスキーム全体」は Type 1 になる。圏の定義に universe u と Type u が出てくるのはそのためで、グロタンディーク宇宙と同じ話だと思ってよい。

これで道具はそろった。以下は、この記法で数学を一段ずつ書いていく。

02 — COMMUTATIVE RINGS

可換環を定義する

一番下から始める。可換環とは、雑にいうと「足し算・引き算・掛け算ができて、掛け算の順序を気にしなくてよい数の体系」である。整数 \(\mathbb Z\)、多項式 \(\mathbb Z[x]\)、\(\mathbb Z/n\mathbb Z\)、関数の環 \(C(X)\)。これから作るスキームとは、「可換環を幾何学的な空間だと思い直したもの」なので、環の定義が土台になる。

数式で書けば、集合 \(R\) と演算 \(+, \cdot\)、元 \(0, 1\)、写像 \(-\) であって次を満たすもの。

\[ \begin{aligned} &(a+b)+c = a+(b+c),\quad a+b=b+a,\quad 0+a=a,\quad (-a)+a=0,\\ &(ab)c=a(bc),\quad ab=ba,\quad 1\cdot a=a,\quad a(b+c)=ab+ac. \end{aligned} \]

Leanではこれをそのまま class として書く。

/-- 可換環。台となる型 `R` に、足し算・掛け算・マイナス・0・1 と、8つの公理を載せたもの。 -/
class CommRing (R : Type) extends Add R, Mul R, Neg R, Zero R, One R where
  add_assoc : ∀ a b c : R, a + b + c = a + (b + c)
  add_comm  : ∀ a b : R, a + b = b + a
  zero_add  : ∀ a : R, 0 + a = a
  neg_add_cancel : ∀ a : R, -a + a = 0
  mul_assoc : ∀ a b c : R, a * b * c = a * (b * c)
  mul_comm  : ∀ a b : R, a * b = b * a
  one_mul   : ∀ a : R, 1 * a = a
  mul_add   : ∀ a b c : R, a * (b + c) = a * b + a * c

読み方。extends Add R, Mul R, Neg R, Zero R, One R は「\(R\) には +、*、-、0、1 の記号が使える」と宣言する部分で、Lean 本体にある記号用の小さな型クラスを継承している。その下の8行が公理で、一行が数式の一つに対応している。可換環とは、この8つの命題の証明を持った型のことである。それ以上でも以下でもない。

8つで足りるのか、と思うかもしれない。\(a + 0 = a\) や \(a \cdot 0 = 0\) が抜けている。それらは定理であって公理ではない。次のブロックで証明する。

整数は可換環である

定義したら、まず例を一つ作る。\(\mathbb Z\) に CommRing 構造を与えるには、8つの公理の証明を用意すればよい。Lean 本体には整数の基本補題が入っているので、名前を並べるだけで済む。

/-- 整数 `ℤ` は可換環である。公理はすべて Lean コアの補題で埋まる。 -/
instance : CommRing Int where
  add_assoc := Int.add_assoc
  add_comm  := Int.add_comm
  zero_add  := Int.zero_add
  neg_add_cancel := Int.add_left_neg
  mul_assoc := Int.mul_assoc
  mul_comm  := Int.mul_comm
  one_mul   := Int.one_mul
  mul_add   := Int.mul_add

example : (2 : Int) * 3 + -6 = 0 := rfl
example (R : Type) [CommRing R] (a : R) : a * 1 = 1 * a := CommRing.mul_comm a 1

example : (2 : Int) * 3 + -6 = 0 := rfl は、具体的な整数の計算が「定義により明らか」（rfl）で通ることを示している。二つ目の example は、任意の可換環 \(R\) で \(a \cdot 1 = 1 \cdot a\) が、公理 mul_comm を \(a, 1\) に適用するだけで出ることを示す。公理は「関数」であり、具体的な元を渡すと証明が返ってくるという感覚をここで掴んでほしい。

公理から出る基本補題

次に、後で必要になる補題を公理から導く。\(a + 0 = a\)、\(a\cdot 0 = 0\)、\(-(a+b) = -a + -b\) など。ここは数学的には全く面白くないが、「公理を8つに絞った代償として、これだけの補題を自分で埋める必要がある」ことを一度見ておく価値はある。

section RingLemmas
variable {R : Type} [CommRing R]
open CommRing

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]
theorem add_neg_cancel (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]
theorem mul_one (a : R) : a * 1 = a := by rw [mul_comm, one_mul]
theorem add_mul (a b c : R) : (a + b) * c = a * c + b * c := by
  rw [mul_comm, mul_add, mul_comm c, mul_comm c]

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  have h' : -a + (a + b) = -a + (a + c) := congrArg (fun x => -a + x) h
  rwa [← add_assoc, ← add_assoc, neg_add_cancel, zero_add, zero_add] at h'

theorem mul_zero (a : R) : a * 0 = 0 := by
  apply add_left_cancel (a := a * 0)
  rw [← mul_add, zero_add, add_zero]
theorem zero_mul (a : R) : 0 * a = 0 := by rw [mul_comm, mul_zero]
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  apply add_left_cancel (a := a)
  rw [h, add_neg_cancel]
theorem mul_neg (a b : R) : a * -b = -(a * b) := by
  symm; apply neg_eq_of_add_eq_zero
  rw [← mul_add, add_neg_cancel, mul_zero]
theorem neg_add (a b : R) : -(a + b) = -a + -b := by
  apply neg_eq_of_add_eq_zero
  -- ゴール: (a + b) + (-a + -b) = 0
  rw [add_assoc, add_comm b, add_assoc, neg_add_cancel, add_zero, add_neg_cancel]
end RingLemmas

たとえば mul_zero の証明を読む。示したいのは \(a \cdot 0 = 0\)。add_left_cancel（\(a + b = a + c \Rightarrow b = c\)）を \(a \cdot 0\) について適用すると、ゴールは \(a\cdot 0 + a \cdot 0 = a \cdot 0 + 0\) になる。左辺は分配法則を逆に使って \(a \cdot (0 + 0)\)、これは \(a \cdot 0\)。右辺も \(a \cdot 0\)。数学の教科書の最初の演習問題と、寸分違わない議論である。rw [← mul_add, zero_add, add_zero] という一行が、その三ステップにそれぞれ対応している。

03 — RING HOMOMORPHISMS

環準同型と、その核

環を定義したら、環と環の間の「正しい写像」を定義する。環準同型とは足し算・掛け算・1 を保つ写像である。

\[ f : R \to S,\qquad f(a+b)=f(a)+f(b),\quad f(ab)=f(a)f(b),\quad f(1)=1. \]

/-- 環準同型。写像であって、足し算・掛け算・1 を保つもの。 -/
structure RingHom (R S : Type) [CommRing R] [CommRing S] where
  toFun   : R → S
  map_add : ∀ a b, toFun (a + b) = toFun a + toFun b
  map_mul : ∀ a b, toFun (a * b) = toFun a * toFun b
  map_one : toFun 1 = 1

infixr:25 " →ᵣ " => RingHom

instance {R S : Type} [CommRing R] [CommRing S] : CoeFun (R →ᵣ S) (fun _ => R → S) :=
  ⟨RingHom.toFun⟩

section HomLemmas
variable {R S T : Type} [CommRing R] [CommRing S] [CommRing T]

theorem RingHom.map_zero (f : R →ᵣ S) : f 0 = 0 := by
  apply add_left_cancel (a := f 0)
  rw [← f.map_add, CommRing.zero_add, add_zero]

theorem RingHom.map_neg (f : R →ᵣ S) (a : R) : f (-a) = -(f a) := by
  symm; apply neg_eq_of_add_eq_zero
  rw [← f.map_add, add_neg_cancel, f.map_zero]

/-- 恒等写像は環準同型。 -/
def RingHom.id (R : Type) [CommRing R] : R →ᵣ R :=
  ⟨fun a => a, fun _ _ => rfl, fun _ _ => rfl, rfl⟩

/-- 環準同型の合成。 -/
def RingHom.comp (g : S →ᵣ T) (f : R →ᵣ S) : R →ᵣ T where
  toFun a := g (f a)
  map_add a b := by rw [f.map_add, g.map_add]
  map_mul a b := by rw [f.map_mul, g.map_mul]
  map_one := by rw [f.map_one, g.map_one]

/-- 環準同型の相等は写像の相等で決まる。 -/
theorem RingHom.ext {f g : R →ᵣ S} (h : ∀ a, f a = g a) : f = g := by
  cases f; cases g
  have : _ = _ := funext h
  simp only at this
  subst this
  rfl
end HomLemmas

読み方。structure RingHom は「写像 toFun と三つの性質の証明」の束である。infixr:25 " →ᵣ " は記法の宣言で、以後 R →ᵣ S と書ける。CoeFun のインスタンスは、f : R →ᵣ S を関数のように f a と書くための約束である。数学で \(f\) と「\(f\) の台となる写像」を区別しないのと同じことを、Leanでは明示的に宣言する。

\(f(0) = 0\) が公理に入っていないことに注意。これも定理である（RingHom.map_zero）。証明は「\(f(0) = f(0+0) = f(0)+f(0)\) から消去」で、前章の add_left_cancel をそのまま使っている。

一方で、恒等写像と合成は定義である。RingHom.comp g f は \(g \circ f\)。三つの性質は、\(f\) と \(g\) の性質を順に書き換えれば出る（rw [f.map_add, g.map_add]）。

04 — IDEALS

イデアル、素イデアル、局所環

イデアルは、雑にいうと「0 の仲間」の集まりである。環 \(R\) から商環 \(R/I\) を作るとき、\(I\) の元はすべて 0 になる。だから \(I\) は 0 を含み、足し算で閉じ、何を掛けても閉じていなければならない。

\[ 0 \in I,\qquad a, b \in I \Rightarrow a + b \in I,\qquad r \in R,\ a \in I \Rightarrow ra \in I. \]

section Ideals
variable {R : Type} [CommRing R]

/-- イデアル。0 を含み、足し算で閉じ、環の元を掛けても閉じている部分集合。 -/
structure Ideal (R : Type) [CommRing R] where
  carrier  : R → Prop
  zero_mem : carrier 0
  add_mem  : ∀ {a b}, carrier a → carrier b → carrier (a + b)
  mul_mem  : ∀ (r : R) {a}, carrier a → carrier (r * a)

instance : Membership R (Ideal R) := ⟨fun I a => I.carrier a⟩

carrier : R → Prop が「\(I\) の元であるという述語」で、前章で述べた「部分集合は述語」の約束に沿っている。instance : Membership は、以後 a ∈ I と書けるようにする宣言である。

素イデアルは「点」になる

次が、代数幾何の最初の飛躍である。素イデアルとは、「積が入っていればどちらかが入っている」イデアルであり、これを空間の点だと思う。なぜか。関数環 \(C(X)\) では、点 \(x\) に対して「\(x\) で消える関数全体」\(\mathfrak m_x = \{f \mid f(x)=0\}\) は素イデアルになる（\(f(x)g(x)=0\) なら \(f(x)=0\) か \(g(x)=0\)）。この対応を逆に使って、任意の環に対して「点とは素イデアルのことである」と定義してしまう。

\[ \mathfrak p \text{ が素イデアル } \iff 1 \notin \mathfrak p \ \text{かつ}\ \bigl(ab \in \mathfrak p \Rightarrow a \in \mathfrak p \lor b \in \mathfrak p\bigr). \]

/-- 素イデアル。全体ではなく、`ab ∈ P` なら `a ∈ P` か `b ∈ P`。 -/
def Ideal.IsPrime (P : Ideal R) : Prop :=
  (1 : R) ∉ P ∧ ∀ {a b : R}, a * b ∈ P → a ∈ P ∨ b ∈ P

/-- 可逆元（単元）。 -/
def IsUnit (a : R) : Prop := ∃ b, a * b = 1

/-- 局所環。`0 ≠ 1` で、任意の `a` について `a` か `1 - a` が可逆。
（「非可逆元全体がイデアルになる」「極大イデアルがただ一つ」と同値。） -/
def IsLocalRing (R : Type) [CommRing R] : Prop :=
  (0 : R) ≠ 1 ∧ ∀ a : R, IsUnit a ∨ IsUnit (1 + -a)

/-- 局所準同型。非可逆元を非可逆元へ送る（同じことだが、`φ a` が可逆なら `a` も可逆）。 -/
def RingHom.IsLocal {S : Type} [CommRing S] (φ : R →ᵣ S) : Prop :=
  ∀ a : R, IsUnit (φ a) → IsUnit a

ここで一緒に、可逆元と局所環も定義している。局所環とは極大イデアルがただ一つの環で、幾何学的には「一点の近くだけを見た環」である。教科書の定義は「極大イデアルがただ一つ」だが、それを言うには極大イデアルの定義と存在定理が要る。ここでは同値な、より初等的な条件を採用した。

\[ R \text{ が局所環 } \iff 0 \ne 1 \ \text{かつ}\ \forall a \in R,\ a \in R^\times \ \lor\ 1 - a \in R^\times. \]

直感はこうである。局所環では「非可逆元全体」がちょうど唯一の極大イデアル \(\mathfrak m\) になる。だから \(a\) と \(1-a\) が両方非可逆なら、両方 \(\mathfrak m\) に入り、和 \(1\) も \(\mathfrak m\) に入ってしまい矛盾する。逆も同様に示せる。RingHom.IsLocal は局所環の間の局所準同型で、「極大イデアルを極大イデアルに送る」ことを「非可逆元を非可逆元に送る」と言い換えたものである。これはスキームの射の定義で本当に使う。

核と、有限生成

準同型の核 \(\ker f = \{a \mid f(a) = 0\}\) はイデアルである。また有限個の元 \(x_1, \dots, x_n\) が生成するイデアル \((x_1,\dots,x_n)\) は、有限和 \(\sum r_i x_i\) 全体である。有限生成は、後で「有限表示」を定義するときに使う。

/-- 環準同型の核 `ker f = {a | f a = 0}` はイデアル。 -/
def RingHom.ker {S : Type} [CommRing S] (f : R →ᵣ S) : Ideal R where
  carrier a := f a = 0
  zero_mem := f.map_zero
  add_mem {a b} ha hb := by
    show f (a + b) = 0
    rw [f.map_add, ha, hb, add_zero]
  mul_mem r {a} ha := by
    show f (r * a) = 0
    rw [f.map_mul, ha, mul_zero]

/-- 有限個の元 `l = [x₁, …, xₙ]` が生成するイデアルの元、すなわち有限和 `Σ rᵢ xᵢ`。 -/
inductive InSpan (l : List R) : R → Prop
  | zero : InSpan l 0
  | add {a b} : InSpan l a → InSpan l b → InSpan l (a + b)
  | smul (r : R) {x} : x ∈ l → InSpan l (r * x)

/-- `span l = (x₁, …, xₙ)`。 -/
def Ideal.span (l : List R) : Ideal R where
  carrier := InSpan l
  zero_mem := InSpan.zero
  add_mem := InSpan.add
  mul_mem r {a} ha := by
    induction ha with
    | zero => rw [mul_zero]; exact InSpan.zero
    | add _ _ iha ihb => rw [CommRing.mul_add]; exact InSpan.add iha ihb
    | smul s hx => rw [← CommRing.mul_assoc]; exact InSpan.smul (r * s) hx

/-- 有限生成イデアル。 -/
def Ideal.IsFG (I : Ideal R) : Prop := ∃ l : List R, ∀ a, a ∈ I ↔ InSpan l a
end Ideals

InSpan は帰納的に定義された述語で、「0 は入っている」「入っているものの和は入っている」「生成元の \(r\) 倍は入っている」の三つの規則で生成される最小の述語である。これは \(\sum r_i x_i\) という有限和の、集合を使わない言い換えになっている。有限集合の代わりに List R（元のリスト）を使うのは、Lean 本体だけで済ませるための素朴な選択である。Ideal.span の mul_mem の証明は、この帰納的定義に対する帰納法で、三つの場合をそれぞれ潰している。

05 — SPECTRUM

Spec R と、ザリスキ位相

前章で「点とは素イデアル」と決めた。すると環 \(R\) から空間が一つ決まる。それが素スペクトル \(\operatorname{Spec} R\) である。

\[ \operatorname{Spec} R := \{\, \mathfrak p \subseteq R \mid \mathfrak p \text{ は素イデアル} \,\}. \]

雑にいうと、環 \(R\) の元 \(a\) を「\(\operatorname{Spec} R\) 上の関数」だと思い、\(a \in \mathfrak p\) を「\(a\) は点 \(\mathfrak p\) で消える」と読む。この読み替えで、\(E \subseteq R\) の「零点集合」\(V(E)\) と、\(f\) の「消えない場所」\(D(f)\) が定義できる。

\[ V(E) := \{\mathfrak p \mid E \subseteq \mathfrak p\},\qquad D(f) := \{\mathfrak p \mid f \notin \mathfrak p\} = \operatorname{Spec} R \setminus V(\{f\}). \]

section Spectrum
variable (R : Type) [CommRing R]

/-- 素スペクトル `Spec R`。点は `R` の素イデアル。 -/
def PrimeSpectrum : Type := { P : Ideal R // P.IsPrime }

variable {R}

/-- 零点集合 `V(E) = { 𝔭 | E ⊆ 𝔭 }`。「E の元がすべて消える点」。 -/
def zeroLocus (E : R → Prop) : PrimeSpectrum R → Prop :=
  fun P => ∀ a, E a → a ∈ P.1

/-- 基本開集合 `D(f) = { 𝔭 | f ∉ 𝔭 }`。「f が消えない点」。 -/
def basicOpen (f : R) : PrimeSpectrum R → Prop :=
  fun P => f ∉ P.1

PrimeSpectrum R は部分型 { P : Ideal R // P.IsPrime }、つまり「素イデアルであることの証明付きのイデアル」の型である。P.1 でイデアル本体、P.2 で素であることの証明が取れる。zeroLocus E と basicOpen f は PrimeSpectrum R → Prop、すなわち部分集合である。

環準同型は逆向きの写像を誘導する

\(\varphi : R \to S\) があると、\(S\) の素イデアル \(\mathfrak q\) の逆像 \(\varphi^{-1}(\mathfrak q)\) は \(R\) の素イデアルになる。だから写像 \(\operatorname{Spec} S \to \operatorname{Spec} R\) が得られる。矢印の向きが反転する。「環 = 関数の集まり、空間 = 点の集まり」と思えば、関数の引き戻しが空間の写像と逆向きなのは自然である。

/-- 環準同型 `φ : R → S` は、逆向きの写像 `Spec S → Spec R`, `𝔮 ↦ φ⁻¹(𝔮)` を誘導する。
素イデアルの逆像は素イデアル。矢印の向きが反転することに注意。 -/
def PrimeSpectrum.comap {S : Type} [CommRing S] (φ : R →ᵣ S) (Q : PrimeSpectrum S) : PrimeSpectrum R :=
  ⟨⟨fun a => φ a ∈ Q.1,
    by show φ 0 ∈ Q.1; rw [φ.map_zero]; exact Q.1.zero_mem,
    fun {a b} ha hb => by show φ (a + b) ∈ Q.1; rw [φ.map_add]; exact Q.1.add_mem ha hb,
    fun r {a} ha => by show φ (r * a) ∈ Q.1; rw [φ.map_mul]; exact Q.1.mul_mem _ ha⟩,
   ⟨fun h => Q.2.1 (by rw [← φ.map_one]; exact h),
    fun {a b} h => Q.2.2 (by rw [← φ.map_mul]; exact h)⟩⟩
end Spectrum

この定義は証明が全部埋まっている。⟨⟨…⟩, ⟨…⟩⟩ という入れ子の角括弧は、「イデアルの4フィールド」と「素であることの2条件」を順に埋めている。たとえば「\(1 \notin \varphi^{-1}(\mathfrak q)\)」は、\(\varphi(1) = 1 \in \mathfrak q\) なら \(\mathfrak q\) が素であることに矛盾する、という一行である。

位相を定義する

\(V(E)\) を閉集合とする位相がザリスキ位相である。位相そのものも Lean 本体にはないので定義する。開集合の族が「全体を含み、有限交叉で閉じ、任意和で閉じる」というだけの構造体である。

/-- 位相。「開集合」と呼ばれる部分集合の族で、全体・有限交叉・任意和で閉じるもの。
部分集合は述語 `X → Prop` で表す。 -/
structure Topology (X : Type) where
  IsOpen : (X → Prop) → Prop
  isOpen_univ : IsOpen (fun _ => True)
  isOpen_inter : ∀ {U V}, IsOpen U → IsOpen V → IsOpen (fun x => U x ∧ V x)
  isOpen_sUnion : ∀ (𝒰 : (X → Prop) → Prop), (∀ U, 𝒰 U → IsOpen U) →
    IsOpen (fun x => ∃ U, 𝒰 U ∧ U x)

/-- 位相空間 = 型 + 位相。 -/
structure TopSpace where
  carrier : Type
  top : Topology carrier

instance : CoeSort TopSpace Type := ⟨TopSpace.carrier⟩

/-- 開集合の型。 -/
def Opens (X : TopSpace) : Type := { U : X → Prop // X.top.IsOpen U }

namespace Opens
variable {X : TopSpace}

instance : LE (Opens X) := ⟨fun V U => ∀ x, V.1 x → U.1 x⟩

theorem le_refl (U : Opens X) : U ≤ U := fun _ h => h
theorem le_trans {U V W : Opens X} (h₁ : W ≤ V) (h₂ : V ≤ U) : W ≤ U :=
  fun x h => h₂ x (h₁ x h)

/-- 二つの開集合の交わり。 -/
def inter (U V : Opens X) : Opens X :=
  ⟨fun x => U.1 x ∧ V.1 x, X.top.isOpen_inter U.2 V.2⟩

theorem inter_le_left (U V : Opens X) : inter U V ≤ U := fun _ h => h.1
theorem inter_le_right (U V : Opens X) : inter U V ≤ V := fun _ h => h.2

/-- 全体集合。 -/
def univ : Opens X := ⟨fun _ => True, X.top.isOpen_univ⟩
theorem le_univ (U : Opens X) : U ≤ univ := fun _ _ => trivial
end Opens

Opens X は開集合の型である。V ≤ U で包含 \(V \subseteq U\) を表し、後の「制限写像」で頻繫に使う。Opens.inter は交わり \(U \cap V\)。ここまでは位相空間論の教科書の1ページ目をそのまま書いている。

/-- ザリスキ位相。閉集合を零点集合 `V(E)` とする。開集合は `V(E)` の補集合。 -/
def zariskiTopology (R : Type) [CommRing R] : Topology (PrimeSpectrum R) where
  IsOpen U := ∃ E : R → Prop, ∀ P, U P ↔ ¬ zeroLocus E P
  isOpen_univ := ⟨fun a => a = 1, fun P => by
    constructor
    · intro _ h; exact P.2.1 (h 1 rfl)
    · intro _; trivial⟩
  isOpen_inter := sorry   -- 演習: V(E) ∪ V(E') = V(E · E')
  isOpen_sUnion := sorry  -- 演習: ⋂ V(Eᵢ) = V(⋃ Eᵢ)

/-- 位相空間としての `Spec R`。 -/
def SpecTop (R : Type) [CommRing R] : TopSpace := ⟨PrimeSpectrum R, zariskiTopology R⟩

ザリスキ位相の定義は「\(U\) が開 \(\iff\) ある \(E\) について \(U = \operatorname{Spec} R \setminus V(E)\)」である。全体が開であることは \(E = \{1\}\) で確認できる（\(V(\{1\}) = \emptyset\)、なぜなら \(1\) はどの素イデアルにも入らない）。この証明は埋めてある。有限交叉と任意和は、\(V(E) \cup V(E') = V(EE')\) と \(\bigcap V(E_i) = V(\bigcup E_i)\) という古典的な計算で、演習として sorry のままにした。

直感を一つ。ザリスキ位相はとても粗い。\(\operatorname{Spec} \mathbb Z\) の開集合は「有限個の素数を除いた全体」か空集合だけである。この粗さが、後で「ザリスキ位相のコホモロジーでは定数層が何も見えない」という問題を引き起こし、エタール位相へ乗り換える動機になる。

/-- 連続写像。開集合の逆像が開集合。 -/
structure ContinuousMap (X Y : TopSpace) where
  toFun : X → Y
  isOpen_preimage : ∀ U : Opens Y, Y.top.IsOpen U.1 → X.top.IsOpen (fun x => U.1 (toFun x))

/-- 連続写像による開集合の逆像。 -/
def ContinuousMap.preimage {X Y : TopSpace} (f : ContinuousMap X Y) (U : Opens Y) : Opens X :=
  ⟨fun x => U.1 (f.toFun x), f.isOpen_preimage U U.2⟩

06 — LOCALIZATION

局所化: 分母を許す

局所化は、雑にいうと「ある元たちで割ることを許した環」である。\(\mathbb Z\) で \(2\) のべきで割ることを許せば \(\mathbb Z[1/2]\)、素数 \(p\) 以外のすべてで割ることを許せば \(\mathbb Z_{(p)}\)（分母が \(p\) で割れない分数）。幾何学的には、\(R[1/f]\) は「\(f\) が消えない場所 \(D(f)\) 上の関数環」、\(R_{\mathfrak p}\) は「点 \(\mathfrak p\) のごく近くだけで定義された関数の環」である。

構成は分数と同じである。乗法的部分集合 \(S\)（\(1\) を含み積で閉じる）を取り、組 \((a, s)\)、\(s \in S\) を「\(a/s\)」と読む。二つの分数が等しいことを

\[ \frac{a}{s} = \frac{b}{t} \iff \exists u \in S,\ u(at - bs) = 0 \]

で定める（\(u\) が要るのは零因子があるときのため）。局所化 \(S^{-1}R\) はこの同値関係による商である。

section Localization
variable {R : Type} [CommRing R]

/-- 乗法的部分集合。1 を含み、掛け算で閉じる。 -/
structure Submonoid (R : Type) [CommRing R] where
  carrier : R → Prop
  one_mem : carrier 1
  mul_mem : ∀ {a b}, carrier a → carrier b → carrier (a * b)

/-- 「分数」`a / s` の表示。分子 `a : R` と、分母 `s ∈ S`。 -/
structure Fraction (S : Submonoid R) where
  num : R
  den : R
  den_mem : S.carrier den

/-- 二つの分数が等しい: `a/s = b/t ⇔ ∃ u ∈ S, u (a t - b s) = 0`。 -/
def Fraction.rel {S : Submonoid R} (x y : Fraction S) : Prop :=
  ∃ u, S.carrier u ∧ u * (x.num * y.den + -(y.num * x.den)) = 0

/-- 局所化 `S⁻¹R`。分数の表示を、上の同値関係で割った商。 -/
def Localization (S : Submonoid R) : Type := Quot (Fraction.rel (S := S))

/-- 分数 `a / s` を局所化の元として見る。 -/
def Localization.mk {S : Submonoid R} (a s : R) (hs : S.carrier s) : Localization S :=
  Quot.mk _ ⟨a, s, hs⟩

ここで前章の Quot が初めて登場する。Fraction S は分数の「表示」（分子、分母、分母が \(S\) に入る証明）、Fraction.rel が同値関係、Localization S := Quot rel がその商である。Localization.mk a s hs が \(a/s\) を表す。

/-- 分数の足し算 `a/s + b/t = (at + bs)/(st)`。代表元の取り方によらないこと（`sorry`）は演習。 -/
def Localization.add {S : Submonoid R} : Localization S → Localization S → Localization S :=
  Quot.lift (fun x => Quot.lift
    (fun y => Localization.mk (x.num * y.den + y.num * x.den) (x.den * y.den) (S.mul_mem x.den_mem y.den_mem))
    sorry) sorry

/-- 分数の掛け算 `(a/s)(b/t) = ab/st`。 -/
def Localization.mul {S : Submonoid R} : Localization S → Localization S → Localization S :=
  Quot.lift (fun x => Quot.lift
    (fun y => Localization.mk (x.num * y.num) (x.den * y.den) (S.mul_mem x.den_mem y.den_mem))
    sorry) sorry

/-- `S⁻¹R` は可換環。公理の検証（`sorry`）は分数計算の演習。 -/
instance (S : Submonoid R) : CommRing (Localization S) where
  add := Localization.add
  mul := Localization.mul
  neg := Quot.lift (fun x => Localization.mk (-x.num) x.den x.den_mem) sorry
  zero := Localization.mk 0 1 S.one_mem
  one  := Localization.mk 1 1 S.one_mem
  add_assoc := sorry
  add_comm := sorry
  zero_add := sorry
  neg_add_cancel := sorry
  mul_assoc := sorry
  mul_comm := sorry
  one_mul := sorry
  mul_add := sorry

足し算は \(\frac{a}{s} + \frac{b}{t} = \frac{at + bs}{st}\)。Quot.lift を二重に使っているのは「二変数の写像を商から定義する」ためで、二つの sorry は「代表元の取り方によらない」ことの証明である。数学の教科書が「well-defined であることは容易に確かめられる」と一行で済ませる箇所が、Leanでは明示的な証明義務として現れる。ここでは 演習として残した。環の公理も同様である。

/-- 素イデアルの補集合 `R ∖ 𝔭` は乗法的部分集合。 -/
def Ideal.primeCompl (P : Ideal R) (hP : P.IsPrime) : Submonoid R where
  carrier a := a ∉ P
  one_mem := hP.1
  mul_mem {a b} ha hb hab := by
    rcases hP.2 hab with h | h
    · exact ha h
    · exact hb h

/-- 素イデアル `𝔭` における局所化 `R_𝔭`。 -/
def localizationAt (P : PrimeSpectrum R) : Type := Localization (P.1.primeCompl P.2)

instance (P : PrimeSpectrum R) : CommRing (localizationAt P) :=
  inferInstanceAs (CommRing (Localization (P.1.primeCompl P.2)))

/-- べき `fⁿ`。 -/
def npow (f : R) : Nat → R
  | 0 => 1
  | n + 1 => npow f n * f

/-- `f` のべきからなる乗法的部分集合 `{1, f, f², …}`。 -/
def Submonoid.powers (f : R) : Submonoid R where
  carrier a := ∃ n : Nat, a = npow f n
  one_mem := ⟨0, rfl⟩
  mul_mem := sorry  -- 演習: fⁿ · fᵐ = fⁿ⁺ᵐ

/-- 標準的な写像 `R → S⁻¹R`, `a ↦ a / 1`。 -/
def Localization.algebraMap (S : Submonoid R) : R →ᵣ Localization S :=
  ⟨fun a => Localization.mk a 1 S.one_mem, sorry, sorry, rfl⟩

/-- `R[1/f]`。 -/
def Away (f : R) : Type := Localization (Submonoid.powers f)

end Localization

二つの重要な例を定義している。localizationAt P は素イデアル \(\mathfrak p\) での局所化 \(R_{\mathfrak p} = (R \setminus \mathfrak p)^{-1} R\)。\(R \setminus \mathfrak p\) が乗法的であることは、まさに素イデアルの定義そのものである（Ideal.primeCompl の証明を見ると、素イデアルの条件を対偶で使っているだけだとわかる）。Away f は \(R[1/f] = \{1, f, f^2, \dots\}^{-1}R\)。

\(R_{\mathfrak p}\) は局所環である。極大イデアルは \(\mathfrak p R_{\mathfrak p}\)、つまり「分子が \(\mathfrak p\) に入る分数」で、それ以外の分数は分母分子を逆にすれば可逆になる。この局所環 \(R_{\mathfrak p}\) が、次章で構造層の茎になる。

07 — PRESHEAVES AND SHEAVES

前層と層: 「局所的なデータを貼り合わせる」の定式化

層は、雑にいうと「各開集合ごとに何かの集まり（関数、切断、解）があって、小さい開集合に制限でき、局所的に与えたものが一意に貼り合う」という状況の公理化である。連続関数、正則関数、ベクトル場、微分方程式の解。すべて層をなす。

まず前層。位相空間 \(X\) の開集合 \(U\) ごとに集合 \(\mathcal F(U)\) があり、\(V \subseteq U\) ごとに制限写像 \(\rho_{UV} : \mathcal F(U) \to \mathcal F(V)\) があって、

\[ \rho_{UU} = \mathrm{id},\qquad \rho_{VW}\circ\rho_{UV} = \rho_{UW}\quad (W \subseteq V \subseteq U). \]

圏論の言葉では、開集合の順序集合を圏と見た反変関手 \(\mathrm{Open}(X)^{\mathrm{op}} \to \mathbf{Set}\) である。

/-- 位相空間 `X` 上の（集合値の）前層。開集合ごとに「切断の集合」`obj U` を対応させ、
`V ⊆ U` に対して制限写像 `res : obj U → obj V` を与える。恒等と合成を保つ。 -/
structure Presheaf (X : TopSpace) where
  obj : Opens X → Type
  res : ∀ {U V : Opens X}, V ≤ U → obj U → obj V
  res_id : ∀ (U : Opens X) (s : obj U), res (Opens.le_refl U) s = s
  res_comp : ∀ {U V W : Opens X} (h₁ : V ≤ U) (h₂ : W ≤ V) (s : obj U),
    res h₂ (res h₁ s) = res (Opens.le_trans h₂ h₁) s

obj U が \(\mathcal F(U)\)、res h が \(\rho_{UV}\)（h : V ≤ U は包含の証明）。res_id、res_comp が二つの関手性の公理である。制限写像の引数に「包含の証明」を渡すのが Lean らしいところで、これによって「\(V \subseteq U\) でないのに制限する」という書き間違いが型エラーになる。

層の条件

前層が層であるとは、開被覆 \(U = \bigcup_i V_i\) に対して次の二つが成り立つことである。

1. 局所性（分離性）

   \(s, t \in \mathcal F(U)\) がすべての \(V_i\) 上で一致すれば \(s = t\)。「関数は局所的に決まる」。

2. 貼り合わせ

   \(s_i \in \mathcal F(V_i)\) が交わり \(V_i \cap V_j\) 上で一致していれば、\(s|_{V_i} = s_i\) となる \(s \in \mathcal F(U)\) がある。「局所的に整合するデータは大域的なデータから来る」。

一つの式で書けば、次の図式が等化子（equalizer）であること。

\[ \mathcal F(U) \longrightarrow \prod_i \mathcal F(V_i) \rightrightarrows \prod_{i,j} \mathcal F(V_i \cap V_j). \]

/-- 開被覆。`U` を覆う開集合の族 `V i ⊆ U`。 -/
structure OpenCover {X : TopSpace} (U : Opens X) where
  ι : Type
  V : ι → Opens X
  le : ∀ i, V i ≤ U
  covers : ∀ x, U.1 x → ∃ i, (V i).1 x

/-- 層。前層であって、「局所性」と「貼り合わせ」を満たすもの。 -/
structure Sheaf (X : TopSpace) extends Presheaf X where
  /-- 局所性: 各 `V i` への制限が一致する二つの切断は等しい。 -/
  locality : ∀ (U : Opens X) (𝒱 : OpenCover U) (s t : obj U),
    (∀ i, res (𝒱.le i) s = res (𝒱.le i) t) → s = t
  /-- 貼り合わせ: 交わりの上で一致する切断の族は、`U` 上の一つの切断から来る。 -/
  gluing : ∀ (U : Opens X) (𝒱 : OpenCover U) (s : ∀ i, obj (𝒱.V i)),
    (∀ i j, res (Opens.inter_le_left (𝒱.V i) (𝒱.V j)) (s i)
          = res (Opens.inter_le_right (𝒱.V i) (𝒱.V j)) (s j)) →
    ∃ t : obj U, ∀ i, res (𝒱.le i) t = s i

OpenCover U は被覆の型で、添字型 ι、開集合の族 V、各 V i ⊆ U の証明、被覆していることの証明からなる。locality と gluing が二条件で、gluing の仮定にある res (inter_le_left …) (s i) = res (inter_le_right …) (s j) が「\(V_i \cap V_j\) 上で一致」である。Opens.inter_le_left は \(V_i \cap V_j \subseteq V_i\) の証明で、制限写像に渡している。

この定義は、集合値の層である。「環の層」「アーベル群の層」は、この上に「各 \(\mathcal F(U)\) が環で、制限が環準同型」という条件を重ねる。それは二章先で行う。

08 — STALKS

茎: 一点の近くだけを見る

点 \(x\) における層の茎 \(\mathcal F_x\) は、雑にいうと「\(x\) のどんなに小さい近傍でもよいから、そこで定義された切断」の集まりである。二つの切断は、\(x\) の十分小さい近傍で一致すれば同じとみなす。関数でいえば、\(x\) におけるテイラー展開の全情報のようなものである。

\[ \mathcal F_x := \varinjlim_{U \ni x} \mathcal F(U) = \Bigl\{ (U, s) \mid x \in U,\ s \in \mathcal F(U) \Bigr\} \Big/ \bigl((U,s)\sim(V,t) \iff \exists W \ni x,\ s|_W = t|_W\bigr). \]

section Stalk
variable {X : TopSpace} (F : Presheaf X) (x : X)

/-- 点 `x` の近傍で定義された切断 `(U, s)`。 -/
structure Germ where
  U : Opens X
  mem : U.1 x
  s : F.obj U

/-- 二つの切断が `x` の近くで一致する。 -/
def Germ.equiv (a b : Germ F x) : Prop :=
  ∃ (W : Opens X) (_ : W.1 x) (h₁ : W ≤ a.U) (h₂ : W ≤ b.U), F.res h₁ a.s = F.res h₂ b.s

/-- 茎 `F_x = colim_{U ∋ x} F(U)`。切断の芽（germ）全体。 -/
def Stalk : Type := Quot (Germ.equiv F x)

/-- 切断 `s ∈ F(U)` の `x` における芽。 -/
def Presheaf.germ {U : Opens X} (hx : U.1 x) (s : F.obj U) : Stalk F x :=
  Quot.mk _ ⟨U, hx, s⟩
end Stalk

Germ F x は「\(x\) を含む開集合 \(U\) と \(U\) 上の切断 \(s\)」の組、Germ.equiv が「\(x\) の近くで一致する」という関係、Stalk F x がその Quot。F.germ hx s は切断 \(s\) の \(x\) における芽 \(s_x\) である。局所化のときと同じパターンで、「有向極限（順極限）」を、Lean 本体だけで Quot を使って構成している。

なぜ茎が要るのか。次章で「局所環付き空間」を定義するときに、構造層の茎が局所環であるという条件を課すからである。\(\operatorname{Spec} R\) の場合、点 \(\mathfrak p\) における茎は \(R_{\mathfrak p}\) になり、前章で見たようにこれは局所環である。

09 — STRUCTURE SHEAF

環の層と、Spec R の構造層

ここまでで「空間 \(\operatorname{Spec} R\)」と「層」が別々に定義された。次に \(\operatorname{Spec} R\) の上に環の層 \(\mathcal O\) を載せる。これが「\(\operatorname{Spec} R\) 上の関数の環」の役割を果たし、環 \(R\) を完全に復元できる（\(\mathcal O(\operatorname{Spec} R) = R\)）。

まず、環の層の定義。各 \(\mathcal O(U)\) が可換環で、制限写像がすべて環準同型であればよい。

/-- 環の層。各 `obj U` が可換環で、制限写像が環準同型。 -/
structure SheafOfRings (X : TopSpace) extends Sheaf X where
  ring : ∀ U, CommRing (obj U)
  res_add : ∀ {U V : Opens X} (h : V ≤ U) (s t : obj U), res h (s + t) = res h s + res h t
  res_mul : ∀ {U V : Opens X} (h : V ≤ U) (s t : obj U), res h (s * t) = res h s * res h t
  res_one : ∀ {U V : Opens X} (h : V ≤ U), res h (1 : obj U) = 1

attribute [instance] SheafOfRings.ring

/-- 制限写像を環準同型として取り出す。 -/
def SheafOfRings.resHom {X : TopSpace} (𝒪 : SheafOfRings X) {U V : Opens X} (h : V ≤ U) :
    𝒪.obj U →ᵣ 𝒪.obj V :=
  ⟨𝒪.res h, 𝒪.res_add h, 𝒪.res_mul h, 𝒪.res_one h⟩

/-- 環の層の茎は環になる（演習）。 -/
noncomputable instance {X : TopSpace} (𝒪 : SheafOfRings X) (x : X) :
    CommRing (Stalk 𝒪.toPresheaf x) := sorry

ring : ∀ U, CommRing (obj U) が「各 \(\mathcal O(U)\) は環」、res_add 以下が「制限は準同型」である。attribute [instance] は、以後 obj U の元に + や * を自動で使えるようにする宣言である。茎が環になることは 演習とした（芽の代表元を共通の近傍に制限して演算する）。

構造層 \(\mathcal O_{\operatorname{Spec} R}\)

\(\operatorname{Spec} R\) の開集合 \(U\) 上の「関数」とは何か。答えはこうである。各点 \(\mathfrak p \in U\) に \(R_{\mathfrak p}\) の元 \(s(\mathfrak p)\) を割り当てる写像で、局所的には一つの分数 \(a/f\) で書けるもの。

\[ \mathcal O(U) := \Bigl\{\, s : \prod_{\mathfrak p \in U} R_{\mathfrak p} \ \Bigm|\ \forall \mathfrak p \in U,\ \exists V \ni \mathfrak p,\ \exists a, f \in R,\ \forall \mathfrak q \in V:\ f \notin \mathfrak q,\ s(\mathfrak q) = a/f \in R_{\mathfrak q} \Bigr\}. \]

これは複素解析で「正則関数とは、局所的に収束べき級数で書ける関数」と定義するのと同じ形をしている。「局所的に \(a/f\) で書ける」が「局所的にべき級数で書ける」に当たる。

section StructureSheaf
variable (R : Type) [CommRing R]

/-- 開集合 `U ⊆ Spec R` 上の「関数」: 各点 `𝔭 ∈ U` に `R_𝔭` の元を割り当てる写像であって、
局所的には一つの分数 `a / f` で書けるもの。 -/
def IsLocallyFraction (U : Opens (SpecTop R))
    (s : ∀ P : PrimeSpectrum R, U.1 P → localizationAt P) : Prop :=
  ∀ (P : PrimeSpectrum R) (_ : U.1 P),
    ∃ (V : Opens (SpecTop R)) (_ : V.1 P) (hVU : V ≤ U) (a f : R),
      ∀ (Q : PrimeSpectrum R) (hQ : V.1 Q),
        ∃ hf : f ∉ Q.1, s Q (hVU Q hQ) = Localization.mk a f hf

/-- `Spec R` の構造層 `𝒪_{Spec R}`。`𝒪(U)` は `U` 上の局所的に分数で書ける関数の環。 -/
noncomputable def specSheaf : SheafOfRings (SpecTop R) where
  obj U := { s : ∀ P : PrimeSpectrum R, U.1 P → localizationAt P // IsLocallyFraction R U s }
  res h s := ⟨fun P hP => s.1 P (h P hP), sorry⟩
  res_id := sorry
  res_comp := sorry
  locality := sorry
  gluing := sorry
  ring := sorry     -- 各点ごとの足し算・掛け算
  res_add := sorry
  res_mul := sorry
  res_one := sorry
end StructureSheaf

IsLocallyFraction U s が上の条件を一字一句そのまま書いたものである。Lean の ∀ (P) (_ : U.1 P), ∃ (V) (_ : V.1 P) (hVU : V ≤ U) (a f : R), ∀ (Q) (hQ : V.1 Q), ∃ hf : f ∉ Q.1, s Q … = Localization.mk a f hf を、数式の量化子と一つずつ対応させてほしい。最後の Localization.mk a f hf は \(R_{\mathfrak q}\) の元 \(a/f\) で、hf は「\(f \notin \mathfrak q\) なので分母として許される」証明である。

specSheaf の各フィールドは sorry が多い。制限写像そのものは定義してある（\(s\) を小さい開集合に絞るだけ）。層であること、各 \(\mathcal O(U)\) が環であること（点ごとの演算）は 演習である。重要なのは、この定義が型検査を通ること、つまり「局所的に分数で書ける関数」という概念が、それまでに定義した素スペクトル・ザリスキ位相・局所化だけで書けている、という事実である。

そして、この層について次が成り立つ（Hartshorne II.2.2）。これらは本物の定理であり、このノートでは述べるだけにする。

\[ \mathcal O_{\mathfrak p} \cong R_{\mathfrak p},\qquad \mathcal O(D(f)) \cong R[1/f],\qquad \mathcal O(\operatorname{Spec} R) \cong R. \]

10 — LOCALLY RINGED SPACES

局所環付き空間と、その射

\(\operatorname{Spec} R\) は「位相空間 + 環の層」という組になった。この組の一般形が環付き空間で、さらに「各茎が局所環」という条件を付けたのが局所環付き空間である。

なぜ茎が局所環である必要があるのか。局所環 \(\mathcal O_x\) の唯一の極大イデアル \(\mathfrak m_x\) が「\(x\) で消える関数」の役割を果たし、\(\mathcal O_x / \mathfrak m_x\) が「\(x\) における値の体」になる。この構造があるからこそ、「関数を点で評価する」という操作が、点集合を一切使わずに定義できる。

/-- 環付き空間: 位相空間と、その上の環の層。 -/
structure RingedSpace where
  X : TopSpace
  𝒪 : SheafOfRings X

/-- 局所環付き空間: すべての茎 `𝒪_x` が局所環である環付き空間。 -/
structure LocallyRingedSpace extends RingedSpace where
  isLocal : ∀ x : X, IsLocalRing (Stalk 𝒪.toPresheaf x)

/-- アフィンスキーム `Spec R`（局所環付き空間として）。茎 `𝒪_𝔭 ≅ R_𝔭` が局所環であることは演習。 -/
noncomputable def Spec (R : Type) [CommRing R] : LocallyRingedSpace where
  X := SpecTop R
  𝒪 := specSheaf R
  isLocal := sorry

Spec R が局所環付き空間になることは、茎 \(\mathcal O_{\mathfrak p} \cong R_{\mathfrak p}\) が局所環であることに帰着し、演習とした。

射

局所環付き空間の射 \((f, f^\sharp) : X \to Y\) は、連続写像 \(f : X \to Y\) と、各開集合 \(V \subseteq Y\) ごとの環準同型

\[ f^\sharp_V : \mathcal O_Y(V) \longrightarrow \mathcal O_X(f^{-1}V) \]

の組で、制限と両立し、さらに各点 \(x\) で誘導される茎の準同型 \(f^\sharp_x : \mathcal O_{Y, f(x)} \to \mathcal O_{X, x}\) が局所準同型であるものである。

直感はこうである。\(f^\sharp\) は「\(Y\) 上の関数を \(f\) で引き戻す」操作 \(g \mapsto g \circ f\) である。局所準同型の条件は、「\(g\) が \(f(x)\) で消えるなら、\(g \circ f\) は \(x\) で消える」、つまり関数の引き戻しが、点の値を正しく引き戻すことを保証する。この条件を落とすと、\(\operatorname{Spec}\) の射と環準同型の対応（\(\operatorname{Hom}(\operatorname{Spec} S, \operatorname{Spec} R) \cong \operatorname{Hom}(R, S)\)）が壊れる。

/-- 局所環付き空間の射 `(f, f♯) : X → Y`。
連続写像 `f` と、各開集合 `V ⊆ Y` ごとの環準同型 `f♯_V : 𝒪_Y(V) → 𝒪_X(f⁻¹V)`。
制限と両立し、茎に誘導される準同型 `𝒪_{Y,f(x)} → 𝒪_{X,x}` が局所準同型。 -/
structure LRSHom (X Y : LocallyRingedSpace) where
  base : ContinuousMap X.X Y.X
  sharp : ∀ V : Opens Y.X, Y.𝒪.obj V →ᵣ X.𝒪.obj (base.preimage V)
  sharp_res : ∀ {V W : Opens Y.X} (h : W ≤ V) (s : Y.𝒪.obj V),
    X.𝒪.res (fun _ hx => h _ hx) (sharp V s) = sharp W (Y.𝒪.res h s)
  stalk_local : ∀ (x : X.X) (V : Opens Y.X) (hx : V.1 (base.toFun x)) (s : Y.𝒪.obj V),
    IsUnit (X.𝒪.germ x hx (sharp V s)) → IsUnit (Y.𝒪.germ (base.toFun x) hx s)

infixr:10 " ⟶ " => LRSHom

/-- 恒等射。 -/
def LRSHom.id (X : LocallyRingedSpace) : X ⟶ X where
  base := ⟨fun x => x, fun U hU => hU⟩
  sharp V := RingHom.id _
  sharp_res := sorry
  stalk_local := sorry

/-- 合成。 -/
def LRSHom.comp {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : X ⟶ Z where
  base := ⟨fun x => g.base.toFun (f.base.toFun x), sorry⟩
  sharp W := RingHom.comp (f.sharp (g.base.preimage W)) (g.sharp W)
  sharp_res := sorry
  stalk_local := sorry

/-- 同型。互いに逆な射の組。 -/
structure LRSIso (X Y : LocallyRingedSpace) where
  hom : X ⟶ Y
  inv : Y ⟶ X
  hom_inv : LRSHom.comp hom inv = LRSHom.id X
  inv_hom : LRSHom.comp inv hom = LRSHom.id Y

stalk_local の書き方に注意。茎の写像を構成する代わりに、「\(V\) 上の切断 \(s\) について、\(f^\sharp(s)\) の \(x\) での芽が可逆なら \(s\) の \(f(x)\) での芽も可逆」と述べている。これは茎の局所準同型性を、芽のレベルで書き下したものである。茎の写像を Quot.lift で作る手間を避けつつ、数学的には同じ内容になっている。

LRSIso は同型で、互いに逆な射の組である。次章のスキームの定義で「\(\operatorname{Spec} R\) と同型」を言うために使う。

開集合への制限

「\(X\) の開集合 \(U\) は、それ自身が局所環付き空間である」。層を \(U\) の開集合だけに絞ればよい。これも定義しておく。

section Restrict
variable (X : LocallyRingedSpace) (U : Opens X.X)

/-- 開集合 `U` を部分空間として位相空間にする。 -/
def Opens.toTopSpace : TopSpace where
  carrier := { x : X.X // U.1 x }
  top :=
    { IsOpen := fun V => ∃ W : Opens X.X, ∀ x, V x ↔ W.1 x.1
      isOpen_univ := ⟨Opens.univ, fun _ => ⟨fun _ => trivial, fun _ => trivial⟩⟩
      isOpen_inter := sorry
      isOpen_sUnion := sorry }

/-- 部分空間 `U` の開集合を `X` の開集合として見る（`U` が開なので開になる）。 -/
def Opens.ofSub (V : Opens (Opens.toTopSpace X U)) : Opens X.X :=
  ⟨fun x => ∃ h : U.1 x, V.1 ⟨x, h⟩, sorry⟩

/-- 局所環付き空間を開集合 `U` に制限したもの `(U, 𝒪_X|_U)`。 -/
noncomputable def LocallyRingedSpace.restrict : LocallyRingedSpace where
  X := Opens.toTopSpace X U
  𝒪 := { obj := fun V => X.𝒪.obj (Opens.ofSub X U V),
          res := fun h s => X.𝒪.res (sorry) s,
          res_id := sorry, res_comp := sorry, locality := sorry, gluing := sorry,
          ring := fun _ => X.𝒪.ring _,
          res_add := sorry, res_mul := sorry, res_one := sorry }
  isLocal := sorry
end Restrict

部分空間の位相、部分空間の開集合を \(X\) の開集合と見なす操作、層の制限、の三段構えである。証明はほとんど sorry だが、データの流れ（\(U\) の開集合 \(V\) に対して \(\mathcal O_X|_U(V) := \mathcal O_X(V)\)、ただし \(V\) を \(X\) の開集合として読む）は書いてある。

11 — SCHEMES

スキーム: 局所的に Spec であるもの

ようやくスキームである。定義は一行で言える。スキームとは、局所環付き空間であって、各点が、あるアフィンスキーム \(\operatorname{Spec} R\) と同型な開近傍を持つもの。多様体が「局所的に \(\mathbb R^n\)」であるのと同じ形の定義である。

\[ \forall x \in X,\ \exists U \ni x \text{ 開},\ \exists R,\quad (U, \mathcal O_X|_U) \cong \operatorname{Spec} R. \]

/-- スキーム。局所環付き空間であって、各点が、あるアフィンスキーム `Spec R` と同型な
開近傍を持つもの。 -/
structure Scheme extends LocallyRingedSpace where
  local_affine : ∀ x : X, ∃ (U : Opens X) (_ : U.1 x) (R : Type) (_ : CommRing R),
    Nonempty (LRSIso (toLocallyRingedSpace.restrict U) (Spec R))

/-- スキームの射は局所環付き空間の射。 -/
def Scheme.Hom (X Y : Scheme) : Type := X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace

/-- アフィン開集合: `U` の上への制限が、ある `Spec R` と同型。 -/
def Scheme.IsAffineOpen (X : Scheme) (U : Opens X.X) : Prop :=
  ∃ (R : Type) (_ : CommRing R), Nonempty (LRSIso (X.toLocallyRingedSpace.restrict U) (Spec R))

/-- `f : X → Y`、`U ⊆ Y`、`V ⊆ f⁻¹U` に対する環準同型 `𝒪_Y(U) → 𝒪_X(f⁻¹U) → 𝒪_X(V)`。 -/
def Scheme.Hom.appLE {X Y : Scheme} (f : Scheme.Hom X Y) (U : Opens Y.X) (V : Opens X.X)
    (h : V ≤ f.base.preimage U) : Y.𝒪.obj U →ᵣ X.𝒪.obj V :=
  RingHom.comp (X.𝒪.resHom h) (f.sharp U)

local_affine がその一行である。∃ (U) (_ : U.1 x) (R) (_ : CommRing R), Nonempty (LRSIso (restrict U) (Spec R))——「\(x\) を含む開集合 \(U\)、環 \(R\)、そして \(U\) への制限と \(\operatorname{Spec} R\) の同型が存在する」。Nonempty は「同型が少なくとも一つある」という命題で、特定の同型を選ばないために使っている。

ここで振り返ると、スキームの定義に必要なものが全部、前の章で自分の手で定義されていることがわかる。可換環（02）、素イデアル（04）、\(\operatorname{Spec}\) と位相（05）、局所化（06）、層（07）、茎（08）、構造層（09）、局所環付き空間と射と制限（10）。どれか一つが抜けていれば、この structure Scheme は型検査を通らない。

スキームの射と、アフィン開集合

スキームの射は、局所環付き空間の射そのものである（追加の条件はない）。後でエタール射を定義するために、二つの道具を用意しておく。「開集合 \(U\) がアフィン」とは \(U\) への制限が何かの \(\operatorname{Spec} R\) と同型であること。そして \(f : X \to Y\)、\(U \subseteq Y\)、\(V \subseteq f^{-1}U\) に対する環準同型

\[ f^\sharp_{U,V} : \mathcal O_Y(U) \xrightarrow{\ f^\sharp_U\ } \mathcal O_X(f^{-1}U) \xrightarrow{\ \text{制限}\ } \mathcal O_X(V). \]

これは Scheme.Hom.appLE として、\(f^\sharp_U\) と制限写像の合成で定義してある。エタール射とは、\(U, V\) がアフィンのとき、この環準同型 \(f^\sharp_{U,V}\) がつねにエタールであるような射、と定義することになる。つまり幾何の条件を、環準同型の条件に帰着させる。そのために、次はいったん幾何を離れて、圏とサイトの一般論を書く。

12 — GROTHENDIECK TOPOLOGIES

圏、篩、グロタンディーク位相

ここで一度立ち止まって、なぜ位相を差し替えるのかを言っておく。前章までで、スキームとその上の層は定義できた。ザリスキ位相で層コホモロジーを取ることもできる。しかしそれは、定数層 \(\mathbb Z/n\) に対してほとんど何も見えない。理由は、ザリスキ位相の開集合が大きすぎて（既約なスキームでは任意の二つの空でない開集合が交わる）、定数層の高次コホモロジーが消えてしまうからである。複素多様体の特異コホモロジー \(H^i(X(\mathbb C), \mathbb Z/n)\) に対応するものを代数的に作りたいのに、ザリスキ位相ではそれができない。

グロタンディークの答えは、「開集合 \(U \subseteq X\)」の代わりに「エタール射 \(U \to X\)」を使うことだった。エタール射は「局所同相の代数版」で、開埋め込みだけでなく、たとえば \(\mathbb C^\times \to \mathbb C^\times,\ z \mapsto z^n\) のような被覆写像も含む。被覆写像を「開被覆」の仲間に入れてやると、定数層が非自明なコホモロジーを持つようになる。

ただしそのためには、「開集合の族」を「対象への射の族」に一般化し、「被覆」の公理を書き直さなければならない。これがグロタンディーク位相である。以下、圏・篩・被覆の三段で定義する。

圏

圏は、対象の型、各対象の組ごとの射の型、恒等射、合成、そして単位律と結合律である。

universe u

/-- （小さいとは限らない）圏。対象の型、射の型、恒等射、合成、公理。 -/
structure Category where
  Obj : Type u
  Hom : Obj → Obj → Type
  id : ∀ X, Hom X X
  comp : ∀ {X Y Z}, Hom X Y → Hom Y Z → Hom X Z
  id_comp : ∀ {X Y} (f : Hom X Y), comp (id X) f = f
  comp_id : ∀ {X Y} (f : Hom X Y), comp f (id Y) = f
  assoc : ∀ {W X Y Z} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

Obj : Type u と宇宙変数 u が付いているのは、後でエタールサイトの対象（スキーム）が Type 1 に住むためである。合成 comp f g は図式順（\(f\) の次に \(g\)、数学の \(g \circ f\)）で書いている。

篩（ふるい）

「開集合 \(U\) の部分開集合の族で、さらに小さい開集合を取っても閉じているもの」を圏の言葉に翻訳したのが篩である。対象 \(U\) 上の篩 \(S\) とは、\(U\) に向かう射の集まりであって、前から何を合成しても閉じているもの。

\[ (f : V \to U) \in S,\ (g : W \to V) \ \Longrightarrow\ f \circ g \in S. \]

section Sieves
variable {C : Category.{u}}

/-- 対象 `U` 上の篩（ふるい）。`U` に向かう射の集まりで、前から射を合成しても閉じているもの。
「開集合 U の部分開集合の族で、さらに小さい開集合を取っても閉じているもの」の一般化。 -/
structure Sieve (U : C.Obj) where
  arrows : ∀ {V : C.Obj}, C.Hom V U → Prop
  downward_closed : ∀ {V W : C.Obj} {f : C.Hom V U}, arrows f → ∀ (g : C.Hom W V), arrows (C.comp g f)

/-- 篩の引き戻し `f⁎S = { g | g ≫ f ∈ S }`。「開集合の族を f⁻¹ で引き戻す」に対応。 -/
def Sieve.pullback {U V : C.Obj} (S : Sieve U) (f : C.Hom V U) : Sieve V where
  arrows g := S.arrows (C.comp g f)
  downward_closed {_ _ g} hg h := by
    show S.arrows (C.comp (C.comp h g) f)
    rw [C.assoc]; exact S.downward_closed hg h

/-- 最大の篩: すべての射。 -/
def Sieve.top (U : C.Obj) : Sieve U := ⟨fun _ => True, fun _ _ => trivial⟩

Sieve.pullback S f は篩の引き戻し \(f^*S = \{g \mid f \circ g \in S\}\) で、「開集合の族を \(f^{-1}\) で引き戻す」に対応する。Sieve.top U はすべての射からなる最大の篩で、「\(U\) 自身一つで \(U\) を覆う」に対応する。

グロタンディーク位相

グロタンディーク位相とは、各対象 \(U\) に対して「被覆篩」と呼ぶ篩の集まり \(J(U)\) を指定したもので、次の三公理を満たす。

1. (T1) 最大篩は被覆

   \(U\) 自身で \(U\) は覆える。

2. (T2) 引き戻しで安定

   \(S \in J(U)\)、\(f : V \to U\) なら \(f^*S \in J(V)\)。「\(U\) の被覆を \(V\) に引き戻せば \(V\) の被覆」。

3. (T3) 局所性（推移性）

   \(S \in J(U)\) で、\(S\) の各 \(f : V \to U\) について \(f^*T \in J(V)\) なら \(T \in J(U)\)。「被覆の各ピースの上で被覆なら、全体でも被覆」。

/-- グロタンディーク位相。各対象 `U` に「被覆篩」の集まり `covering U` を指定したもので、
(T1) 最大篩は被覆、(T2) 被覆篩の引き戻しは被覆、(T3) 局所的に被覆なら被覆、を満たす。 -/
structure GrothendieckTopology (C : Category.{u}) where
  covering : ∀ (U : C.Obj), Sieve U → Prop
  top_mem : ∀ U, covering U (Sieve.top U)
  pullback_stable : ∀ {U V : C.Obj} (S : Sieve U) (f : C.Hom V U), covering U S → covering V (S.pullback f)
  transitive : ∀ {U : C.Obj} (S : Sieve U) (T : Sieve U), covering U S →
    (∀ {V : C.Obj} (f : C.Hom V U), S.arrows f → covering V (T.pullback f)) → covering U T
end Sieves

位相空間の開被覆の公理（05章の Topology）と見比べてほしい。「全体は開」「交叉で閉じる」「和で閉じる」が、それぞれ (T1)(T2)(T3) に化けている。しかし決定的な違いは、もはや「点」も「部分集合」も出てこないことである。すべてが射で書かれている。だからこそ、開埋め込みでない射（エタール射）を「被覆」に含めることができる。

13 — SHEAVES ON A SITE

サイト上の層

圏とグロタンディーク位相の組をサイトと呼ぶ。サイト上の層を定義するには、07章の層の条件を篩の言葉に書き直せばよい。

/-- サイト = 圏 + グロタンディーク位相。 -/
structure Site where
  C : Category.{u}
  J : GrothendieckTopology C

section SiteSheaf
variable {C : Category.{u}}

/-- 圏 `C` 上の（集合値の）前層。反変関手 `Cᵒᵖ → Set`。 -/
structure CPresheaf (C : Category.{u}) where
  obj : C.Obj → Type
  map : ∀ {U V : C.Obj}, C.Hom V U → obj U → obj V
  map_id : ∀ (U : C.Obj) (s : obj U), map (C.id U) s = s
  map_comp : ∀ {U V W : C.Obj} (f : C.Hom V U) (g : C.Hom W V) (s : obj U),
    map g (map f s) = map (C.comp g f) s

圏上の前層は、単に反変関手 \(C^{\mathrm{op}} \to \mathbf{Set}\) である。07章の Presheaf と比べると、res (h : V ≤ U) が map (f : Hom V U) に置き換わっただけである。「包含の証明」が「射」になった。

層条件を篩で書く

07章の層の条件は「被覆 \(\{V_i \to U\}\) の上の整合的な切断の族は、ただ一つの切断に貼り合う」だった。篩 \(S\) について同じことを言う。

\[ \text{切断の族: } x = (x_f)_{f \in S},\ x_f \in \mathcal F(V) \text{ for } f : V \to U. \]

\[ \text{両立: } \forall (f : V \to U) \in S,\ \forall (g : W \to V),\quad g^* x_f = x_{f \circ g}. \]

\[ \text{貼り合わせ } t \in \mathcal F(U):\quad \forall f \in S,\ f^* t = x_f. \]

層であるとは、すべての被覆篩 \(S \in J(U)\) について、両立する族がただ一つの貼り合わせを持つことである。

/-- 篩 `S` に沿った「切断の族」: `S` に属する各射 `f : V → U` に切断 `x f ∈ F(V)` を割り当てたもの。 -/
def FamilyOfElements (F : CPresheaf C) {U : C.Obj} (S : Sieve U) : Type u :=
  ∀ {V : C.Obj} (f : C.Hom V U), S.arrows f → F.obj V

/-- 両立する族: 射をさらに合成しても割り当てが整合する（開集合の言葉では「交わりの上で一致」）。 -/
def FamilyOfElements.Compatible {F : CPresheaf C} {U : C.Obj} {S : Sieve U}
    (x : FamilyOfElements F S) : Prop :=
  ∀ {V W : C.Obj} (f : C.Hom V U) (hf : S.arrows f) (g : C.Hom W V),
    F.map g (x f hf) = x (C.comp g f) (S.downward_closed hf g)

/-- `t ∈ F(U)` が族 `x` の貼り合わせ（融合）であること。 -/
def FamilyOfElements.IsAmalgamation {F : CPresheaf C} {U : C.Obj} {S : Sieve U}
    (x : FamilyOfElements F S) (t : F.obj U) : Prop :=
  ∀ {V : C.Obj} (f : C.Hom V U) (hf : S.arrows f), F.map f t = x f hf

/-- 前層 `F` が篩 `S` について層条件を満たす: 両立する族はただ一つの貼り合わせを持つ。 -/
def IsSheafFor (F : CPresheaf C) {U : C.Obj} (S : Sieve U) : Prop :=
  ∀ x : FamilyOfElements F S, x.Compatible →
    ∃ t : F.obj U, x.IsAmalgamation t ∧ ∀ t', x.IsAmalgamation t' → t' = t

/-- サイト上の層: すべての被覆篩について層条件を満たす前層。 -/
structure CSheaf (𝒳 : Site.{u}) extends CPresheaf 𝒳.C where
  isSheaf : ∀ (U : 𝒳.C.Obj) (S : Sieve U), 𝒳.J.covering U S → IsSheafFor toCPresheaf S
end SiteSheaf

読み方。FamilyOfElements F S は「\(S\) の各射 \(f\) に \(\mathcal F(V)\) の元を割り当てる関数」（依存関数型 ∀ {V} (f : Hom V U), S.arrows f → F.obj V）。Compatible の条件 F.map g (x f hf) = x (C.comp g f) … は「\(x_f\) を \(g\) で引き戻したものは \(x_{f\circ g}\) に等しい」。07章の「\(V_i \cap V_j\) の上で一致」が、ここでは「任意の \(g\) で引き戻して一致」に一般化されている。交わり \(V_i \cap V_j\) は、圏の言葉ではファイバー積 \(V_i \times_U V_j\) であり、篩の定式化を使うとファイバー積の存在を仮定せずに層条件が書ける、というのが技術的な利点である。

IsSheafFor の結論 ∃ t, IsAmalgamation t ∧ ∀ t', IsAmalgamation t' → t' = t が「ただ一つ」の展開形である。CSheaf 𝒳 は、この条件をすべての被覆篩に課した前層である。

これでサイトの一般論は終わりである。あとは「\(X\) 上エタールなスキームの圏」に「全射な族を被覆とする位相」を載せるだけで、エタールサイトができる。そのために、エタール射を定義する。

14 — ÉTALE ALGEBRAS

エタール代数: 「局所同相」の代数版

エタール射は、雑にいうと「微分が同型な写像」の代数幾何版である。複素解析なら、\(f'(z) \ne 0\) のとき \(f\) は局所的に双正則写像になる（逆関数定理）。\(z \mapsto z^n\) は原点以外でエタールである。代数幾何ではザリスキ位相が粗すぎて「局所的に同型」にはならないが、「無限小のレベルでは同型」という条件を課すことができる。それが形式的エタールである。

無限小持ち上げ条件

\(R\)-代数 \(A\) が形式的エタールであるとは、任意の \(R\)-代数 \(B\) と、二乗すると \(0\) になるイデアル \(I \subseteq B\)（\(I^2 = 0\)）について、次の持ち上げがただ一通りに存在することである。

\[ \begin{array}{ccc} A & \xrightarrow{\ \ g\ \ } & B/I \\ & {\scriptstyle \exists!\, f\ \nearrow} & \big\uparrow \pi \\ & & B \end{array} \qquad\text{つまり}\qquad \operatorname{Hom}_R(A, B) \xrightarrow{\ \pi\circ -\ } \operatorname{Hom}_R(A, B/I) \text{ は全単射}. \]

直感はこうである。\(B/I\) は \(B\) の「一次近似」で、\(B \to B/I\) は無限小の情報を落とす。\(A\) が形式的エタールとは、\(A\) から \(B/I\) への写像が与えられれば、それを無限小の分だけ「ただ一通りに」延長できる、ということ。存在だけ（「少なくとも一つ」）なら形式的スムーズ、一意性だけ（「高々一つ」）なら形式的不分岐である。逆関数定理で「\(f'\ne0\) なら局所的に逆が一意に存在する」と言うのと同じ構造である。

section Algebras
variable {R : Type} [CommRing R]

/-- `R`-代数: 可換環 `A` と環準同型 `R → A`（構造射）。 -/
structure Algebra (R A : Type) [CommRing R] [CommRing A] where
  algebraMap : R →ᵣ A

/-- `R`-代数の準同型: 構造射と両立する環準同型。 -/
structure AlgHom {A B : Type} [CommRing A] [CommRing B] (𝒜 : Algebra R A) (ℬ : Algebra R B) where
  toRingHom : A →ᵣ B
  commutes : ∀ r, toRingHom (𝒜.algebraMap r) = ℬ.algebraMap r

\(R\)-代数とは、環 \(A\) と構造射 \(R \to A\) の組である。\(R\)-代数の準同型は構造射と両立する環準同型（commutes）。

/-- 「二乗零の核を持つ全射」: `π : B → C` 全射で、`ker π · ker π = 0`。
`C = B / I`, `I² = 0` という状況を、商環を構成せずに表現している。 -/
structure SquareZeroExt {B C : Type} [CommRing B] [CommRing C] (π : B →ᵣ C) : Prop where
  surj : Function.Surjective π.toFun
  sq_zero : ∀ a b, π a = 0 → π b = 0 → a * b = 0

/-- 形式的エタール: 任意の二乗零拡大 `π : B → C` に対し、`A → C` は `A → B` にただ一通りに持ち上がる。
図式: A ⟶ C を、A ⟶ B ⟶ C と分解する仕方が「ちょうど一つ」。 -/
def Algebra.FormallyEtale {A : Type} [CommRing A] (𝒜 : Algebra R A) : Prop :=
  ∀ (B C : Type) [CommRing B] [CommRing C] (ℬ : Algebra R B) (𝒞 : Algebra R C)
    (π : AlgHom ℬ 𝒞), SquareZeroExt π.toRingHom →
    ∀ (g : AlgHom 𝒜 𝒞),
      ∃ (f : AlgHom 𝒜 ℬ), (∀ a, π.toRingHom (f.toRingHom a) = g.toRingHom a) ∧
        ∀ (f' : AlgHom 𝒜 ℬ), (∀ a, π.toRingHom (f'.toRingHom a) = g.toRingHom a) → f' = f

/-- 形式的不分岐: 持ち上げは高々一つ。 -/
def Algebra.FormallyUnramified {A : Type} [CommRing A] (𝒜 : Algebra R A) : Prop :=
  ∀ (B C : Type) [CommRing B] [CommRing C] (ℬ : Algebra R B) (𝒞 : Algebra R C)
    (π : AlgHom ℬ 𝒞), SquareZeroExt π.toRingHom →
    ∀ (f₁ f₂ : AlgHom 𝒜 ℬ), (∀ a, π.toRingHom (f₁.toRingHom a) = π.toRingHom (f₂.toRingHom a)) → f₁ = f₂

/-- 形式的スムーズ: 持ち上げが少なくとも一つ。 -/
def Algebra.FormallySmooth {A : Type} [CommRing A] (𝒜 : Algebra R A) : Prop :=
  ∀ (B C : Type) [CommRing B] [CommRing C] (ℬ : Algebra R B) (𝒞 : Algebra R C)
    (π : AlgHom ℬ 𝒞), SquareZeroExt π.toRingHom →
    ∀ (g : AlgHom 𝒜 𝒞), ∃ (f : AlgHom 𝒜 ℬ), ∀ a, π.toRingHom (f.toRingHom a) = g.toRingHom a
end Algebras

技術的な工夫を一つ。商環 \(B/I\) を構成する代わりに、「二乗零の核を持つ全射 \(\pi : B \to C\)」という形で状況を表現している（SquareZeroExt）。\(\ker \pi = I\)、\(C \cong B/I\) なので数学的には同じであり、商環の構成（Quot による環構造と well-definedness の証明）を丸ごと省ける。

Algebra.FormallyEtale 𝒜 の本文を読む。「任意の \(B, C\)、\(R\)-代数構造、\(R\)-代数準同型 \(\pi\)、\(\pi\) が二乗零拡大、任意の \(g : A \to C\) について、\(\pi \circ f = g\) となる \(f : A \to B\) がただ一つ存在する」。FormallyUnramified は同じ設定で「\(\pi\circ f_1 = \pi\circ f_2 \Rightarrow f_1 = f_2\)」、FormallySmooth は「\(f\) が存在する」。エタール = 不分岐 + スムーズという関係が、定義の形からそのまま見える。

有限表示

形式的エタールだけでは、たとえば \(R \to \widehat R\)（完備化）のような「無限に大きい」拡大も含んでしまう。幾何学的に意味のある「有限型」の条件を足す必要がある。有限表示とは、有限個の変数の多項式環を、有限個の関係式で割ったものと同型であること。

\[ A \cong R[X_1, \dots, X_n] / (f_1, \dots, f_m). \]

そのために、まず多項式環 \(R[X_1,\dots,X_n]\) を作らなければならない。Lean 本体には多項式がないので、「多項式の式」を項として帰納的に定義し、環の公理で生成される合同関係で割るという、最も素朴な構成を採る。

section FreeAlgebra
variable (R : Type) [CommRing R] (n : Nat)

/-- 多項式の「式」。変数 `Xᵢ`、定数、和、積、マイナスから作られる項。 -/
inductive Term
  | var : Fin n → Term
  | const : R → Term
  | add : Term → Term → Term
  | mul : Term → Term → Term
  | neg : Term → Term

/-- 式の間の同値関係: 可換環の公理と「定数は環準同型」で生成される最小の合同関係。
`R[X₁,…,Xₙ]` はこれで式を割ったもの。 -/
inductive Term.Rel : Term R n → Term R n → Prop
  | refl (t) : Rel t t
  | symm {s t} : Rel s t → Rel t s
  | trans {s t u} : Rel s t → Rel t u → Rel s u
  | add_congr {s s' t t'} : Rel s s' → Rel t t' → Rel (.add s t) (.add s' t')
  | mul_congr {s s' t t'} : Rel s s' → Rel t t' → Rel (.mul s t) (.mul s' t')
  | neg_congr {s s'} : Rel s s' → Rel (.neg s) (.neg s')
  | add_assoc (a b c) : Rel (.add (.add a b) c) (.add a (.add b c))
  | add_comm (a b) : Rel (.add a b) (.add b a)
  | zero_add (a) : Rel (.add (.const 0) a) a
  | neg_add_cancel (a) : Rel (.add (.neg a) a) (.const 0)
  | mul_assoc (a b c) : Rel (.mul (.mul a b) c) (.mul a (.mul b c))
  | mul_comm (a b) : Rel (.mul a b) (.mul b a)
  | one_mul (a) : Rel (.mul (.const 1) a) a
  | mul_add (a b c) : Rel (.mul a (.add b c)) (.add (.mul a b) (.mul a c))
  | const_add (r s : R) : Rel (.const (r + s)) (.add (.const r) (.const s))
  | const_mul (r s : R) : Rel (.const (r * s)) (.mul (.const r) (.const s))

/-- 多項式環 `R[X₁, …, Xₙ]`。式を同値関係で割ったもの。 -/
def FreeCommAlg : Type := Quot (Term.Rel R n)

/-- `R[X₁,…,Xₙ]` は可換環（演習: 各演算が同値関係と両立し、公理は `Rel` の生成元から出る）。 -/
noncomputable instance : CommRing (FreeCommAlg R n) := sorry

/-- 構造射 `R → R[X₁,…,Xₙ]`, `r ↦ 定数 r`。 -/
noncomputable def FreeCommAlg.algebra : Algebra R (FreeCommAlg R n) := ⟨⟨fun r => Quot.mk _ (.const r), sorry, sorry, sorry⟩⟩

end FreeAlgebra

Term R n は、変数 \(X_i\)、定数 \(r\)、和、積、マイナスから作られる式の型である。Term.Rel は「二つの式が多項式として等しい」という関係で、（1）同値関係であること、（2）演算と両立すること、（3）可換環の8公理、（4）定数の埋め込みが環準同型であること、の規則で生成される。FreeCommAlg R n := Quot Rel がこれで割った商である。

これは「自由可換 \(R\)-代数」の普遍性からの構成で、\(R[X_1,\dots,X_n]\) の元を「係数の有限列」で表す通常の構成とは異なる。しかし普遍性（\(A\) への \(R\)-代数準同型は変数の行き先 \(x_1, \dots, x_n \in A\) で決まる）は同じであり、定義の見通しはこちらの方がよい。

section Etale
variable {R : Type} [CommRing R]

/-- 有限表示: 有限変数の多項式環からの全射で、核が有限生成のもの。
`A ≅ R[X₁,…,Xₙ] / (f₁,…,fₘ)`。 -/
def Algebra.FinitePresentation {A : Type} [CommRing A] (𝒜 : Algebra R A) : Prop :=
  ∃ (n : Nat) (φ : AlgHom (FreeCommAlg.algebra R n) 𝒜),
    Function.Surjective φ.toRingHom.toFun ∧ φ.toRingHom.ker.IsFG

/-- エタール代数 = 形式的エタール + 有限表示。 -/
def Algebra.Etale {A : Type} [CommRing A] (𝒜 : Algebra R A) : Prop :=
  𝒜.FormallyEtale ∧ 𝒜.FinitePresentation

/-- 環準同型 `φ : R → S` がエタール: `S` を `φ` で `R`-代数と見てエタール。 -/
def RingHom.IsEtale {S : Type} [CommRing S] (φ : R →ᵣ S) : Prop :=
  Algebra.Etale (⟨φ⟩ : Algebra R S)

/-- 恒等写像はエタール。 -/
theorem RingHom.id_isEtale : (RingHom.id R).IsEtale := sorry

/-- 例: 局所化 `R → R[1/f]` はエタール（開埋め込み `D(f) ↪ Spec R` に対応）。 -/
theorem localization_isEtale (f : R) : (Localization.algebraMap (Submonoid.powers f)).IsEtale := sorry
end Etale

Algebra.FinitePresentation：「ある \(n\) と、全射な \(R\)-代数準同型 \(\varphi : R[X_1,\dots,X_n] \to A\) があって、\(\ker\varphi\) が有限生成」。Algebra.Etale はその二条件の連言である。RingHom.IsEtale φ は環準同型 \(\varphi : R \to S\) を「\(S\) を \(\varphi\) で \(R\)-代数と見たとき」に読み替えたもので、次章のスキームの射で使う形である。

例として、恒等写像と局所化 \(R \to R[1/f]\) がエタールであることを定理として述べた（定理）。局所化のエタール性は、幾何学的には「開埋め込み \(D(f) \hookrightarrow \operatorname{Spec} R\) はエタール」を意味する。他の典型例を数式だけで挙げておく。

1. 標準エタール代数

   \(R[x]_g / (f)\) で、\(f\) はモニック、\(f'\) が \(R[x]_g/(f)\) で可逆。「\(f'\ne0\) なら局所同相」の代数版で、実はすべてのエタール代数は局所的にこの形である（局所構造定理）。

2. 体の分離拡大

   \(k \to L\) がエタール \(\iff\) \(L\) は \(k\) の有限分離拡大（の有限積）。分離性が「不分岐」、有限性が「有限表示」に対応する。

3. 反例: \(\mathbb Z \to \mathbb Z[i]\)

   \(2\) で分岐する（\((2) = (1+i)^2\)）ので不分岐でない。一方 \(\mathbb Z[1/2] \to \mathbb Z[1/2][i]\) はエタール。

15 — THE ÉTALE SITE

エタール射と、エタールサイト

スキームの射 \(f : X \to Y\) がエタールであることを、環準同型のエタール性に帰着させて定義する。11章で用意した \(f^\sharp_{U,V} : \mathcal O_Y(U) \to \mathcal O_X(V)\) を使う。

\[ f \text{ がエタール } :\iff \forall\, U \subseteq Y \text{ アフィン開},\ \forall\, V \subseteq f^{-1}U \text{ アフィン開},\quad f^\sharp_{U,V} : \mathcal O_Y(U) \to \mathcal O_X(V) \text{ はエタール}. \]

/-- スキームの射 `f : X → Y` がエタール: `Y` のアフィン開集合 `U` と、`f⁻¹U` に含まれる `X` の
アフィン開集合 `V` のすべてについて、環準同型 `𝒪_Y(U) → 𝒪_X(V)` がエタール。 -/
def Scheme.Hom.IsEtale {X Y : Scheme} (f : Scheme.Hom X Y) : Prop :=
  ∀ (U : Opens Y.X) (V : Opens X.X) (h : V ≤ f.base.preimage U),
    Y.IsAffineOpen U → X.IsAffineOpen V → (f.appLE U V h).IsEtale

/-- 恒等射はエタール（演習: `R → R` は形式的エタールかつ有限表示）。 -/
theorem Scheme.id_isEtale (X : Scheme) :
    Scheme.Hom.IsEtale (X := X) (Y := X) (LRSHom.id X.toLocallyRingedSpace) := sorry

この定義は「すべてのアフィン開の組で成り立つ」と要求している。実際には「あるアフィン開被覆で成り立てばよい」ことが定理として示せる（エタール性は局所化で保たれ、局所的な性質だから）。その定理はここでは扱わない。恒等射がエタールであることは、環の言葉では「\(R \to R\) はエタール」であり、定理として述べた。

小エタールサイト \(X_{\mathrm{ét}}\)

いよいよエタールサイトである。対象は「\(X\) 上エタールなスキーム」\((U, f : U \to X)\)、射は \(X\) 上の射、そして被覆は「像が合わさって全体になる射の族」（jointly surjective）である。

\[ \{U_i \to U\}_i \text{ が被覆 } :\iff \bigcup_i \operatorname{im}(U_i \to U) = U. \]

/-- `X` 上エタールなスキーム `(U, f : U → X)`。小エタールサイトの対象。 -/
structure EtaleOver (X : Scheme) where
  U : Scheme
  f : Scheme.Hom U X
  etale : f.IsEtale

/-- `X` 上の射: `X` への射と両立するスキームの射。 -/
structure EtaleOver.Hom {X : Scheme} (V U : EtaleOver X) where
  g : Scheme.Hom V.U U.U
  w : LRSHom.comp g U.f = V.f

/-- `X` 上エタールなスキームの圏 `Ét(X)`。 -/
noncomputable abbrev etaleCategory (X : Scheme) : Category.{1} where
  Obj := EtaleOver X
  Hom := EtaleOver.Hom
  id U := ⟨LRSHom.id _, sorry⟩
  comp g h := ⟨LRSHom.comp g.g h.g, sorry⟩
  id_comp := sorry
  comp_id := sorry
  assoc := sorry

EtaleOver X が対象の型（Type 1 に住むことに注意——スキーム全体は大きい）。EtaleOver.Hom V U は \(V \to U\) であって \(X\) への射と両立するもの（w が三角形の可換性）。etaleCategory X はこれらを 12章の Category 構造にまとめたもので、単位律・結合律は局所環付き空間の射のそれに帰着する（演習）。

/-- エタール位相。`U` 上の篩が被覆 ⇔ 篩に属する射たちの像が `U` を覆う（jointly surjective）。 -/
noncomputable def etaleTopology (X : Scheme) : GrothendieckTopology (etaleCategory X) where
  covering U S := ∀ x : U.U.X, ∃ (V : EtaleOver X) (g : EtaleOver.Hom V U) (y : V.U.X),
    S.arrows g ∧ g.g.base.toFun y = x
  top_mem := sorry          -- 恒等射一本で覆える
  pullback_stable := sorry  -- 定理: エタール射はファイバー積で保たれ、全射性も保たれる
  transitive := sorry       -- 被覆の被覆は被覆

/-- 小エタールサイト `X_ét`。 -/
noncomputable abbrev etaleSite (X : Scheme) : Site.{1} := ⟨etaleCategory X, etaleTopology X⟩

/-- `X` 自身（恒等射）はエタールサイトの終対象。層の「大域切断」はここでの値。 -/
noncomputable def EtaleOver.self (X : Scheme) : EtaleOver X := ⟨X, LRSHom.id _, X.id_isEtale⟩

covering U S の定義を読む。「\(U\) の各点 \(x\) に対して、\(S\) に属する射 \(g : V \to U\) と \(V\) の点 \(y\) があって \(g(y) = x\)」。これが jointly surjective を篩の言葉で書いたものである。

三つの公理はすべて sorry で、これは 定理である。特に (T2) 引き戻し安定性は、「エタール射の族のファイバー積による基底変換はエタールで、全射性は基底変換で保たれる」という本物の定理（エタール射は基底変換で安定。Stacks Project, Étale Morphisms of Schemes）に依存する。位相空間の開被覆では「\(f^{-1}\) で引き戻せば被覆」が自明だったが、エタール射では「ファイバー積 \(V \times_U U_i\) がまたエタールで、それらが \(V\) を覆う」ことを示さなければならない。

最後に、\(X\) 自身（恒等射）はこの圏の終対象で、層の「大域切断」\(\mathcal F(X)\) はここでの値である。これは次章以降で使う。

16 — ABELIAN SHEAVES

アーベル層、完全列、入射的対象

コホモロジーを取るには、層の値が集合ではなくアーベル群でなければならない。「切断を足したり引いたりできる」ことが、核や像、ひいては「どれだけ貼り合わせに失敗したか」を測る道具になる。

/-- アーベル群。 -/
class AddCommGroup (A : Type) extends Add A, Neg A, Zero A where
  add_assoc : ∀ a b c : A, a + b + c = a + (b + c)
  add_comm  : ∀ a b : A, a + b = b + a
  zero_add  : ∀ a : A, 0 + a = a
  neg_add_cancel : ∀ a : A, -a + a = 0

/-- 可換環は（足し算について）アーベル群。 -/
instance {R : Type} [CommRing R] : AddCommGroup R where
  add_assoc := CommRing.add_assoc
  add_comm := CommRing.add_comm
  zero_add := CommRing.zero_add
  neg_add_cancel := CommRing.neg_add_cancel

/-- アーベル群の準同型。 -/
structure AddHom (A B : Type) [AddCommGroup A] [AddCommGroup B] where
  toFun : A → B
  map_add : ∀ a b, toFun (a + b) = toFun a + toFun b

instance {A B : Type} [AddCommGroup A] [AddCommGroup B] : CoeFun (AddHom A B) (fun _ => A → B) :=
  ⟨AddHom.toFun⟩

可換環と同じ流儀で、公理4つの型クラスとして定義する。可換環は加法についてアーベル群である、というインスタンスも付けた。

section AbelianSheaves
variable {𝒳 : Site.{u}}

/-- アーベル群の前層: 各対象にアーベル群、各射に群準同型。 -/
structure AbPresheaf (C : Category.{u}) where
  obj : C.Obj → Type
  grp : ∀ U, AddCommGroup (obj U)
  map : ∀ {U V : C.Obj}, C.Hom V U → obj U → obj V
  map_add : ∀ {U V : C.Obj} (f : C.Hom V U) (s t : obj U), map f (s + t) = map f s + map f t
  map_id : ∀ (U : C.Obj) (s : obj U), map (C.id U) s = s
  map_comp : ∀ {U V W : C.Obj} (f : C.Hom V U) (g : C.Hom W V) (s : obj U),
    map g (map f s) = map (C.comp g f) s

attribute [instance] AbPresheaf.grp

/-- 群構造を忘れて集合値の前層と見る。 -/
def AbPresheaf.toCPresheaf {C : Category.{u}} (F : AbPresheaf C) : CPresheaf C :=
  ⟨F.obj, F.map, F.map_id, F.map_comp⟩

/-- サイト上のアーベル群の層。 -/
structure AbSheaf (𝒳 : Site.{u}) extends AbPresheaf 𝒳.C where
  isSheaf : ∀ (U : 𝒳.C.Obj) (S : Sieve U), 𝒳.J.covering U S → IsSheafFor toAbPresheaf.toCPresheaf S

/-- アーベル層の射: 各対象で群準同型、制限と両立（自然変換）。 -/
structure AbSheaf.Hom (F G : AbSheaf 𝒳) where
  app : ∀ U, F.obj U → G.obj U
  app_add : ∀ U (a b : F.obj U), app U (a + b) = app U a + app U b
  naturality : ∀ {U V : 𝒳.C.Obj} (f : 𝒳.C.Hom V U) (s : F.obj U), app V (F.map f s) = G.map f (app U s)

/-- 零射。 -/
def AbSheaf.Hom.zero (F G : AbSheaf 𝒳) : F.Hom G := ⟨fun _ _ => 0, sorry, sorry⟩

AbPresheaf は「各対象にアーベル群、各射に群準同型」で、13章の CPresheaf に群構造を足したものである。AbSheaf 𝒳 は、群構造を忘れた前層（toCPresheaf）が層条件を満たすもの。層の条件は集合値のときと同じでよく、群構造は「切断の集合に加法がある」という追加のデータに過ぎない、というのがここでの整理である。

AbSheaf.Hom F G は層の射（自然変換）で、各対象で群準同型 app U をなし、制限と可換（naturality）。

完全列を「局所的に」定義する

ここに層の理論の核心がある。アーベル群の列 \(A \to B \to C\) が完全とは「像 = 核」だが、層の列 \(\mathcal F \xrightarrow{\varphi} \mathcal G \xrightarrow{\psi} \mathcal H\) では、各 \(U\) で \(\mathcal F(U) \to \mathcal G(U) \to \mathcal H(U)\) が完全であることを要求してはいけない。要求してよいのは「茎で完全」または「局所的に完全」であり、\(\ker \psi_U\) の元は \(U\) 上では \(\varphi\) の像に入らなくても、\(U\) のある被覆の上では入る、という形になる。

\[ \psi\circ\varphi = 0,\quad\text{かつ}\quad \forall s \in \mathcal G(U),\ \psi(s)=0 \Rightarrow \exists\, \{U_i \to U\} \in J(U),\ \exists\, t_i \in \mathcal F(U_i),\ \varphi(t_i) = s|_{U_i}. \]

なぜ「局所的」でなければならないか。指数関数列 \(0 \to \mathbb Z \to \mathcal O \xrightarrow{\exp} \mathcal O^\times \to 0\) を思い出すとよい。\(\mathbb C^\times\) 上の関数 \(z\) は \(\mathcal O^\times\) の切断だが、大域的な対数を持たない。しかし局所的には持つ。層の完全性とは、まさにこの「局所的には解ける」を公理化したものである。そして「局所的に解けるのに大域的に解けない度合い」を測るのがコホモロジーである。

/-- 単射（モノ射）: 各対象の上で単射。 -/
def AbSheaf.Hom.IsMono {F G : AbSheaf 𝒳} (φ : F.Hom G) : Prop :=
  ∀ U, Function.Injective (φ.app U)

/-- `F →φ→ G →ψ→ H` が `G` で完全。
(1) `ψ ∘ φ = 0`、(2) `ψ(s) = 0` なる切断 `s ∈ G(U)` は、`U` のある被覆の上で局所的に `φ` の像に入る。
（層の圏では「像 = 核」を各切断ごとには要求できないので、被覆の上での持ち上げで言い換える。） -/
def AbSheaf.IsExactAt {F G H : AbSheaf 𝒳} (φ : F.Hom G) (ψ : G.Hom H) : Prop :=
  (∀ U (s : F.obj U), ψ.app U (φ.app U s) = 0) ∧
  ∀ (U : 𝒳.C.Obj) (s : G.obj U), ψ.app U s = 0 →
    ∃ S : Sieve U, 𝒳.J.covering U S ∧
      ∀ {V : 𝒳.C.Obj} (f : 𝒳.C.Hom V U), S.arrows f → ∃ t : F.obj V, φ.app V t = G.map f s

IsExactAt φ ψ の第二成分が上の式である。∃ S : Sieve U, covering U S ∧ ∀ {V} (f : Hom V U), S.arrows f → ∃ t : F.obj V, φ.app V t = G.map f s——「被覆篩 \(S\) があって、\(S\) の各射 \(f : V \to U\) について、\(s\) の \(V\) への引き戻しが \(\varphi\) の像に入る」。位相空間の場合の茎による定義（\(\mathcal F_x \to \mathcal G_x \to \mathcal H_x\) が完全）を、点を使わずに書いたものである。エタールサイトにも「点」（幾何学的点 \(\operatorname{Spec}\bar k \to X\)）はあり、茎による定義も可能だが、被覆による定義の方が一般的である。

この定義には層化（前層を層にする操作）が出てこない。教科書では「像の層 = 像の前層の層化」を定義してから完全性を言うが、上の定式化は層化を経由せずに同じ内容を述べている。層化の構成を省けたのは、このノートの構成上の小さな利点である。

入射的対象と入射的分解

導来関手の定義には入射的対象が要る。層 \(\mathcal I\) が入射的とは、任意の単射 \(\iota : \mathcal A \hookrightarrow \mathcal B\) と射 \(\alpha : \mathcal A \to \mathcal I\) に対して、\(\alpha\) が \(\mathcal B\) まで延長できること。

\[ \begin{array}{ccc} \mathcal A & \xrightarrow{\ \iota\ } & \mathcal B \\ {\scriptstyle\alpha}\big\downarrow & \swarrow{\scriptstyle \exists\,\beta} & \\ \mathcal I & & \end{array} \qquad \beta\circ\iota = \alpha. \]

直感的には、入射的対象は「十分に大きくて柔らかく、どこからでも写像を延長して受け止められる」対象である。アーベル群では \(\mathbb Q\) や \(\mathbb Q/\mathbb Z\) が入射的（可除群）。層では、各点で入射的群を立てた「摩天楼層の積」が入射的になる。

/-- 入射的対象: 単射 `A ↪ B` に沿って、`A → I` はいつでも `B → I` に延長できる。 -/
def AbSheaf.IsInjective (I : AbSheaf 𝒳) : Prop :=
  ∀ (A B : AbSheaf 𝒳) (ι : A.Hom B), ι.IsMono →
    ∀ (α : A.Hom I), ∃ β : B.Hom I, ∀ U (a : A.obj U), β.app U (ι.app U a) = α.app U a

/-- 入射的分解 `0 → F → I⁰ → I¹ → I² → ⋯`（完全列で、各 `Iⁿ` が入射的）。 -/
structure InjectiveResolution (F : AbSheaf 𝒳) where
  I : Nat → AbSheaf 𝒳
  injective : ∀ n, (I n).IsInjective
  ε : F.Hom (I 0)
  d : ∀ n, (I n).Hom (I (n + 1))
  ε_mono : ε.IsMono
  exact₀ : AbSheaf.IsExactAt ε (d 0)
  exact : ∀ n, AbSheaf.IsExactAt (d n) (d (n + 1))
end AbelianSheaves

InjectiveResolution F は、層の列 \(0 \to \mathcal F \xrightarrow{\varepsilon} \mathcal I^0 \xrightarrow{d^0} \mathcal I^1 \xrightarrow{d^1} \cdots\) で、各 \(\mathcal I^n\) が入射的、\(\varepsilon\) が単射、各所で完全なもの。exact₀ が \(\mathcal I^0\) での完全性、exact n が \(\mathcal I^{n+1}\) での完全性である。

このデータが常に存在すること（アーベル層の圏は十分な入射的対象を持つ）は、グロタンディークの Tôhoku 論文の定理で、証明はやさしくない。次章で定理として述べる。

17 — COHOMOLOGY OF A COMPLEX

複体のコホモロジーと、大域切断

最後の部品は、アーベル群の余鎖複体とそのコホモロジーである。複体 \(A^0 \xrightarrow{d^0} A^1 \xrightarrow{d^1} A^2 \to \cdots\)、\(d^{n+1}\circ d^n = 0\) に対して

\[ Z^n := \ker d^n,\qquad B^n := \operatorname{im} d^{n-1}\ (B^0 := 0),\qquad H^n(A^\bullet) := Z^n / B^n. \]

\(d\circ d = 0\) より \(B^n \subseteq Z^n\) であり、\(H^n\) は「閉じているが、境界ではないもの」を測る。

/-- アーベル群の余鎖複体 `A⁰ → A¹ → A² → ⋯`, `d ∘ d = 0`。 -/
structure Cocomplex where
  A : Nat → Type
  grp : ∀ n, AddCommGroup (A n)
  d : ∀ n, AddHom (A n) (A (n + 1))
  d_d : ∀ n (a : A n), d (n + 1) (d n a) = 0

attribute [instance] Cocomplex.grp

namespace Cocomplex
variable (K : Cocomplex)

/-- 余輪体 `Zⁿ = ker dⁿ`。 -/
def Cocycles (n : Nat) : Type := { a : K.A n // K.d n a = 0 }

/-- 余境界 `Bⁿ = im dⁿ⁻¹`（`n = 0` では `0`）。 -/
def IsCoboundary : ∀ n : Nat, K.A n → Prop
  | 0 => fun a => a = 0
  | n + 1 => fun a => ∃ b : K.A n, K.d n b = a

/-- コホモロジー `Hⁿ(K) = Zⁿ / Bⁿ`。二つの余輪体は差が余境界なら同一視する。 -/
def H (n : Nat) : Type :=
  Quot (fun a b : K.Cocycles n => K.IsCoboundary n (a.1 + -b.1))
end Cocomplex

Cocycles n が \(Z^n\)（部分型）、IsCoboundary n a が「\(a \in B^n\)」で、\(n = 0\) と \(n+1\) で場合分けしている（Lean では \(A^{-1}\) がないので、\(B^0 = 0\) を別に書く必要がある）。H n は「二つの余輪体は差が余境界なら同一視する」という関係による Quot。これで \(Z^n/B^n\) になる。これも局所化・茎と同じ Quot のパターンである。

/-- 入射的分解の各項を `X` 自身で評価した複体 `Γ(X, I⁰) → Γ(X, I¹) → ⋯`。 -/
noncomputable def globalSections {X : Scheme} {F : AbSheaf (etaleSite X)}
    (I : InjectiveResolution F) : Cocomplex where
  A n := (I.I n).obj (EtaleOver.self X)
  grp n := (I.I n).grp _
  d n := ⟨(I.d n).app _, (I.d n).app_add _⟩
  d_d n a := (I.exact n).1 _ a

入射的分解 \(\mathcal I^\bullet\) の各項を \(X\) 自身（エタールサイトの終対象）で評価すると、アーベル群の複体 \(\Gamma(X, \mathcal I^0) \to \Gamma(X, \mathcal I^1) \to \cdots\) ができる。d_d（\(d\circ d = 0\)）は、層の完全性の第一成分 \(\psi\circ\varphi=0\) をそのまま \(X\) で評価したもので、証明が埋まっている（(I.exact n).1 _ a）。

大事な点を一つ。層の列は完全でも、大域切断の列 \(\Gamma(X,\mathcal I^\bullet)\) は完全とは限らない。\(\Gamma(X, -)\) は左完全だが右完全ではない。この「完全性の崩れ」がコホモロジーであり、入射的分解を取るのは、その崩れ具合を「分解の取り方によらない」形で取り出すための標準的な手続きである。

18 — THE DEFINITION

エタール・コホモロジーの定義

部品が全部そろった。定義を書く。

/-- 定理（十分な入射的対象の存在）: すべてのアーベル層は入射的分解を持つ。 -/
theorem exists_injectiveResolution {X : Scheme} (F : AbSheaf (etaleSite X)) :
    Nonempty (InjectiveResolution F) := sorry

/-- **エタール・コホモロジー** `Hⁿ(X_ét, F)`。
入射的分解 `F → I•` を一つ選び、大域切断の複体 `Γ(X, I•)` の `n` 次コホモロジーを取る。 -/
noncomputable def etaleCohomology (X : Scheme) (F : AbSheaf (etaleSite X)) (n : Nat) : Type :=
  (globalSections (Classical.choice (exists_injectiveResolution F))).H n

読み方。exists_injectiveResolution F は「\(\mathcal F\) の入射的分解が存在する」という定理（証明は sorry）。Classical.choice でその一つを選び、globalSections で大域切断の複体にし、.H n で \(n\) 次コホモロジーを取る。

\[ H^n(X_{\mathrm{ét}}, \mathcal F) \;=\; H^n\bigl(\Gamma(X, \mathcal I^\bullet)\bigr),\qquad 0 \to \mathcal F \to \mathcal I^\bullet \text{ 入射的分解}. \]

これが Type（普通のサイズの型）に住むことにも注意してほしい。エタールサイトの対象は Type 1 に住むが、切断の群はすべて Type であり、その商も Type である。00章で「Ext群は集合である」と言ったことが、この構成では自動的に成り立っている。

定義に付随する定理

定義が「定義として意味を持つ」ためには、次が成り立たなければならない。いずれも 定理として述べ、証明は sorry にした。

/-- 二つの型の間の全単射。 -/
structure Bijection (α β : Type) where
  toFun : α → β
  invFun : β → α
  left_inv : ∀ a, invFun (toFun a) = a
  right_inv : ∀ b, toFun (invFun b) = b

/-- 定理（分解の取り方によらない）: 別の入射的分解を使っても同じ群が得られる。 -/
theorem etaleCohomology_independent {X : Scheme} (F : AbSheaf (etaleSite X)) (n : Nat)
    (I I' : InjectiveResolution F) :
    Nonempty (Bijection ((globalSections I).H n) ((globalSections I').H n)) := sorry

/-- 定理: `H⁰(X_ét, F) = F(X)`（大域切断）。 -/
theorem etaleCohomology_zero (X : Scheme) (F : AbSheaf (etaleSite X)) :
    Nonempty (Bijection (etaleCohomology X F 0) (F.obj (EtaleOver.self X))) := sorry

1. 分解の取り方によらない

   二つの入射的分解は鎖ホモトピー同値であり、大域切断のコホモロジーは同型になる。これが「導来関手は well-defined」の内容で、Classical.choice でどの分解を選んでも同じ群が得られることを保証する。

2. \(H^0(X_{\mathrm{ét}}, \mathcal F) = \mathcal F(X)\)

   \(0 \to \mathcal F \to \mathcal I^0 \to \mathcal I^1\) の完全性と \(\Gamma\) の左完全性から、\(\ker(\Gamma(\mathcal I^0)\to\Gamma(\mathcal I^1)) = \Gamma(\mathcal F)\)。0 次コホモロジーは大域切断である。

ここで一度、依存の鎖を最下段から振り返っておく。CommRing（02）→ RingHom（03）→ Ideal、IsPrime（04）→ PrimeSpectrum、Topology（05）→ Localization（06）→ Presheaf、Sheaf（07）→ Stalk（08）→ SheafOfRings、specSheaf（09）→ LocallyRingedSpace、LRSHom（10）→ Scheme（11）→ Category、Sieve、GrothendieckTopology（12）→ IsSheafFor（13）→ Algebra.Etale（14）→ etaleSite（15）→ AbSheaf、IsExactAt、InjectiveResolution（16）→ Cocomplex.H、globalSections（17）→ etaleCohomology（18）。約1000行、外部ライブラリなし。これが「セルフコンテインド」の具体的な意味である。

19 — COEFFICIENTS

係数層: 定数層、𝔾ₘ、μₙ と Kummer 列

定義ができたので、何を係数にして計算するのかを見る。エタール・コホモロジーで最も重要な係数は定数層 \(\mathbb Z/n\mathbb Z\)（\(n\) が \(X\) 上可逆のとき）である。ザリスキ位相では見えなかったものが、エタール位相では見える。

定数層 \(\underline{A}\) は「\(U\) 上の局所定数関数 \(U \to A\)」の層である。位相空間の言葉でいえば、\(A\) に離散位相を入れた連続関数。

\[ \underline{A}(U) := \{\, s : U \to A \mid s \text{ は局所定数} \,\} = C(U, A_{\mathrm{disc}}). \]

section Coefficients
variable (X : Scheme)

/-- 局所定数関数: 各点の近傍で一定。 -/
def IsLocallyConstant {T : TopSpace} {α : Type} (s : T → α) : Prop :=
  ∀ x, ∃ W : Opens T, W.1 x ∧ ∀ y, W.1 y → s y = s x

/-- 定数層 `ℤ/nℤ`: `U ↦ { U → ℤ/nℤ : 局所定数 }`。 `Fin n` を `ℤ/nℤ` として使う。 -/
noncomputable def constantSheaf (n : Nat) : AbSheaf (etaleSite X) where
  obj (U : EtaleOver X) := { s : U.U.X → Fin (n + 1) // IsLocallyConstant s }
  grp _ := sorry
  map {U V : EtaleOver X} (g : EtaleOver.Hom V U) s := ⟨fun y => s.1 (g.g.base.toFun y), sorry⟩
  map_add := sorry
  map_id := sorry
  map_comp := sorry
  isSheaf := sorry  -- 定理: 局所定数関数はエタール被覆に沿って貼り合う

Fin (n+1) を \(\mathbb Z/(n+1)\mathbb Z\) として使っている（Lean 本体の Fin には mod の足し算が入っている）。層であることは 定理である：エタール射は開写像で、jointly surjective な族に沿って局所定数関数が貼り合うことを示す必要がある。

/-- 乗法群 `𝔾ₘ`: `U ↦ 𝒪(U)ˣ`。群演算は掛け算。 -/
noncomputable def Gm : AbSheaf (etaleSite X) where
  obj (U : EtaleOver X) := { a : U.U.𝒪.obj Opens.univ // IsUnit a }
  grp _ := sorry    -- 単元群（掛け算をアーベル群の「+」として使う）
  map {U V : EtaleOver X} (g : EtaleOver.Hom V U) a := ⟨g.g.sharp Opens.univ a.1, sorry⟩
  map_add := sorry
  map_id := sorry
  map_comp := sorry
  isSheaf := sorry  -- 定理（エタール降下）: `𝒪` はエタール位相で層

/-- 自然数 `n` を環の元 `n · 1` と見る。 -/
def ofNat' {R : Type} [CommRing R] : Nat → R
  | 0 => 0
  | n + 1 => ofNat' n + 1

/-- `n` 乗写像 `𝔾ₘ → 𝔾ₘ`。 -/
noncomputable def Gm.pow (n : Nat) : (Gm X).Hom (Gm X) := ⟨fun U a => ⟨npow a.1 n, sorry⟩, sorry, sorry⟩

/-- `n` 乗根の層 `μₙ = ker(𝔾ₘ →ⁿ 𝔾ₘ)`。 -/
noncomputable def mu (n : Nat) : AbSheaf (etaleSite X) where
  obj (U : EtaleOver X) := { a : (Gm X).obj U // npow a.1 n = 1 }
  grp _ := sorry
  map {U V : EtaleOver X} (g : EtaleOver.Hom V U) a := ⟨(Gm X).map g a.1, sorry⟩
  map_add := sorry
  map_id := sorry
  map_comp := sorry
  isSheaf := sorry

/-- 包含 `μₙ → 𝔾ₘ`。 -/
noncomputable def mu.incl (n : Nat) : (mu X n).Hom (Gm X) := ⟨fun _ a => a.1, sorry, sorry⟩

乗法群 \(\mathbb G_m(U) := \mathcal O(U)^\times\) と、その部分層 \(\mu_n(U) := \{a \in \mathcal O(U)^\times \mid a^n = 1\}\)。\(\mathbb G_m\) がエタール位相で層であることは、構造層 \(\mathcal O\) がエタール位相（実は fpqc 位相）で層であるという降下理論の基本定理（Grothendieck の忠実平坦降下）による。

/-- **Kummer 完全列** `0 → μₙ → 𝔾ₘ →ⁿ 𝔾ₘ → 0`（`n` が `X` 上可逆のとき、エタール位相で完全）。 -/
theorem kummer_exact (n : Nat) (hn : IsUnit (ofNat' n : X.𝒪.obj Opens.univ)) :
    (mu.incl X n).IsMono ∧ AbSheaf.IsExactAt (mu.incl X n) (Gm.pow X n) ∧
    ∀ (U : EtaleOver X) (a : (Gm X).obj U), ∃ S : Sieve U, (etaleTopology X).covering U S ∧
      ∀ {V : EtaleOver X} (f : EtaleOver.Hom V U), S.arrows (C := etaleCategory X) f →
        ∃ b : (Gm X).obj V, (Gm.pow X n).app V b = (Gm X).map f a := sorry
end Coefficients

Kummer 列 \(0 \to \mu_n \to \mathbb G_m \xrightarrow{\ n\ } \mathbb G_m \to 0\) は、\(n\) が \(X\) 上可逆のとき、エタール位相で完全である。特に右側の全射性（\(n\) 乗根がエタール局所的に取れる）はザリスキ位相では成り立たない。\(a \in \mathcal O(U)^\times\) の \(n\) 乗根を取る操作は、\(U' = U[t]/(t^n - a) \to U\) というエタール被覆を取れば可能になるが、これは開埋め込みではない。まさにこの一点のために、エタール位相が必要だった。

Kummer 列の長完全列から、ただちに次が得られる（Hilbert の定理 90 の層版 \(H^1(X_{\mathrm{ét}}, \mathbb G_m) = \operatorname{Pic}(X)\) と合わせて）。

\[ 0 \to \mathcal O(X)^\times / n \to H^1(X_{\mathrm{ét}}, \mu_n) \to \operatorname{Pic}(X)[n] \to 0. \]

これがエタール・コホモロジーの最初の「計算」であり、\(X\) が体 \(k\) のとき \(H^1(k_{\mathrm{ét}}, \mu_n) = k^\times / (k^\times)^n\) というクンマー理論そのものになる。

20 — MAIN THEOREMS

主定理: 比較・基底変換・双対・Weil 予想

定義が書けたので、この理論が「何を成し遂げるのか」を、主定理の形で整理する。以下はすべて NOT YET、つまりこのノートの Lean ファイルには入っていない。数式で正確に述べ、参照先を付ける。文献は英語で確認した（Milne Lectures on Étale Cohomology、Stacks Project、Deligne La conjecture de Weil I、Freitag–Kiehl）。

以下、\(\Lambda = \mathbb Z/\ell^m\) または \(\mathbb Q_\ell\)、\(\ell\) は \(X\) 上可逆な素数、\(k\) は分離閉体とする。

1. 点のコホモロジー = ガロア・コホモロジー

\[ H^i\bigl((\operatorname{Spec} k)_{\mathrm{ét}}, \mathcal F\bigr) \;\cong\; H^i\bigl(\operatorname{Gal}(k^{\mathrm{s}}/k),\ \mathcal F_{\bar k}\bigr). \]

体のエタールサイト上の層は、絶対ガロア群の離散モジュールと同じものである。エタール・コホモロジーはガロア・コホモロジーの「幾何学的な広がりを持った版」であり、この定理がその架け橋になる。数論的な応用（Brauer 群、類体論との関係）はここを通る。

2. Artin の比較定理

\(X\) を \(\mathbb C\) 上有限型のスキーム、\(\mathcal F\) を構成可能層（有限係数）とする。

\[ H^i(X_{\mathrm{ét}}, \mathcal F) \;\cong\; H^i\bigl(X(\mathbb C)^{\mathrm{an}},\ \mathcal F^{\mathrm{an}}\bigr). \]

右辺は複素解析的な空間の（特異）コホモロジーである。これが「エタール位相は正しい位相である」ことの証拠であり、グロタンディークの構想（純代数的な手段で位相不変量を復元する）が実現したことを意味する。有限係数が必要で、\(\mathbb Z\) 係数では成り立たない（たとえば正規なスキームでは \(H^1(X_{\mathrm{ét}}, \mathbb Z) = 0\) になってしまう）。

3. 有限性と固有基底変換

\(f : X \to Y\) を固有射、\(\mathcal F\) を \(X\) 上の構成可能層（ねじれ係数）とする。

\[ R^i f_* \mathcal F \text{ は構成可能},\qquad (R^i f_* \mathcal F)_{\bar y} \;\cong\; H^i\bigl(X_{\bar y},\ \mathcal F|_{X_{\bar y}}\bigr). \]

右の式が固有基底変換で、「固有射の高次順像の茎は、ファイバーのコホモロジー」である。トポロジーの固有写像に対する同様の定理の類似で、理論全体の技術的な要石になっている。有限性（\(X\) が \(k\) 上固有なら \(H^i(X_{\mathrm{ét}}, \mathcal F)\) は有限群）もここから出る。

4. スムーズ基底変換と純粋性

ファイバー積の図式で \(f : Y' \to Y\) がスムーズ、\(g : X \to Y\) が準コンパクト準分離、\(\mathcal F\) がねじれ層のとき、

\[ f^* R^i g_* \mathcal F \;\xrightarrow{\ \sim\ }\; R^i g'_* (f'^* \mathcal F). \]

また \(Z \hookrightarrow X\) が余次元 \(c\) の正則閉埋め込み（スムーズなスキームの中のスムーズな閉部分スキーム）のとき、局所コホモロジー層 \(\mathcal H^i_Z(\Lambda)\) は \(i = 2c\) 以外で消え、\(\mathcal H^{2c}_Z(\Lambda) \cong \Lambda(-c)\)（コホモロジー的純粋性）。ここで \(\Lambda(r) = \mu_{\ell^m}^{\otimes r}\) は Tate ひねりである。

5. 消滅定理

\(X\) を \(k\) 上有限型で次元 \(d\) とする。

\[ H^i(X_{\mathrm{ét}}, \mathcal F) = 0\quad (i > 2d),\qquad X \text{ アフィンなら } H^i(X_{\mathrm{ét}}, \mathcal F) = 0\quad (i > d). \]

後者が Artin の消滅定理で、アフィン多様体が \(d\) 次元 CW 複体のホモトピー型を持つという Andreotti–Frankel の定理の代数版である。

6. ポアンカレ双対と Künneth

\(X\) を \(k\) 上スムーズで次元 \(d\) とする。跡写像 \(H^{2d}_c(X, \Lambda(d)) \to \Lambda\) があり、次のペアリングは完全である。

\[ H^i(X_{\mathrm{ét}}, \Lambda) \times H^{2d-i}_c(X_{\mathrm{ét}}, \Lambda(d)) \longrightarrow H^{2d}_c(X_{\mathrm{ét}}, \Lambda(d)) \xrightarrow{\ \mathrm{tr}\ } \Lambda. \]

また \(X, Y\) が固有なら Künneth 公式 \(H^n(X \times Y) \cong \bigoplus_{i+j=n} H^i(X) \otimes H^j(Y)\) が成り立つ。Tate ひねり \((d)\) が現れるのが、位相幾何との唯一の違いである。

7. ℓ 進コホモロジーと Lefschetz 跡公式

有限係数を極限で束ねると \(\ell\) 進コホモロジーになる。

\[ H^i(X, \mathbb Z_\ell) := \varprojlim_m H^i(X_{\mathrm{ét}}, \mathbb Z/\ell^m),\qquad H^i(X, \mathbb Q_\ell) := H^i(X, \mathbb Z_\ell)\otimes_{\mathbb Z_\ell}\mathbb Q_\ell. \]

\(X_0\) を \(\mathbb F_q\) 上の分離有限型スキーム、\(X = X_0 \otimes \bar{\mathbb F}_q\)、\(F\) を Frobenius とする。Grothendieck–Lefschetz 跡公式：

\[ \#X_0(\mathbb F_{q^n}) \;=\; \sum_{i=0}^{2d} (-1)^i\, \operatorname{Tr}\bigl(F^n \,\big|\, H^i_c(X, \mathbb Q_\ell)\bigr). \]

有理点の個数が、コホモロジー上の Frobenius の跡で書ける。トポロジーの Lefschetz 固定点定理の類似で、「Frobenius の固定点 = \(\mathbb F_q\)-有理点」という観察がすべての出発点である。

8. Weil 予想（Deligne, 1974）

\(X_0\) を \(\mathbb F_q\) 上スムーズ射影的で次元 \(d\) とする。ゼータ関数は跡公式から

\[ Z(X_0, t) = \prod_{i=0}^{2d} \det\bigl(1 - F t \,\big|\, H^i(X, \mathbb Q_\ell)\bigr)^{(-1)^{i+1}} = \frac{P_1(t) P_3(t)\cdots P_{2d-1}(t)}{P_0(t) P_2(t) \cdots P_{2d}(t)} \]

と有理関数になり（有理性）、ポアンカレ双対から関数等式 \(Z(X_0, 1/(q^d t)) = \pm q^{d\chi/2} t^{\chi} Z(X_0, t)\) が出る。そして Deligne の定理：

\[ P_i(t) \in \mathbb Z[t],\qquad P_i(t) = \prod_j (1 - \alpha_{ij} t),\qquad |\alpha_{ij}| = q^{i/2}\ \text{（すべての複素埋め込みで）}. \]

Frobenius の固有値の絶対値がちょうど \(q^{i/2}\)。これが「有限体上のリーマン予想」で、\(P_i\) の次数が \(X_0\) の複素持ち上げのベッチ数に一致する（比較定理）。エタール・コホモロジーは、この一連の予想を証明するために設計された道具であり、20 年かけてその目的を達した。

形式化の距離感

これらを Lean で述べるのに何が足りないかを書いておく。定理 1 にはガロア群の連続コホモロジー、定理 2 には複素解析空間と特異コホモロジー、定理 3–6 には高次順像 \(R^i f_*\)、コンパクト台コホモロジー \(H^i_c\)、構成可能層、Tate ひねり、跡写像、定理 7–8 には射影極限・Frobenius 作用・\(\ell\) 進層が要る。定義（18章）から主定理までの距離は、可換環から定義までの距離より、おそらく一桁長い。それでも、定義が機械で書けたことは、その道の最初の一歩が確定したことを意味する。

参照した文献: J. S. Milne, Lectures on Étale Cohomology (v2.21) · Stacks Project, Étale Cohomology · Stacks Project, Étale Morphisms of Schemes · P. Deligne, La conjecture de Weil I (英訳) · nLab: proper base change theorem · Encyclopedia of Mathematics: Étale cohomology · Grothendieck trace formula

21 — MATHLIB

Mathlibにあるもの、ないもの

最後に、実務の話をする。このノートは Mathlib を使わずに書いたが、Mathlib（2026年9月時点の master）には、ここで手書きした概念のほぼすべてが、はるかに一般的な形で入っている。対応表を付けておく。

だから、Mathlib の上でなら、エタール・コホモロジーの定義は次の数行になる。

import Mathlib
open CategoryTheory AlgebraicGeometry

/-- `X` 上のエタール層: 小エタールサイト上の、アーベル群の層。 -/
abbrev EtaleSheaf (X : Scheme.{u}) := Sheaf X.smallEtaleTopology Ab.{u}

/-- エタール・コホモロジー。定数層 `ℤ` からの `n` 次 Ext 群。 -/
noncomputable def etaleCohomology (X : Scheme.{u}) (F : EtaleSheaf X) (n : ℕ) : Type u :=
  F.H n

このノートの1000行と、この数行は、同じ対象を指している。違いは、Mathlib 版が数万行のライブラリに依存していて、その中で「十分な入射的対象の存在」「Ext の良定義性」などがすべて証明済みだという点である。このノートで sorry にした定理は、Mathlib では定理として埋まっている。一方で Mathlib にもまだないものがある。比較定理、固有基底変換、ポアンカレ双対、跡公式、Weil 予想。Mathlib の \(\ell\) 進コホモロジーのファイル冒頭には「古典的なエタール・コホモロジーによる定義との比較は今後の課題」と書かれている。

自分の中では、こう整理している。定義を自分の手で書くのは「理解」のため、Mathlib を使うのは「先へ進む」ためである。両方見たときに初めて、ライブラリの一行が何を圧縮しているかがわかる。そして、次に形式化されるべき定理が何か（おそらく固有基底変換）も見えてくる。

22 — POSTSCRIPT

蛇足

このノートを書いて一番印象に残ったのは、「定義の依存関係を機械に確認させる」という作業が、思ったより数学の理解そのものだったことである。たとえば「層の完全性は局所的に定義しなければならない」という事実は、教科書で読んだときは技術的な注意に見えたが、Lean で書くと「層化を定義していないので、像の層が作れない。どう書く？」という切迫した問題として現れ、被覆による定式化に自然に到達した。定義を書くことが、定義を選ぶことになる。

もう一つ。78 個の sorry のうち、本物の定理は十数個で、残りは routine な検証である。数学の教科書が「容易に確かめられる」と書く箇所の総量が、ここで初めて数値になった。それは思ったより多く、そして思ったより本当に routine だった。

次にやりたいのは、このファイルの sorry を Mathlib の定理で埋めていくことである。自前の Scheme と Mathlib の Scheme の間に関手を作り、自前の etaleCohomology が Sheaf.H と同型であることを示す。それができれば、このノートの「セルフコンテインド」と Mathlib の「証明済み」が繋がる。どこまで行けるかは、まだよくわからない。