文献あり

ノート：トポス (1) - 初等トポスは有限余完備である

328

忙しい人向けダイジェスト

Mac Lane のⅥ章6～7節や、 MacLane-Moerdĳk のⅣ章4～5節の内容をやります。

前書き

集合論、あるいは数理論理学 (の一部断片) の圏論的実装として、初等トポス (elementary topos) と呼ばれる構造が知られています。「トポス」とは古代ギリシャ語で「場所」を意味するτόποςから来ており、トポロジー (topology/Topologie) との関連が深い (というより、語源へ逆流？) ことを示しています。

トポスは代数幾何学の巨人グロタンディーク (A. Grothendieck, 1928–2014) が層理論の研究をする中で、層や層のなす構造を一般化した結果誕生しました。圏 $C$ 上のグロタンディーク位相についての層がなす圏はグロタンディークトポスと呼ばれる構造を持ちます。
同時期に、ローヴェア (などの圏論学者) は圏論によって数学の基礎を打ち建てようと試み、その過程でトポスに注目しました ( ETCS )。ローヴェア (F. W. Lawvere) はティアニー (M. Tierney) と共に、集合論的な仮定から自由となった初等トポスを導入します。

初等トポス

圏 $\envcat$ が初等トポス (elementary topos) であるとは、 $\envcat$ が以下の条件を満たすことである。

カルテシアン閉である。すなわち、二項積 $\times$ 、その単位対象でもある終対象 $1$ 、随伴 $\envcat (A \times B, C) ≅ \envcat (A, C^{B})$ を与える関手 $(\_)^{(\_)}\colon\envcat^{\op}\times\envcat\to\envcat$ を備えている。
引き戻しを持つ。すなわち、任意の $A \overset{f}{\to} C \overset{g}{\leftarrow} B$ に対して、 $A \overset{p_{1}}{\leftarrow} P \overset{p_{2}}{\to} B$ が存在して $f p_{1} = g p_{2}$ が成り立ち (下図左)、任意の $f q_{1} = g q_{2}$ を満たす $A \overset{q_{1}}{\leftarrow} Q \overset{q_{2}}{\to} B$ に対して、 $q_{1} = p_{1} h, q_{2} = p_{2} h$ を満たす $h : Q \to P$ がただ1つ存在する (下図右)。
$Q q_{1} q_{2} P p_{2} p_{1} B g P p_{2} p_{1} B g A f C A f C$
部分対象分類子 (subobject classifier) を持つ。すなわち、ある対象 $Ω$ と射 $true : 1 \to Ω$ が存在して、任意の単射 $s : S ↪ A$ に対して次の図式を引き戻しにする $χ_{s} : A \to Ω$ がただ1つ定まる。
$S s 1 true A χ_{s} Ω$

初等トポスの例としては、小さい集合の圏 $\CSet$ 、有限集合の圏 $FinSet$ 、位相群 $G$ からの連続作用を備えた集合の圏 $G Set$ 、小さな圏 $C$ から $\CSet$ への関手圏 $\CSet^{C}$ などがあります。

初等トポスはその上で集合論および数理論理学の様々な概念を実装、模倣することができますが、ZFCの全てを実行できるほどは強くありません。例えば [MacLane-Moerdĳk] では、選択公理とNNOを備えたwell-pointed toposの理論が、RZCと呼ばれる制限されたツェルメロ公理系 (に選択公理を追加したもの) と無矛盾等価であることが示されています。

本記事の内容

本記事は以下の定理までの道のりを記述するノートです：

初等トポス $\envcat$ は有限余完備である。
（すなわち、任意の有限圏 $J$ と関手 $F : J \to \envcat$ について、 $F$ は余極限を持つ。）

初等トポスの定義は余極限について何も表明していません (二項積・引き戻し・終対象によって、有限完備であることはすぐに確認できます。本記事でも命題18で登場します)。その結果かどうかはわかりませんが、この定理を示すための道のりは険しい山道のようになっています。

定理を証明するための3つのマイルストーンを先に示しておきます。

ベック–シュバレー条件

トポス $\envcat$ において、単射 $k : B^{'} ↪ B$ から以下の図式が可換になるような射 $\exists_{k} : Ω^{B^{'}} \to Ω^{B}$ が定まる。
$E 1 true 1 true B^{'} \times Ω^{B^{'}} \in_{B^{'}} k \times \id Ω B \times Ω^{B^{'}} \id \times \exists_{k} Ω B \times Ω^{B} \in_{B} Ω$

また、関手 $\pow \colon \envcat^{\op}\to\envcat$ を $\pow X = Ω^{X}$ で定める。これを冪関手と呼ぶ (詳細は後述)。

いま、射 $m : C^{'} ↪ C$ が射 $k : B^{'} ↪ B$ の $g : C \to B$ に沿った引き戻しであるとき (下図左)、以下 (右) の図式は可換となる。
$C^{'} g^{'} m B^{'} k \pow B^{'} \exists_{k} \pow g^{'} \pow C^{'} \exists_{m} C g B \pow B \pow g \pow C$

ベックの定理 (反映対によるバージョン)

圏 $C, D$ の間に随伴 $F ⊣ G : C ⇀ D$ が存在し、 $T = G F$ を随伴による $C$ 上のモナド、関手 $K : D \to C^{T}$ をそれらについての比較関手とする。このとき、

$C$ において、射の対 $s, t : X \to Y$ が $s i = t i = \id_{Y}$ を満たすような $i : Y \to X$ を持つとき必ずコイコライザが存在するならば、 $K$ は左随伴 $L$ を持つ。
加えて、 $G$ が上記の条件を満たすコイコライザを保存するとき、随伴の単位 $\Id_{C^{T}} \Rightarrow K L$ は同型となる。
さらに加えて、 $G$ が同型を反映するならば、随伴の余単位 $L K \Rightarrow \Id_{D}$ は同型となる。すなわち、 $K$ は圏同値を与える ( $G$ はモナディックな関手である)。

初等トポス $\envcat$ において、冪関手 $\pow \colon \envcat^{\op}\to\envcat$ はモナディックである。

ベック–シュバレー条件 (Beck–Chevalley condition) がやっていることは代入と量化子 $\exists$ ( $\forall$ ) の交換 ( 参考 )、あるいはpullとpushの交換です ( 参考1 参考2 )。MacLane-Moerdĳkではトポスに対する "内部" (internal) と "外部" (external) 条件、グロタンディーク位相の引き戻し図式に対するもの、位相空間の圏における引き戻し図式に対するものが登場します。
文脈によって条件付けが変わってしまうため何度も登場してしまうのですが、引き戻しによる反変関手とその左随伴に関するとても基本的なツールであり、その結果として今回の議論でも登場します。

ベックの定理は元々、1960年代に代数とモナドの関係について調べられた中で発見されました。モナド $T : \arbcat \to \arbcat$ に対して随伴を構築する普遍的な方法として、「 $T$ -代数の圏」ことアイレンバーグ–ムーア圏と「自由 $T$ -代数の圏」ことクライスリ圏という2つの構成が存在します。そこで通常の代数の圏 (つまり $\CAb$ とか $Grp$ とか $Ring$ とか) のような圏は $T$ -代数の圏なのか？というような、代数と $T$ -代数の関係性についての疑問が生まれてきます。
ベックの定理は $T$ -代数の圏と同型あるいは圏同値となるようなものの条件(しばしば必要十分条件)を与えます。これによって例えば、代数の圏は確かに $T$ -代数の圏である (しかも同型である) ことがわかります。

これらの道具を用いることで、冪関手 $\pow$ が自身の逆 $\pow ^{\op}\colon \envcat\to\envcat^{\op}$ を左随伴に持ち、さらに $\envcat^{\op}$ は $PP$ -代数の圏と圏同値であることがわかります。 $PP$ -代数とはよい条件を満たす射 $PP A \to A$ であり、冪集合が ${0, 1}$ への射と1対1対応することと併せて考えると、これは二重否定除去 $\neg \neg φ \to φ$ に対応します。

$\pow$ がモナディックな自己反変関手であることを用いて、ようやく $\envcat$ に有限余極限がすべて備わっていることが示されます。

冪対象・順像とベック–シュバレー条件

まず、初等トポスにおいて (そして本稿の最終目標である定理においても) 重要な概念である冪対象について定義します。これは例えば集合の圏 $\CSet$ において冪集合に対応する概念です。

トポス $\envcat$ における $A \in \envcat$ の冪対象 (power object) $\pow A$ とは、射 $\in_{A} : A \times \pow A \to Ω$ を備えた $\envcat$ の対象であり、任意の $f : A \times C \to Ω$ の形の射に対して次の図式を可換にする $g : C \to \pow A$ がただ1つ定まるものをいう。
$A \times C f \id \times g A \times \pow A \in_{A} Ω$

今回、私たちは $\envcat$ に対してカルテシアン閉であることを定義に組み込んだため、冪対象が $\pow A = Ω^{A}$ であり、従ってすべての対象に対して冪対象が存在することが直ちに従います。
逆に冪対象を前提とする場合、次の事実が成り立ちます：

事実 (Theorem Ⅳ.2.1, [MacLane-Moerdĳk])

$\envcat$ が終対象・部分対象分類子・すべての引き戻し・すべての冪対象を持つとき、 $\envcat$ はすべての指数対象 $A^{B}$ を持つ。

$\pow A = Ω^{A}$ であったため、冪対象を与える対応は反変関手 $\pow : \envcat^{| \to ⟩ ⟨ \to |} \envcat$ を構成します。そこでこれを冪関手と呼ぶことにします。

トポス $\envcat$ において、単射 $k : B^{'} ↪ B$ から以下の図式が可換になるような射 $\exists_{k} : Ω^{B^{'}} \to Ω^{B}$ が定まる。これを $k$ による順像 (direct image) という。
$E m 1 true 1 true B^{'} \times Ω^{B^{'}} \in_{B^{'}} k \times \id Ω B \times Ω^{B^{'}} {}_{k}E \id \times \exists_{k} Ω B \times Ω^{B} \in_{B} Ω$
ここで、図式中の $m, χ_{E}, \exists_{k}$ は以下の通り定まる。

$m : E ↪ B^{'} \times Ω^{B^{'}}$ は $\in_{B^{'}}$ に沿った $true$ の引き戻し。
${}_{k}E : B \times Ω^{B^{'}} \to Ω$ は単射 $(k \times \id) m : E ↪ B \times Ω^{B^{'}}$ を特徴付ける射。
$\exists_{k} : Ω^{B^{'}} \to Ω^{B}$ は $χ_{E}$ から指数対象 $Ω^{B}$ についての普遍性によって定まる射。

順像と呼ぶ通り、集合の圏 $\CSet$ においては $\exists_{k} : B^{'} \supset S ⟼ k (S) = {k (x) \in B ∣ x \in S}$ という対応を構成します。また、順像 $k (S)$ の定義から
$y \in k (S) ⟺ \exists x \in S . y = k (x)$
と書けるため、順像は存在量化子 $\exists$ のシンプルな実装と見ることもできます。

\exists

に対するベック–シュバレー条件 (定理2再掲)

トポス $\envcat$ において、射 $m : C^{'} ↪ C$ が射 $k : B^{'} ↪ B$ の $g : C \to B$ に沿った引き戻しであるとき (下図左)、以下 (右) の図式は可換となる。
$C^{'} g^{'} m B^{'} k \pow B^{'} \exists_{k} \pow g^{'} \pow C^{'} \exists_{m} C g B \pow B \pow g \pow C$

冪対象の普遍性から $\envcat (\pow B^{'}, \pow B) ≃ \envcat (B \times \pow B^{'}, Ω)$ が従うが、この同型は $\exists_{k}$ の定義から $\exists_{k}$ を ${}_{k}E$ に対応させることがわかる。

示すべき図式に対してこれらの同型 ( $\exists_{k} \mapsto {}_{k}E$ , $\exists_{m} \mapsto {}_{m}E$ , $\envcat (\pow B^{'}, \pow C) ≃ \envcat (C \times \pow B^{'}, Ω)$ ) を適用すると、次の図式の可換性を証明すればよいことがわかる。
$C \times \pow B^{'} C \times \pow g^{'} g \times \pow B^{'} C \times \pow C^{'} {}_{m}E B \times \pow B^{'} {}_{k}E Ω$
2つの射 ${}_{m}E \conc (C \times \pow g^{'})$ , ${}_{k}E \conc (g \times \pow B^{'})$ それぞれについて、次のような引き戻し図式が書ける
$R r E_{C^{'}} 1 true C^{'} \times \pow B^{'} C^{'} \times \pow g^{'} m \times \pow B^{'} C^{'} \times \pow C^{'} m \times \pow C^{'} \in_{C^{'}} C \times \pow B^{'} C \times \pow g^{'} C \times \pow C^{'} {}_{m}E Ω$
$R^{'} r^{'} E_{B^{'}} 1 true C^{'} \times \pow B^{'} g^{'} \times \pow B^{'} m \times \pow B^{'} B^{'} \times \pow B^{'} k \times \pow B^{'} \in_{B^{'}} C \times \pow B^{'} g \times \pow B^{'} B \times \pow B^{'} {}_{k}E Ω$
ここで、次の図式が引き戻しになることから、 $r$ と $r^{'}$ はどちらも $true$ の $\in_{B^{'}} \conc (g^{'} \times \pow B^{'}) = \in_{C^{'}} \conc (C^{'} \times \pow g^{'})$ に沿った引き戻しであることが従う。すなわち $R ≃ R^{'}$ であり、この2つは同一視してよい。
$R ≃ R^{'} E_{C^{'}} e_{C^{'}} x E_{B^{'}} e_{B^{'}} 1 true C^{'} \times \pow B^{'} C^{'} \times \pow g^{'} x g^{'} \times \pow B^{'} C^{'} \times \pow C^{'} \in_{C^{'}} B^{'} \times \pow B^{'} \in_{B^{'}} Ω$
ここから、 ${}_{m}E \conc (C \times \pow g^{'})$ と ${}_{k}E \conc g \times \pow B^{'}$ はどちらも同じ単射を特徴付ける $C^{'} \times \pow B^{'} \to Ω$ の射であり、 $Ω$ の普遍性から両者は同じ射であることがわかる。

射 $k : B^{'} ↪ B$ がモノ射であるとき、 $\pow k \conc \exists_{k} : \pow B^{'} \to \pow B^{'}$ は単位射である。

任意のモノ射 $k : B^{'} ↪ B$ について、次の図式が引き戻しとなる。
$B^{'} \id \id B^{'} k B^{'} k B$
$\pow \id$ と $\exists_{\id}$ はどちらも単位射となるため、ベック-シュバレー条件から $\pow k \conc \exists_{k} = \exists_{\id} \conc \pow \id = \id_{\pow B^{'}}$ を得る。

$\CSet$ においてベック-シュバレー条件の主張を確認してみると、 $S \subset B^{'}$ に対して
$\begin{aligned} (\exists_{m} \conc \pow g^{'}) (S) & = {m (x^{'}) \in C ∣ x^{'} \in \pow g^{'} (S)} \\ = {m (x^{'}) \in C ∣ g^{'} (x^{'}) \in S} \\ (\pow g \conc \exists_{k}) (S) & = {x \in C ∣ g (x) \in \exists_{k} (S)} \\ = {x \in C ∣ \exists y \in S . k (y) = g (x)} \end{aligned}$
という2つの集合を得ます。 $g \conc m = k \conc g^{'}$ であることから、 $x \in (\exists_{m} \conc \pow g^{'}) (S) ⟶ x \in (\pow g \conc \exists_{k}) (S)$ は簡単に確認できます。
一方、その逆は非自明です。特に、 $x \in C$ について、
$\exists y \in S . k (y) = g (x) ⟹ \exists x^{'} \in C^{'} . x = m (x^{'})$
であることは $k, m$ の単射性を必要とするため、これが $\CSet$ におけるベック-シュバレー条件の肝であることが伺えます。

随伴の比較とベックの定理

ベックの定理は関手がモナディックであるための条件を与えます。モナディックであることを定義するために、随伴とモナドの定義から始めていきます。

とはいえ随伴はそれだけでどの入門書でも1章は費やすほどの重要概念なので、詳しい説明はそれら入門書に譲ることとします。

圏 $\arbcat$ , $D$ とその間の関手 $L : \arbcat \to D$ , $R : D \to \arbcat$ について、 $L$ が $R$ の左随伴 (left adjoint) である ( $R$ が $L$ の右随伴 (right adjoint) である) とは、以下の同値な条件を満たすことである。

集合としての同型 $φ_{x, y} : D (L x, y) ≃ \arbcat (x, R y)$ が存在して、 $x \in \arbcat$ , $y \in D$ それぞれに対して自然である。
自然変換 $\uni : \Id_{\arbcat} \Rightarrow R L$ が存在して、各 $\uni_{x} : x \to R L x$ が $x$ から $R$ への普遍射である。
自然変換 $\couni : L R \Rightarrow \Id_{D}$ が存在して、各 $\couni_{y} : L R y \to y$ が $L$ から $y$ への普遍射である。
自然変換 $\uni : \Id_{\arbcat} \Rightarrow R L$ と $\couni : L R \Rightarrow \Id_{D}$ が存在して、 $\couni L \conc L \uni = \id_{L}$ と $R \couni \conc \uni R = \id_{R}$ が成り立つ。

$\uni$ を随伴の単位 (unit)、 $\couni$ を随伴の余単位 (counit) という。また、 $L$ が $R$ の左随伴であることを $L ⊣ R$ や $L ⊣ R : \arbcat ⇀ D$ で表す。

圏 $\arbcat$ 上のモナドとは、関手 $T : \arbcat \to \arbcat$ と自然変換 $μ : T T \Rightarrow T$ , $\uni : : \Id_{\arbcat} \Rightarrow T$ の3つ組で、以下の条件を満たすものをいう。

$μ \conc T μ = μ \conc μ T : T^{3} \Rightarrow T$
$μ \conc T η = μ \conc η T = \id_{T} : T \Rightarrow T$
$T T T x T μ_{x} μ_{T x} T T x μ_{x} T x T η_{x} η_{T x} T T x μ_{x} T T x μ_{x} T x T T x μ_{x} T x$

恒等関手はモナドの自明な例である。このとき、 $μ$ と $η$ はどちらも自明な自然変換であり、従ってモナドが満たすべき条件もすべて満たされる。
$\CSet$ 上の関手 $L : A \mapsto ∐_{n = 0}^{\infty} A^{n}$ について考える。このとき、 $L A$ の要素 $a \in L A$ とは $A$ の要素の有限列 $a = (a_{1}, \dots, a_{n})$ (長さ0の列 $()$ を含む) である。このとき、 $μ$ を有限個の有限列の連結 $((a_{11}, \dots, a_{1 l_{1}}), \dots, (a_{n 1}, \dots, a_{n l_{n}})) \mapsto (a_{11}, \dots, a_{1 l_{1}}, \dots, a_{n 1}, \dots, a_{n l_{n}})$ 、 $\uni$ を長さ1の列への対応 $a \mapsto (a)$ とすると、 $\CSet$ 上の関手 $L$ はモナドとなる。これはプログラミングにおけるListモナドに対応する。
$\CSet$ 上の関手 $M : A \mapsto 1 + A = {⊥} ⊔ A$ について考える。このとき、 $\uni_{A} : A \to M A$ は直和への埋め込み、 $μ_{A} : M M A \to M A$ を ( $M M A = {⊥_{1}} ⊔ {⊥_{2}} ⊔ A$ として)
$\begin{aligned} μ_{A} : ⊥_{1} & ⟼ ⊥ \\ ⊥_{2} & ⟼ ⊥ \\ (A ∋) a & ⟼ a \end{aligned}$
で定めると、 $M$ はモナドとなる。これはMaybeモナドに対応する。

随伴 $L ⊣ R : \arbcat ⇀ D$ に対して、 $T = R L$ とすると、 $T$ は $\arbcat$ 上のモナドを構成する。

$μ = R \couni L$ とおく。このとき、 $μ \conc T μ = μ \conc μ T = R \couni \couni L$ が成り立つ。また、
$\begin{aligned} μ \conc T η & = R \couni L \conc R L η \\ = R (\couni L \conc L η) \\ = R (\id_{L}) \\ = \id_{T} \\ μ \conc η T & = R \couni L \conc η R L \\ = (R \couni \conc η R) L \\ = (\id_{R}) L \\ = \id_{T} \end{aligned}$
以上より $(T = R L, μ = R \couni L, η)$ はモナドである。

$A$ を $Ring$ や $Grp$ 、 $Monoid$ のような代数の圏とする。このとき、忘却関手 $U : (A, \dots) \mapsto A$ は左随伴を持ち、それは自由関手と呼ばれる。この随伴関係は自由–忘却随伴 (free-forgetful adjunction) などと呼ばれることもある。
上述の定理から、自由代数の底集合を取る操作 $T = U F$ はモナドになる。

随伴からモナドを構成することは比較的単純ですが、逆にモナドから随伴を作ることはそれほど単純ではありません。モナドから随伴を作る普遍的な方法は2種類知られていますが、今回は「 $T$ -代数の圏」とも表現されるアイレンバーグ–ムーア圏のみに注目します。アイレンバーグ–ムーア圏の構成には $T$ -代数が必要なので、 $T$ -代数とその間の射から定義します。

$T : \arbcat \to \arbcat$ は $\arbcat$ 上のモナドとする。このとき、 $T$ -代数 ( $T$ -algebra) とは、 $\arbcat$ の対象 $A \in \arbcat$ と射 $α : T A \to A$ の組で、以下の条件を満たすものである。

$α \conc T α = α \conc μ_{A} : T T A \to A$
$α \conc η_{A} = \id_{A} : A \to A$

$T$ -代数 $(A, α), (B, β)$ に対して、 $T$ -代数の射 (準同型) $f : (A, α) \to (B, β)$ とは、 $\arbcat$ の射 $f : A \to B$ であって、次の図式を可換にするものである。
$T A T f α T B β A f B$

図式を並べて接続することで、 $T$ -代数の射の合成が定義でき、また恒等射は明らかに $T$ -代数の恒等射となるため、これによって $T$ -代数は圏をなすことがわかります。

$\arbcat$ 上のモナド $T : \arbcat \to \arbcat$ について、 $T$ のアイレンバーグ–ムーア圏 (Eilenberg-Moore category) $\arbcat^{T}$ とは、 $\arbcat$ 上の $T$ -代数とその間の射すべてからなる圏である。

任意の $A \in \arbcat$ に対して、 $μ_{A} : T T A \to T A$ は定義から $T$ -代数になります。また、任意の $T$ -代数は $\arbcat$ の対象を構成要素に持っているため、 $T$ -代数から $\arbcat$ の対象を取り出すことができます。
これらの対応を $F^{T} : A \mapsto (T A, μ_{A})$ , $U^{T} : (A, α) \mapsto A$ で表すことにすると、これらはそのまま圏の間の関手 $F^{T} : \arbcat \to \arbcat^{T}$ , $U^{T} : \arbcat^{T} \to \arbcat$ になって、さらに $U^{T} F^{T} = T$ であることが従います。

$F^{T}$ は $U^{T}$ の左随伴。

$T$ -代数の定義から、 $A = (A, α) \in \arbcat^{T}$ に対して $α \conc T α = α \conc μ_{A}$ であるが、この等式から $α$ が $\arbcat^{T}$ の射 $α : (T A, μ_{A}) \to (A, α)$ となることが従う。これを $\couni_{A} = α$ で表すと、

$\begin{aligned} \couni_{F^{T} A} \conc F^{T} \uni_{A} & = \couni_{T A} \conc F^{T} \uni_{A} \\ = μ_{A} \conc F^{T} \uni_{A} \\ = \id_{F^{T} A} \\ U^{T} \couni_{A} \conc \uni_{U^{T} A} & = α \conc \uni_{U^{T} A} \\ = \id_{U^{T} A} \end{aligned}$
従って、 $F^{T} ⊣ U^{T}$ である。

随伴 $L ⊣ R : \arbcat ⇀ D$ に対して、 $T = R L$ とする。このとき、ある関手 $K : D \to \arbcat^{T}$ が存在して、
$K L = F^{T}, R = U^{T} K$
$D K D K R \arbcat L F^{T} \arbcat \arbcat^{T} \arbcat^{T} U^{T}$
が成り立つ。
この $K$ を ( $L$ と $F^{T}$ の) 比較関手という。

$y \in D$ に対して、
$R \couni_{y} : R L R y \to R y$ は $T$ -代数となる。
そこで $K y = (R y, R \couni_{y})$ とすると、この等式は $y$ に対して自然であることから $K$ が関手として定義できることが従う。

定義から $K L = F^{T}$ と $R = U^{T} K$ も従うことがわかる。

余談

モナド $T : \arbcat \to \arbcat$ から随伴を構成するもう一つの方法であるクライスリ圏 $\arbcat_{T}$ についても同様に、随伴 $F_{T} ⊣ U_{T} : \arbcat \to \arbcat_{T}$ が存在して、任意の随伴 $L ⊣ R : \arbcat ⇀ D$ に対して、 $L = K^{'} F_{T}$ かつ $R K^{'} = U_{T}$ が成り立つような $K^{'} : \arbcat_{T} \to D$ が存在することが言えます (比較関手の方向に関して、 $\arbcat^{T}$ と双対の関係にあります)。

前書きでも軽く触れましたが、通常「代数」と呼ばれるもの、すなわち、集合の上にいくつかの演算と満たすべき等式が定まった構造と、あるモナド $T$ による $T$ -代数はその定義や構成方法に違いがあり、同じものを指しているかどうか (現段階では) 明らかではありません。

通常の代数には自由関手と忘却関手による随伴が存在するので、それが関連するモナドのアイレンバーグ–ムーア圏と「十分に同じ」かどうかを計る性質がモナディック (monadic)、古い言い方で tripleable と呼ばれるものです。

関手 $U : A \to \arbcat$ がモナディック (monadic) であるとは、 $U$ が左随伴 $F : \arbcat \to A$ を持ち、比較関手 $K : A \to \arbcat^{T}$ が圏同値であることを言う。

圏 $\arbcat$ の射 $f, g : A \to B$ , $q : B \to Q$ が $q \conc f = q \conc g$ を満たすとします。 $q^{'} \conc f = q^{'} \conc g$ を満たす任意の $q^{'} : B \to Q^{'}$ に対して、 $q^{'} = h \conc q$ を満たす射 $h : Q \to Q^{'}$ がただ1つ存在するとき、 $q$ は $(f, g)$ のコイコライザ (coequalizer) であるといいます。
$A f g B q q^{'} Q h Q^{'}$

コイコライザは集合でいえば、 $f$ と $g$ が定める $B$ 上の同値関係 ( $f (x) \sim g (x)$ で定まる関係を同値関係になるように拡張したもの) で $B$ を割った商集合にあたります。代数の場合も商代数をとる操作と関連付けられます。

ベックの定理 (あるいはその変種) において、コイコライザは重要な役割を果たします。ベックの定理を証明する前に、もう少し表記の単純な条件 (その分強まっているので使い勝手はよくない) から導かれる変種の定理でそれを確認していきます。

関手 $U : A \to \arbcat$ は左随伴 $F : \arbcat \to A$ を持つとする。このとき、 $A$ が全てのコイコライザを持つならば、比較関手 $K : A \to \arbcat^{T}$ は左随伴を持つ。

$T$ -代数 $(A, α : T A \to A)$ に対して、コイコライザ
$F U F A \couni_{F A} F α F A q_{α} L_{α}$
を取る。 $T$ -代数の射 $f : (A, α) \to (B, β)$ に対して、 $f \conc α = β \conc T f$ と $\couni$ の自然性から次の図式が可換になり、コイコライザの普遍性から射 $L_{α} \to L_{β}$ をただ1つ得る。
$F U F A \couni_{F A} F α F U F f F A q_{α} F f L_{α} F U F B \couni_{F B} F β F B q_{β} L_{β}$
ここから、 $L$ が関手であることが従う。

$\arbcat^{T}$ の射 $g : (A, α) \to (U B, U \couni_{B})$ に対して、次の図式を考える。
$F U F A \couni_{F A} F α F U F g F U g^{♯} F A q_{α} F g g^{♯} L (A, α) f F U F U B F U \couni_{B} F U B \couni_{B} B$
ただし $g^{♯} = \couni_{B} \conc F g : F A \to B$ である。このとき、
$\begin{aligned} g^{♯} \conc \couni_{F A} & = \couni_{B} \conc F U g^{♯} \\ = \couni_{B} \conc F U \couni_{B} \conc F U F g \\ = \couni_{B} \conc F g \conc F α \\ = g^{♯} \conc F α \end{aligned}$
が成り立つため、コイコライザの普遍性から $g^{♯} = f \conc q_{α}$ を満たす $f$ の存在が言える。

$f : L (A, α) \to B$ は $g^{♯} : F A \to B$ と1対1対応し、また $g^{♯}$ と $g : A \to U B$ は随伴より定まる1対1対応なので、これにより集合の同型 $A (L (A, α), B) ≃ \arbcat^{T} ((A, α), K B)$ が言えて、構成から明らかにこの同型は $A, B$ について自然。

以上より $L ⊣ K$ である。

関手 $U : A \to \arbcat$ が $T : J \to A$ のコイコライザを保存するとは、 $A$ の射 $f, g : A \to B$ にコイコライザ $q : B \to Q$ が存在するとき、 $U q : U B \to U Q$ がふたたび $U f, U g$ のコイコライザになることを言います。

関手 $U : A \to \arbcat$ は左随伴 $F : \arbcat \to A$ を持つとする。 $A$ が全てのコイコライザを持ち、加えて $U$ が全てのコイコライザを保存するとき、比較関手を右随伴とする随伴 $L ⊣ K$ の単位は同型となる。

$A$ が全てのコイコライザを持つため、比較関手 $K$ は左随伴を持つ (補題9)。随伴の単位を $\uni^{'} : \Id_{\arbcat^{T}} \To K L$ とすると、これは補題9で示した方法で恒等射に移るので、 $\arbcat$ 上で次の図式が可換になる。
$A \uni_{A} U^{T} \uni_{A}^{'} U F U F A U \couni_{F A} U F α U F A U q_{α} U ((U^{T} \uni_{A}^{'})^{♯}) U L (A, α) \id U L (A, α)$
ここで、 $g^{♯} = \couni_{B} \conc F g : F A \to B$ に対して $g = U (g^{♯}) \conc \uni_{A}$ であることを用いている。

いま、 $U q_{α} = U^{T} \uni_{A}^{'} \conc α$ であることが、
$\begin{aligned} U^{T} \uni_{A}^{'} \conc α & = U q_{α} \conc \uni_{A} \conc α \\ = U q_{α} \conc T α \conc \uni_{T A} \\ = U q_{α} \conc μ_{A} \conc \uni_{T A} \\ = U q_{α} \end{aligned}$
から従う (次の図式も参照)。
$U F A α \uni_{U F A} A \uni_{A} U^{T} \uni_{A}^{'} U F U F A U \couni_{F A} = μ_{A} U F α = T α U F A U q_{α} U L (A, α)$

$U$ はコイコライザを保存するため、 $U L (A, α)$ は $(U \couni_{F A}, U F α)$ のコイコライザである。従って、 $α \conc \uni_{A} = \id_{A}$ とコイコライザの普遍性から、 $U^{T} \uni_{A}^{'}$ は同型となる。 $q_{α}$ は $T$ -代数の射であったので、 $U^{T} q_{α}$ の同型から $q_{α}$ の同型が従う。

関手 $U : A \to \arbcat$ がコイコライザを反映するとは、 $A$ における次のような射の組 $(f, g, q)$
$A f g B q Q$
において、 $U q$ が $(U f, U g)$ のコイコライザである時には、必ず $q$ が $(f, g)$ のコイコライザであることをいいます。

(Beck)

関手 $U : A \to \arbcat$ は左随伴 $F : \arbcat \to A$ を持つとする。 $A$ が全てのコイコライザを持ち、加えて $G$ が全てのコイコライザを保存して反映するならば、 $G$ はモナディックである。

補題9, 10より、比較関手 $K : A \to \arbcat^{T}$ は左随伴を持ち、随伴の単位 $\uni^{'} : \Id_{\arbcat^{T}} \Rightarrow K L$ は同型となる。

随伴の余単位 $\couni^{'} : L K \To \Id_{A}$ について、各コンポーネント $\couni_{X}^{'} : L K X \to X$ は次の図式のように定まる。
$F U F U X \couni_{F U X} F U \couni_{X} F U X q_{U \couni_{X}} \couni_{X} L (U X, U \couni_{X}) \couni_{X}^{'} X$

補題10の証明で示したように、 $T$ -代数を構成する $α : T A \to A$ は $\arbcat$ で $(U \couni_{F A}, U F α)$ のコイコライザである。これを $T$ -代数 $U \couni_{X} : T U X \to U X$ に適用すると、 $U \couni_{X}$ は $(U \couni_{F U X}, U F U \couni_{X})$ のコイコライザであることを得る。

仮定より $U$ はコイコライザを反映するので、 $\couni_{X}$ は $(\couni_{F U X}, F U \couni_{X})$ のコイコライザである。以上より $\couni_{X}^{'}$ が同型であることが従う。

上述の定理11はベック (Jon Beck) が1968年に初めて定理を発表した時に、「粗いモナド化可能性定理」(Crude triplableness theorem) と呼んでいたものです。通常、「 $A$ が全てのコイコライザを持つ」などの条件は強すぎるため、より弱い十分条件でモナディックであることを示す定理が様々に存在しています。

定理3で載せたものは[MacLane-Moerdĳk]の定理Ⅳ.4.2で使用されているバージョンです。ここで関手 $G : D \to \arbcat$ が同型を反映するとは、 $G f$ が同型であるならば $f$ も同型であることをいいます。

ベックの定理 (定理3再掲)

$C$ において、射の対 $s, t : X \to Y$ が $s i = t i = \id_{Y}$ を満たすような $i : Y \to X$ を持つとき必ずコイコライザが存在するならば、 $K$ は左随伴 $L$ を持つ。
加えて、 $G$ が上記の条件を満たすコイコライザを保存するとき、随伴の単位 $\Id_{C^{T}} \Rightarrow K L$ は同型となる。
さらに加えて、 $G$ が同型を反映するならば、随伴の余単位 $L K \Rightarrow \Id_{D}$ は同型となる。すなわち、 $K$ は圏同値を与える ( $G$ はモナディックな関手である)。

任意の $T$ -代数 $(A, α : T A \to A)$ に対して、 $D$ における射の組 $\couni_{F A}, F α : F U F A \to F A$ は右逆射 $F η_{A} : F A \to F U F A$ を持つ。従って、この射の組はコイコライザを持ち、以降補題9に従って左随伴 $L : \arbcat^{T} \to D$ を得る。 $L$ の単位が同型であることは補題10と同様に従う。

補題11で示した通り、 $U \couni_{X}$ は $(U \couni_{F U X}, U F U \couni_{X})$ のコイコライザである。ここで $G$ がコイコライザを保存するので、 $U \couni_{X}^{'}$ が同型であることがわかる。仮定から $G$ は同型を反映するため、 $\couni_{X}^{'}$ の同型が従う。

冪関手のモナド性

先に補題を2つほど証明します。

忠実な関手はモニック射とエピ射を反映する。すなわち、関手 $F : \arbcat \to D$ が忠実 (任意の写像 $F_{x, y} : \arbcat (x, y) \to D (F x, F y)$ が単射) であるとき、以下が成り立つ。

$\arbcat$ の射 $f : x \to y$ について、 $F f \conc g = F f \conc g^{'}$ ならば $g = g^{'}$ が $D$ において成り立つ ( $F f : F x \to F y$ がモニックである) とき、 $f$ についても $f \conc h = f \conc h^{'}$ ならば $h = h^{'}$ が成り立つ。
$\arbcat$ の射 $f : x \to y$ について、 $g \conc F f = g^{'} \conc F f$ ならば $g = g^{'}$ が成り立つとき ( $F f : F x \to F y$ がエピである) とき、 $f$ についても $h \conc f = h^{'} \conc f$ が成り立つ。

関手 $F : \arbcat \to D$ は忠実とする。

$F f$ が $D$ においてモニックであるとする。このとき、 $f \conc h = f \conc h^{'}$ ならば $F f \conc F h = F f \conc F f^{'}$ から $F h = F h^{'}$ 。さらに $F$ が忠実であるため、 $h = h^{'}$ が従う。
$F f$ が $D$ においてエピであるとする。このとき、 $h \conc f = h^{'} \conc f$ から $F h \conc F f = F h^{'} \conc F f$ より $F h = F h^{'}$ が成り立つ。さらに $F$ が忠実であるため、 $h = h^{'}$ が従う。

初等トポス $\envcat$ において、同型であることはモニックかつエピであることと同値である。

モニックかつエピであれば同型であることを示せばよい (逆は明らかである)。
いま、 $\envcat$ の射 $f : A \to B$ がモニックかつエピである。このとき、次の図式が引き戻しとなる。
$A f 1 true B χ_{f} Ω$
さらに、終対象への射は対象ごとにただ1つであるため、射 ${true}_{B} : B \to 1 \overset{true}{\to} Ω$ に対して $χ_{f} \conc f = {true}_{B} \conc f$ が成り立つ。
このとき、引き戻し図式の普遍性から $f$ は $χ_{f}$ と ${true}_{B}$ のイコライザであることが従う。

他方、 $f$ はエピであったため、 $χ_{f} \conc f = {true}_{B} \conc f$ より $χ_{f} = true$ である。同じ射の組のイコライザは同型射となるため、 $f$ は同型射である。

冪関手 $\pow$ についていくつか確認しておきます。モナド $\envcat$ に対して、冪対象は $P A := Ω^{A}$ で与えられるため、指数写像の関手性から $P$ は反変関手をなすことがわかります。冪対象の定義から、 $P f$ が次のように導出され、冪対象によってトポスを定義した場合はここから $P$ の関手性を得ます。

冪対象の定義からの導出

初等トポス $\envcat$ の射 $f : A \to B$ に対して、 $P f : P B \to P A$ が次の図式を可換にするように定まる。
$A \times P B f \times \id \id \times P f B \times P B \in_{A} A \times P A \in_{B} Ω$

冪関手がモナディックであることはベックの定理を適用することで証明できます。そのために、冪関手にベックの定理が適用可能であること（すなわち、左随伴を持つことと、定理が要求する3つの条件を満たすこと）を示す必要があります。

初等トポス $\envcat$ において、冪関手 $\pow \colon \envcat^{\op}\to\envcat$ は忠実である。

$\envcat$ の射 $f : B \to A$ に対して、 $⟨ \id, f ⟩ : B \to B \times A$ はモニックである。ここで、以下の可換図式を考える。
$B f ⟨ \id, f ⟩ A Δ_{A} 1 true B \times A f \times \id A \times A δ_{A} Ω$
ここで $Δ_{A} = ⟨ \id, \id ⟩$ は対角射、 $δ_{A}$ は $Δ_{A}$ を引き戻しにする射である。部分対象分類子の性質から、 $⟨ \id, f ⟩$ を引き戻しにする射は $δ_{A} \conc f \times \id$ であり、図式はすべて引き戻しになる。

冪対象の性質から $δ_{A}$ が定める射を ${_}_{A} : A \to \pow A$ で表す。このとき、次の図式が可換となる。
$B \times A f \times \id \id \times {_}_{A} A \times A \id \times {_}_{A} δ_{A} B \times \pow A f \times \id \id \times \pow f A \times \pow A \in_{A} B \times \pow B \in_{B} Ω$
従って、 $f, f^{'} : B \to A$ が $\pow f = \pow f^{'}$ であるとき、 $δ_{A} \conc (f \times \id) = δ_{A} \conc (f^{'} \times \id)$ であり、これに沿って $true$ を引き戻すことで最終的に $f = f^{'}$ を得る。

以上より $\pow_{A, B} : \envcat (B, A) \to \envcat (\pow A, \pow B)$ が任意の $A, B$ について単射であるため、 $\pow$ は忠実関手である。

Theorem Ⅳ.5.1, [MacLane-Moerdĳk]

冪関手 $P : \envcat^{| \to ⟩ ⟨ \to |} \envcat$ は左随伴を持ち、それは $\mathcal{P}^\op\colon\envcat\to\envcat^\op$ である。

冪対象の性質から、 $\envcat (A, P B) ≃ \envcat (A \times B, Ω) ≃ \envcat (B, P A) ≃ \envcat^{| (⟩ ⟨ (|} P A, B)$ である。従って、 $\mathcal{P}^\op\colon\envcat\to\envcat^\op$ は $P$ の左随伴である。

随伴 $P^{| ⊣ ⟩ ⟨ ⊣ |} P$ について、その単位 $\uni\colon\Id_\envcat\To\mathcal{P}\mathcal{P}^\op$ は次の図式を可換にするように定まります。
$P A \times A \sim \id \times \uni_{A} A \times P A \in_{A} P A \times PP A \in_{P A} Ω$
$P$ と $\mathcal{P}^\op$ が互いに反対であることから、随伴の余単位は $\couni_{A} = \uni_{A}^{| : ⟩ ⟨ : |} PP A \to A$ で定まります。

(定理4再掲) Theorem Ⅳ.5.3, [MacLane-Moerdĳk]

初等トポス $\envcat$ において、冪関手 $\pow \colon \envcat^{\op}\to\envcat$ はモナディックである。

ベックの定理によって証明する。まず、 $\envcat$ は二項積と引き戻しを持つため、次の引き戻しによって射の組 $f, g : A \to B$ のイコライザ $q : Q \to A$ を得る。
$Q q A ⟨ f, g ⟩ B Δ_{B} B \times B$
$\envcat$ のイコライザは $\envcat^\op$ のコイコライザであるため、 $\envcat^\op$ は全てのコイコライザを持つ。

$\envcat^\op$ におけるコイコライザの図式
$\begin{xy} \xymatrix{ A \ar@<.6ex>[r]^-{f^\op} \ar@<-.6ex>[r]_-{g^\op} & B \ar[r]^-{q^\op} & Q } \end{xy}$
であって、 $f^{| \conc ⟩ ⟨ \conc |} i^{| = ⟩ ⟨ = |} g^{| \conc ⟩ ⟨ \conc |} i^{| = ⟩ ⟨ = |} \id_{B}$ を満たすような $i^{| : ⟩ ⟨ : |} B \to A$ を備えているものについて考える。これは $\envcat$ において、 $i \conc f = i \conc g = \id_{B}$ を満たす $i : A \to B$ を備えたイコライザの図式となる。

次の図式について、
$Q q q B f B g A$
$f \conc h = g \conc h^{'}$ を満たす射 $h, h^{'} : X \to B$ について、 $i$ を後ろに合成することで $h = h^{'}$ がわかり、従って $q$ がイコライザであることから $h = h^{'} = q \conc k$ を満たす $k : X \to Q$ がただ1つ存在する。以上のことから上の図式は引き戻しである。
$q$ が $f$ と $g$ の引き戻しでもあることから、 $q$ がモニックであることが従う。

ベック-シュバレー条件より、次の図式が可換となる。
$\pow B \pow q \exists_{f} \pow Q \exists_{q} \pow A \pow g \pow B$
また、ベック-シュバレー条件の系から、 $\pow q \conc \exists_{q} = \id_{\pow Q}$ と $\pow f \conc \exists_{f} = \id_{\pow B}$ がわかる。

従って、 $\pow f, \pow g, \pow q$ は分裂フォーク (split fork) と呼ばれる図式を構成する。
このとき、 $h \conc \pow f = h \conc \pow g$ を満たすような $h : \pow B \to X$ に対して、 $h \conc \exists_{q} \conc \pow q = h$ が成り立つ。
$\pow A \pow f \pow g \pow B \pow q \exists_{f} \pow A \pow g \pow f \pow B x h \pow Q \exists_{q} \pow B h X$
また、 $k \conc \pow q = k^{'} \conc \pow q = h$ を満たす $k, k^{'} : \pow Q \to X$ は、 $\exists_{q}$ を前から合成することで $k = k^{'}$ を得る。
以上より $\pow q$ は $(\pow f, \pow g)$ のコイコライザであり、すなわち $\pow$ はコイコライザを保存する。

最後に、補題15と16から、 $\pow$ はモニック射とエピ射を反映するが、それはすなわち同型も反映することがわかる。以上より、ベックの定理によって $\pow$ がモナディックであることが従う。

分裂フォーク、およびそれのなす分裂コイコライザと呼ばれるコイコライザについてはCWMのⅥ章6節を参照。

余極限の構成

$\envcat$ が有限余完備であることは、 $\pow$ がモナディックであることを用いて、 $\envcat$ の有限完備性 $⟹$ $\envcat^{T}$ の有限完備性 $⟹$ $\envcat^\op$ の有限完備性 $⟹$ $\envcat$ の有限余完備性の順番で示されます。 $\envcat$ が有限完備であることは (有限余完備性と異なり) 初等トポスの基本的な性質です。

すべての有限積とすべてのイコライザを持つ圏はすべての有限極限を持つ。
特に、初等モナドは全ての有限極限を持つ。

$\arbcat$ はすべての有限積とイコライザを持つ圏、 $J$ は有限圏とする。
このとき、関手 $F : J \to \arbcat$ に対して、有限積 $\prod_{j \in J} F j$ と $\prod_{d : i \to j} F j$ が取れるため、次の図式における $π, τ$ とそのイコライザ $(Q, q)$ を考える。
$F j F j Q q \prod_{j \in J} F j π τ \prod_{d : i \to j} F j F i F (d : i \to j) F j$
ただし $π$ とは積の性質を用いて各 $F j$ への射影から導かれる射、 $τ$ は各 $F d : F i \to F j$ から導かれる射である。
このとき $Q \overset{q}{\to} \prod_{j \in J} F j \to F j$ によって $Q$ から $F$ への錐が構成でき、さらに任意の $F$ への $X$ からの錐は、対応する $k : X \to \prod_{j \in J} F j$ について $π \conc k = τ \conc k$ が成り立つため、 $k = q \conc k^{'}$ を満たす $k^{'} : X \to Q$ がただ1つ存在する。従って $Q$ は $F$ の極限である。

$J$ と $F$ は任意に選べたため、 $\arbcat$ は任意の有限極限を持つ。

初等モナド $\envcat$ について、終対象は0項積と思うことができるので、二項積と併せて $\envcat$ は全ての有限積を持つ。従って $\envcat$ は有限完備である。

上記の方法による完備性の証明は、まったく同じ形で任意の (小さな) 積とイコライザを持つ圏が (小) 完備であることを示す証明に書き直すことができます。特にこれにより、小さな集合の圏 $\CSet$ が小完備であることが示されます。[Mac Lane,Ⅴ.2節]

関手 $F : \arbcat \to D$ が極限を創出する (create) とは、関手 $D : J \to \arbcat$ に対して $F D : J \to D$ に極限錐 ${τ_{j} : L \to F D j}_{j \in J}$ が存在するとき、 $L = F L^{'}$ かつ $τ_{j} = F τ_{j}^{'}$ を満たす $L^{'} \in \arbcat$ と錐 ${τ_{j}^{'} : L^{'} \to D j}$ が存在して、さらにこれは $D$ の極限錐となるものをいいます。

反映と異なり、 $\arbcat$ において $D$ からの錐 (極限錐とも限らない) の存在を仮定していないことに注意してください。

圏 $\arbcat$ 上のモナド $T : \arbcat \to \arbcat$ について、忘却関手 $U^{T} : \arbcat^{T} \to \arbcat$ は極限を創出する。
すなわち、関手 $D : J \to \arbcat^{T}$ に対して $U^{T} \circ D$ が極限を持つならば、 $U^{T}$ によってその極限錐に移る $\arbcat^{T}$ 上の錐がただ1つ存在して、さらにそれは $D$ の極限錐となる。

$x \in J$ に対して $D x = (D_{x}, d_{x} : T D_{x} \to D_{x})$ とおく。 $U^{T} \conc D$ の極限錐を ${τ_{x} : L \to D_{x}}_{x \in J}$ で表すと、 $d_{x} \conc T τ_{x} : T L \to D_{x}$ が $T L$ から $U^{T} \conc D$ への錐となるため、普遍性から $λ : T L \to L$ が存在して $d_{x} \conc T τ_{x} = τ_{x} \conc λ$ である。同様に $L$ が極限であることから $λ \conc \uni_{L} = \id$ と $λ \conc T λ = λ \conc μ_{L}$ が従うため、 $(L, λ)$ は $T$ -代数である。

$d_{x} \conc T τ_{x} = τ_{x} \conc λ$ であったことから、各 $τ_{x}$ は $T$ -代数の射 $τ_{x} : (L, λ) \to D x$ である。 $τ_{x}$ は $\arbcat$ で極限錐を構成していたので、 $\arbcat^{T}$ 上で $τ_{x}$ がなす錐も極限錐となる。

(定理1再掲)

初等トポス $\envcat$ は有限余完備である。
（すなわち、任意の有限圏 $J$ と関手 $F : J \to \envcat$ について、 $F$ は余極限を持つ。）

$J$ を有限圏とする。初等トポスは有限完備であるため、任意の関手 $F : J^{| \to ⟩ ⟨ \to |} \envcat$ に対して $F$ の極限が存在する。

$T=\pow\pow^\op$ とすると、これは $\envcat$ 上のモナドとなる。定理19より忘却関手 $U^{T} : \envcat^{T} \to \envcat$ は極限を創出するため、 $\envcat^{T}$ においても任意の $F : J^{| \to ⟩ ⟨ \to |} \envcat^{T}$ に対して極限が存在する。

冪関手 $\pow$ はモナディックであったため、 $\envcat^{T}$ と $\envcat^\op$ は圏同値である。すなわち $\envcat^\op$ も任意の $F\colon\mathcal{J}^\op\to\envcat^\op$ に対する極限を持つ。

$\mathcal{J}^\op\to\envcat^\op$ に対する極限とは $J \to \envcat$ に対する余極限と同じことであるため、以上より $\envcat$ は有限余完備である。

$\envcat$ を初等トポスとする。 $\envcat$ の終対象 $1$ について、 $1$ への射として定まる $!_{\pow \pow 1} : \pow \pow 1 \to 1$ は $T (= \pow \pow^{|) ⟩ ⟨) |}$ -代数を構成する。構成から明らかに $(1,!_{\pow \pow 1})$ は $\envcat^{T}$ の終対象である。

$T$ -代数 $(1,!)$ を圏同値 $L\colon\envcat^T\to\envcat^\op$ で送ると、 $0 := L (1,!)$ は $\uni_{\pow 1}, \pow!_{\pow \pow 1} : \pow 1 \to \pow \pow \pow 1$ のイコライザとして定まる。

任意の対象 $A \in \envcat$ に対して、 $\uni_{A}$ が $\uni_{\pow \pow A}, \pow \pow \uni_{A}$ のイコライザであることから、次の図式が可換になり、射 $0 \to A$ がただ1つ定まる。
$0 q \pow 1 \uni_{\pow 1} \pow!_{\pow \pow 1} \pow!_{\pow A} \pow \pow \pow 1 \pow \pow \pow!_{\pow A} A \uni_{A} \pow \pow A \uni_{\pow \pow A} \pow \pow \uni_{A} \pow \pow \pow \pow A$

以上より、 $0$ は $\envcat$ の始対象である。

参考文献 (リンク)

Toposes, Triples, and Theories (Barr & Wells, 1985) Republished in: Reprints in Theory and Applications of Categories, No. 12 (2005)
untitled manuscript (Beck, 1968) 1968年にベックが会議で初めてtriplability theoremsを発表した時の原稿