[0034] 降下性

高次帰納的型は一価性公理の下で降下性(descent property)という著しい性質を持つ。降下性という言葉は∞トポス理論[Lurie--2009-0000]から取ったもので、余極限と有限極限を強く関連付ける性質である。

ファイバー余積の場合の降下性について説明する。少し長くなるが、ファイバー余積に関連する図式に名前を付ける。

$$i$$ を階数とする。型 $\mathord {\textnormal {\textsf {Span}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Left}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Right}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Center}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {leg-l}}}:\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Left}}}$
- $\mathord {\textnormal {\textsf {leg-r}}}:\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Right}}}$

\mathord {\textnormal {\textsf {Span}}}(i)

の要素を(階数

\(i\)

の)スパン(span)と呼ぶ。

[007K] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパンとする。型 $\mathord {\textnormal {\textsf {Cocone}}}(A):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Vertex}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}:A.\mathord {\textnormal {\textsf {Left}}}\to \mathord {\textnormal {\textsf {Vertex}}}$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}:A.\mathord {\textnormal {\textsf {Right}}}\to \mathord {\textnormal {\textsf {Vertex}}}$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}:A.\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Vertex}}}$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}:\prod _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x)=\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(A.\mathord {\textnormal {\textsf {leg-l}}}(x))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}:\prod _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x)=\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(A.\mathord {\textnormal {\textsf {leg-r}}}(x))$

\mathord {\textnormal {\textsf {Cocone}}}(A)

の要素を

\(A\)

下の余錐(cocone)と呼ぶ。

[007L] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $C:\mathord {\textnormal {\textsf {Cocone}}}(A)$ を余錐とする。関数

\mathord {\textnormal {\textsf {cmp}}}(C):A.\mathord {\textnormal {\textsf {Left}}}\mathbin {{}_{A.\mathord {\textnormal {\textsf {leg-l}}}}\smash {+}_{A.\mathord {\textnormal {\textsf {leg-r}}}}}A.\mathord {\textnormal {\textsf {Right}}}\to C.\mathord {\textnormal {\textsf {Vertex}}}

を次のように定義する。

- $x:A.\mathord {\textnormal {\textsf {Left}}}$ に対して $\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(x)$
- $y:A.\mathord {\textnormal {\textsf {Right}}}$ に対して $\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(y)$
- $z:A.\mathord {\textnormal {\textsf {Center}}}$ に対して $\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {glue}}}(z))=C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(z)\circ {(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(z))}^{-1}$

[007M] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $C:\mathord {\textnormal {\textsf {Cocone}}}(A)$ を余錐とする。型 $\mathord {\textnormal {\textsf {IsUniversal}}}(C):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsEquiv}}}(\mathord {\textnormal {\textsf {cmp}}}(C))$ と定義する。 $\mathord {\textnormal {\textsf {IsUniversal}}}(C)$ の要素があるとき、 $$C$$ は普遍余錐(universal cocone)であると言う。

降下性は「相対的な」余錐を使って説明されるので、それを導入する。

[007N] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパンとする。型 $\mathord {\textnormal {\textsf {SpanOver}}}(A):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Left}}}:A.\mathord {\textnormal {\textsf {Left}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Right}}}:A.\mathord {\textnormal {\textsf {Right}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Center}}}:A.\mathord {\textnormal {\textsf {Center}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {leg-l}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Left}}}(A.\mathord {\textnormal {\textsf {leg-l}}}(x))$
- $\mathord {\textnormal {\textsf {leg-r}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Right}}}(A.\mathord {\textnormal {\textsf {leg-r}}}(x))$

\mathord {\textnormal {\textsf {SpanOver}}}(A)

の要素を

\(A\)

上のスパンと呼ぶ。

[007O] 定義

- $\mathord {\textnormal {\textsf {Vertex}}}:C.\mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Left}}}\rbrace }B.\mathord {\textnormal {\textsf {Left}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(x))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Right}}}\rbrace }B.\mathord {\textnormal {\textsf {Right}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(x))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }B.\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\prod _{y:B.\mathord {\textnormal {\textsf {Center}}}(x)}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(y)=_{C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(x)}^{\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(B.\mathord {\textnormal {\textsf {leg-l}}}(y))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\prod _{y:B.\mathord {\textnormal {\textsf {Center}}}(x)}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(y)=_{C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(x)}^{\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(B.\mathord {\textnormal {\textsf {leg-r}}}(y))$

\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)

の要素を

\(C\)

上

\(B\)

下の余錐と呼ぶ。

相対的な余錐は対型を取ることで普通の余錐にすることができる。

[007P] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $B:\mathord {\textnormal {\textsf {SpanOver}}}(A)$ を $$A$$ 上のスパンとする。スパン $\mathord {\textnormal {\textsf {Total}}}(B):\mathord {\textnormal {\textsf {Span}}}(i)$ を次のように定義する。

- $\mathord {\textnormal {\textsf {Left}}}\equiv \sum _{x:A.\mathord {\textnormal {\textsf {Left}}}}B.\mathord {\textnormal {\textsf {Left}}}(x)$
- $\mathord {\textnormal {\textsf {Right}}}\equiv \sum _{x:A.\mathord {\textnormal {\textsf {Right}}}}B.\mathord {\textnormal {\textsf {Right}}}(x)$
- $\mathord {\textnormal {\textsf {Center}}}\equiv \sum _{x:A.\mathord {\textnormal {\textsf {Center}}}}B.\mathord {\textnormal {\textsf {Center}}}(x)$
- $\mathord {\textnormal {\textsf {leg-l}}}(x)\equiv \mathord {\textnormal {\textsf {pair}}}(A.\mathord {\textnormal {\textsf {leg-l}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),B.\mathord {\textnormal {\textsf {leg-l}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$
- $\mathord {\textnormal {\textsf {leg-r}}}(x)\equiv \mathord {\textnormal {\textsf {pair}}}(A.\mathord {\textnormal {\textsf {leg-r}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),B.\mathord {\textnormal {\textsf {leg-r}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$

[007Q] 定義

- $\mathord {\textnormal {\textsf {Vertex}}}\equiv \sum _{x:C.\mathord {\textnormal {\textsf {Vertex}}}}D.\mathord {\textnormal {\textsf {Vertex}}}(x)$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(x)\equiv \mathord {\textnormal {\textsf {pair}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(x)\equiv \mathord {\textnormal {\textsf {pair}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x)\equiv \mathord {\textnormal {\textsf {pair}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(x)$ は $\mathord {\textnormal {\textsf {pair}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$ に[002B]を適用して定義する。
- $\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(x)$ は $\mathord {\textnormal {\textsf {pair}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(x)),D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(x)))$ に[002B]を適用して定義する。

最後にカルテシアンという性質を導入する。

[007R] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $B:\mathord {\textnormal {\textsf {SpanOver}}}(A)$ を $$A$$ 上のスパンとする。型 $\mathord {\textnormal {\textsf {IsCart}}}(B):\mathcal {U}(i)$ を $(\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(B.\mathord {\textnormal {\textsf {leg-l}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(B.\mathord {\textnormal {\textsf {leg-r}}}\lbrace x\rbrace ))$ と定義する。 $\mathord {\textnormal {\textsf {IsCart}}}(B)$ の要素があるとき、 $$B$$ はカルテシアン(cartesian)であると言う。

[007S] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $B:\mathord {\textnormal {\textsf {SpanOver}}}(A)$ を $$A$$ 上のスパン、 $C:\mathord {\textnormal {\textsf {Cocone}}}(A)$ を余錐、 $D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)$ を $$C$$ 上の余錐とする。型 $\mathord {\textnormal {\textsf {IsCart}}}(D):\mathcal {U}(i)$ を $(\forall _{x:A.\mathord {\textnormal {\textsf {Left}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Right}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}\lbrace x\rbrace ))$ と定義する。 $\mathord {\textnormal {\textsf {IsCart}}}(D)$ の要素があるとき、 $$D$$ はカルテシアン(cartesian)であると言う。

いよいよ本題に入る。次の[007T]はファイバー余積が引き戻しで安定(stable under pullback)であることを表し、これには一価性は必要ない。

[007T] 演習

一価性はカルテシアンな $$C$$ 上の余錐を構成するのに使われる。

[003V] 演習

\lbrace D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)\mid \mathord {\textnormal {\textsf {IsCart}}}(D)\rbrace

は可縮である。さらに、一意に存在するカルテシアンな

D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)

に対して、

\mathord {\textnormal {\textsf {Total}}}(D):\mathord {\textnormal {\textsf {Cocone}}}(\mathord {\textnormal {\textsf {Total}}}(B))

は普遍余錐である。

∞トポス理論で降下性と呼ばれる性質は[007U]のように述べられる。

[007U] 演習

関数外延性と一価性を仮定する。 $$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパン、 $B:\mathord {\textnormal {\textsf {SpanOver}}}(A)$ を $$A$$ 上のスパン、 $C:\mathord {\textnormal {\textsf {Cocone}}}(A)$ を余錐、 $D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)$ を $$C$$ 上の余錐とする。 $$B$$ がカルテシアンで、 $$C$$ が普遍余錐であるとすると、 $$D$$ がカルテシアンであることと $\mathord {\textnormal {\textsf {Total}}}(D)$ が普遍余錐であることは論理的に同値である。