正本：FormalLab/CategoryTheory/InitialAndTerminal.lean

第42章：始対象と終対象——零項の普遍性#

空型に要素はなく、単位型には一つだけ要素があります。しかし圏論は要素数を直接数えず、他の対象との射だけで同じ特徴を表します。空型からは任意の型へただ一つ関数があり、任意の型から単位型へもただ一つ関数があります。この「任意の相手に対する存在と一意性」が、始対象と終対象の最初の普遍性です。

本章ではまだ一般の圏をLeanで定義せず、型を対象、関数を射とする Type の圏で普遍性の論理的な骨格を取り出します。内部表現から、射による特徴づけへ視点を移します。そこで現れる「データ、方程式、一意な媒介射」は、後の普遍構成でも反復されます。具体的には積・余積、一般の圏、表現可能関手で再び現れます。

全ての対象との一意な射で特徴づける#

圏 𝒞 の対象 I が始対象、T が終対象であることを

I\;\text{が始対象} \quad\Longleftrightarrow\quad \forall A\in\mathrm{Ob}(\mathcal C).\,\exists!f:I\to A,

T\;\text{が終対象} \quad\Longleftrightarrow\quad \forall A\in\mathrm{Ob}(\mathcal C).\,\exists!g:A\to T.

と書きます。型を対象、関数を射とみなす圏では、型 I が対象 A に対して始的であるとは、 I → A が一意に存在することです。型 T が A に対して終的であるとは、 A → T が一意に存在することです。

この見方では、型の内部を直接調べる代わりに、他の型との関数空間によって特徴づけます。圏論でいう対象は点、射は向き付きの関係ではなく合成できる写像です。この章では恒等関数と関数合成を持つ「型と関数」の世界だけを扱い、一般の圏の構造体はまだ導入しません。

ここでは宇宙サイズの問題を隠さないため、「全ての型を集めた圏」をまだ定義せず、対象 A ごとの性質 IsInitialAt I A と IsTerminalAt T A を定義します。全対象についてこの性質を持つことが、圏論での始対象・終対象です。

Leankernel-checked counterpartL47–51

namespace FormalLab.CategoryTheory.InitialAndTerminal

universe u v

open FormalLab.Logic.Equality

固定した相手に対する一意な関数を定義する#

ExistsExactlyOne を展開すると、始性の証明には次の三成分が必要です。

標準射 chosen : I → A。
その射が要求された条件を満たす証明。この章では条件が True なので自明。
任意の別の射 f : I → A が chosen と等しいという一意性。

「射が一つ以下」だけでも「少なくとも一つ」だけでも足りません。普遍性では存在と一意性を分けて確認します。

I から A への関数がただ一つ存在する、という相対的な始性です。

Leankernel-checked counterpartL67–68

def IsInitialAt (I : Type u) (A : Type v) : Prop :=
  ExistsExactlyOne (fun _ : I → A => True)

A から T への関数がただ一つ存在する、という相対的な終性です。

Leankernel-checked counterpartL71–72

def IsTerminalAt (T : Type u) (A : Type v) : Prop :=
  ExistsExactlyOne (fun _ : A → T => True)

指定した対象宇宙の全型に対する始性です。

Leankernel-checked counterpartL75–76

def IsInitial (I : Type u) : Prop :=
  ∀ A : Type v, IsInitialAt I A

指定した対象宇宙の全型に対する終性です。

Leankernel-checked counterpartL79–80

def IsTerminal (T : Type u) : Prop :=
  ∀ A : Type v, IsTerminalAt T A

空型は始的である#

Empty → A の関数定義で入力を受け取っても、入力の構成子は一つもありません。そのためどの A に対しても分岐なしで関数を定義できます。一意性も同じ理由から、二つの関数を各入力で比較する場面そのものがありません。

空型から任意の型への関数。処理すべき入力構成子はありません。

Leankernel-checked counterpartL91–92

def fromInitial (A : Type v) : Empty → A :=
  fun impossible => nomatch impossible

空型から A への任意の関数は標準関数と等しい。

Leankernel-checked counterpartL95–97

theorem fromInitialUnique (A : Type v) (f : Empty → A) : f = fromInitial A := by
  funext impossible
  exact nomatch impossible

Empty から固定した任意の対象 A への射は一意に存在します。

Leankernel-checked counterpartL100–101

theorem emptyIsInitialAt (A : Type v) : IsInitialAt Empty A :=
  ⟨fromInitial A, True.intro, fun f _ => fromInitialUnique A f⟩

Empty は指定した宇宙の全ての型に対して始的です。

Leankernel-checked counterpartL104–105

theorem emptyIsInitial : IsInitial Empty :=
  fun A => emptyIsInitialAt A

単位型は終的である#

A → Unit では入力はいくつあっても、出力候補は () 一つだけです。存在は全入力を () へ送る関数で示し、一意性は任意の関数の出力 f x : Unit を場合分けすると () しかないことから示します。始性では始域の空性、終性では終域の一点性が、一意な関数という同じ外部的条件へ現れます。

任意の型から単位型へ、全入力を唯一の構成子へ送ります。

Leankernel-checked counterpartL117–118

def toTerminal (A : Type v) : A → Unit :=
  fun _ => ()

A から単位型への任意の関数は標準関数と等しい。

Leankernel-checked counterpartL121–124

theorem toTerminalUnique (A : Type v) (f : A → Unit) : f = toTerminal A := by
  funext x
  cases f x
  rfl

固定した任意の対象 A から Unit への射は一意に存在します。

Leankernel-checked counterpartL127–128

theorem unitIsTerminalAt (A : Type v) : IsTerminalAt Unit A :=
  ⟨toTerminal A, True.intro, fun f _ => toTerminalUnique A f⟩

Unit は指定した宇宙の全ての型に対して終的です。

Leankernel-checked counterpartL131–132

theorem unitIsTerminal : IsTerminal Unit :=
  fun A => unitIsTerminalAt A

`Type` における実例と一般の圏#

空型から関数を作れることは、空型の値を作れたという意味ではありません。単位型への関数が一意であることは、始域が一点だという意味でもありません。どちらも関数空間の一意性です。また始対象・終対象は一般に文字通り同じ対象ではなく、矢印を反転することで交換される双対な概念です。

一般の圏では始対象や終対象が文字どおり一つの内部表現に決まるとは限りません。しかし二つの始対象があれば、その普遍性から両方向の一意な射が生じ、合成は一意性によって恒等射になるため一意な同型が得られます。「一意」は通常、等号による一意性ではなく一意な同型を除く一意性です。

要点#

普遍性は対象の内部表現より、他の対象との射の存在と一意性で対象を特徴づける。
始対象から任意の対象へは一意な射が出て、任意の対象から終対象へは一意な射が入る。
Empty の始性は入力がないこと、Unit の終性は出力候補が一つであることに由来する。
始対象と終対象はすべての矢印を反転すると交換される双対概念である。
普遍対象の一意性は、一般には一意な同型を除く一意性である。

研究史と文献案内#

Eilenberg–Mac Laneの1945年論文 [EM45] は、圏・関手・自然同値を体系的に導入しました。ただし、現在の教科書的な普遍性の全体系を同論文へ帰属させることはできません。始・終対象と普遍構成を現代の記法で学ぶには [LEI14]、標準的な研究語彙は [MAC98]、型理論・論理との接続は [LS86] を参照してください。

問題#

存在一意性を型のデータへ分解する#

IsInitialAt I A を展開し、各対象 A への射、満たす条件、その射の一意性を区別せよ。関数の圏における Empty について fromInitial を構成し、この関数が Empty の項を作っているのではなく、存在しない入力を除去していることを説明する。

同様に Unit への射を構成し、fromInitialUnique と toTerminalUnique がそれぞれ空性と一点性をどこで使うかを比較せよ。対象の要素数と、その対象を始域・終域とする射の一意性を混同しないこと。

普遍対象の一意性を導く#

二つの始対象 I と J を仮定し、普遍性から I ⟶ J と J ⟶ I を得よ。二つの合成が各恒等射に等しいことを、射の具体的定義ではなく一意性だけから示す。これにより始対象が一意な対象ではなく、一意な同型を除いて一意であることを導け。

同じ議論を終対象へ双対化し、どの等式で合成順序が反転するかを明記する。証明を丸ごと暗記せず、普遍性の一意性節から再構成できれば完了である。

射を反転して終性を復元する#

始性の定義に現れる全ての射を反転し、終性の式を数式で書け。反対圏という語を使う前に、対象を変えず射の向きと合成順序を変える操作として説明する。

A → Unit が一意であることから A が一点型だとは結論できない具体例を与えよ。普遍性は対象の内部要素を直接数える条件ではなく、周囲の全対象との射の配置を特徴づける条件であることを示すこと。