依存直積型
表記
Leanでは以下のように表記する
(a : α) × β a
Σ a : α, β a
$ \Sigma_n:\mathrm{Nat}.A^n
Leanでの(n : Nat) × A^nと同じ
具体例
具体的に書き出してみるとわかりやすい
普通の集合$ Aがある
$ A=\{x,y,z\}
また、$ Aに依存するような集合$ B(a)を以下のように定める
$ B(x)=\{1,2\}
$ B(y)=\{\mathrm{True},\mathrm{False}\}
$ B(z)=\{\heartsuit,\clubsuit\,\spadesuit\}
このとき、依存直積$ (a:A)\times B(a)は以下のようになる
$ \{(x,1),(x,2),(y,\mathrm{True}),(y,\mathrm{False}),(z,\heartsuit),(z,\clubsuit),(z,\spadesuit)\}
従って、$ \Sigmaを使って、
$ \sum_{a\in A} B(a)と表記する
これは、なぜ「依存直積型」なのに「Σ」を使うのかという疑問に答えている
Leanの表記の
(a : A) × B aや
Σ a : A, B aの意味もわかる
本当は↑Leanでも表現できるような具体例を書きたかったが、色々知識不足過ぎて無理なので諦めたmrsekut.icon
上記の例だと(a : A) × B aとした時、
B aはaに依存した直積になっているが、
(a : A) × Cのような直積は、
通常の直積A × Cと同じである
以下2つは同じ意味
code:lean
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a b
ちなみに前者の記号⟨は、\<とか\langleで出せるmrsekut.icon