このブログの更新は X（旧Twitter）アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

［参照用 記事］

テレスコープと包括クラン

雑記／備忘

テレスコープと包括クランという概念を導入して、“型理論／インスティチューション理論のための圏論”のツールボックスに付け加えます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
%\newcommand{\Imp}{\Longrightarrow} % for meta prop
%\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
`$

内容：

テレスコープ

証明支援系のマニュアルや論理／型理論の論文・書籍などで、たまに「テレスコープ〈telescope〉」という言葉を見かけます。この言葉を使い始めたのはド・ブラウン〈Nicolaas Govert de Bruijn〉です。次の論文の1.6節に A few remarks about the word “telescope” があります。

ド・ブラウンは、ラムダ式のド・ブラウン・インデックスや証明ソフトウェアの先駆けといえる Automath で有名な数学者です。

テレスコープは、型宣言や命題のリストです。次のような形をしています。

$`\quad (x_1: A_1, \cdots, x_n: A_n)`$

$`x_i`$ は名前ですが、名前は削除できます（「指標から名前の削除」「指標から名前の削除 その2」参照）。リストの項目〈成分〉のあいだに依存性があってもかまいません。つまり、$`k`$番目の項目 $`A_k`$ は、$`k`$番目より前の名前（変数名） $`x_1, \cdots, x_{k-1}`$ を含むかもしれない式〈記号的表現〉です。

「テレスコープ」は、型理論の「コンテキスト」やインスティチューション理論の「指標」と同義です。「同義語を増やす気か？」となじられそうですが、「コンテキスト／指標」とは別な意味で「テレスコープ」を使いたいことがあるのです。

型理論／インスティチューション理論において、テレスコープがコンテキスト／指標と100パーセント同じこともありますが、テレスコープをコンテキスト／指標と同一視できない場合があります。

包括クラン

型理論／インスティチューション理論を展開する場として、どのような圏がいいか？ これには色々な意見があります。現状、僕は、次の3つの概念を組み合わせるのが良いと思っています。

  1. ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉
  2. ジョイアル〈Andre Joyal〉のクラン〈clan〉
  3. カートメル／ヴォエヴォドスキー〈John Cartmell, Vladimir Voevodsky〉のC-システム〈C-system〉（カートメルの用語ではコンテキスト圏〈contextual category〉）

包括圏は、抽象度が高い（アブストラクト・ナンセンスな）方法で定義されています。初見では分かりにくいでしょうが、包摂する範囲は広く、次のように要求してもよさそうです。

  • 依存性を持つ型理論／インスティチューション理論／論理は、包括圏により定式化すべき。

実際、より具体的に定義される構造は、包括圏の特殊化、構造・条件を追加したものと解釈できる場合がほとんどです。具体的な定義では、コンテキスト拡張演算〈context extension operator〉を使う場合が多いので、そのときは、ジェイコブスの包括構造を拡張包括構造〈extension-comprehension structure〉とも呼びます。拡張包括構造については：

「最近の型理論： 拡張包括構造を持ったインデックス付き圏 // 拡張包括構造」にも記述がありますが、ちょっと分かりにくいので再論したのが上記過去記事です。

クランは、拡張包括構造を載せる下部構造として適切だと思います。クランについては、以下の過去記事を参照してください。

C-システムは、ほどよい抽象度の型理論的圏（「指標の圏はコンテキストの圏の反対圏」参照）です。以下の過去記事を参照してください。

さて、C-システムよりは抽象度が高く、包括圏よりは具体的な型理論的圏（「指標の圏はコンテキストの圏の反対圏」参照）として、包括クラン〈comprehension clan〉を定義します。

まず、$`\cat{C} = (\u{\cat{C}}, \mbf{1}_\cat{C}, \cat{P}_\cat{C})`$ をクランとします。ここで：

  • $`\u{\cat{C}}`$ ： クランの台圏
  • $`\mbf{1}_\cat{C}`$ ： 特定された終対象
  • $`\cat{P}_\cat{C}`$ ： クランのファイブレーションクラス

包括クラン $`\cat{K}`$ は、台クラン $`\cat{C}_\cat{K}`$ に拡張包括構造が追加されます。次のように書きます。

$`\quad \cat{K} = (\cat{C}_\cat{K}, \msc{S}_\cat{K}, \mrm{CExt}_\cat{K}, \rho_\cat{K}, \mrm{CPBSq}_\cat{K})`$

ここで：

  • $`\msc{S}_\cat{K}`$ ： エス関手（「コンテキストの圏と指標の圏と限量子 // エス関手」参照）、台圏（台クランの台圏）上の前層
  • $`\mrm{CExt}_\cat{K}`$ ： コンテキスト拡張演算、通常ドットで書く； $`(\Gamma, A)\mapsto \Gamma\cdot A`$
  • $`\rho_\cat{K}`$ ： 対象〈コンテキスト〉 $`\Gamma`$ と $`A\in \msc{S}(\Gamma)`$ に標準射影〈canonical projection〉$`\rho_\cat{K}^{\Gamma, A}`$ を割り当てる写像
  • $`\mrm{CPBSq}_\cat{K}`$ ： 射 $`\varphi: \Gamma \to \Delta`$ と $`B\in \msc{S}(\Delta)`$ に標準プルバック四角形〈canonical pullback square〉$`\mrm{CPBSq}_\cat{K}(\varphi, B)`$ を割り当てる写像

これらは拡張包括構造の条件を満たすとします。この条件は、エス関手 $`\msc{S}_\cat{K}`$ をグロタンディーク構成したファイバー付き圏上に、ジェイコブスの意味の包括関手（アロー圏へのデカルト関手）を作れることを保証します。

包括クランのテレスコープ圏

記号の乱用により、包括クランと台クランを同じ記号 $`\cat{C}`$ で表します。

$`\quad \cat{C} = (\cat{C}, \msc{S}_\cat{C}, \mrm{CExt}_\cat{C}, \rho_\cat{C}, \mrm{CPBSq}_\cat{C})`$

下付きの $`{_\cat{C}}`$ はたいてい省略します。さらに、台クランの台圏も同じ記号 $`\cat{C}`$ で書きます。コンテキスト拡張演算 $`\mrm{CExt}`$ はドット（$`\cdot`$）で書きます。

包括クラン $`\cat{C}`$ の対象（正確には、包括クランの台クランの台圏の対象）$`\Gamma`$ を固定します。そして、次のようなリストを考えます。

$`\quad (A_1, A_2, \cdots, A_n)\\
\text{where}\\
\quad A_1 \in \msc{S}(\Gamma)\\
\quad A_2 \in \msc{S}(\Gamma\cdot A1)\\
\quad \cdots\\
\quad A_n \in \msc{S}(\Gamma\cdot A1\cdot\;\cdots\; \cdot A_{n - 1})
`$

この形のリストを、$`\Gamma`$ 上のテレスコープ〈telescope〉と呼びます。長さ 0 のリスト $`()`$ も特別なテレスコープと考えます。長さ 1 のリスト $`(A)\;\text{ where }A\in \msc{S}(\Gamma)`$ はもちろんテレスコープです。

C-システムでは、カートメルツリー構造の存在から、すべてのコンテキストを終対象上のテレスコープの形で書けます。したがって、コンテキストとテレスコープを区別する必要がなく、テレスコープという概念を導入する意味はありません。しかし、C-システムとは限らない（カートメルツリー構造を持たない）包括クランでは、すべてのコンテキストが終対象上のテレスコープと同一視できることは保証されません。コンテキストとテレスコープは別な概念となります。

テレスコープによるコンテキスト拡張は次のように定義します。

  • $`\Gamma\cdot () := \Gamma`$
  • $`\Gamma\cdot (A) := \Gamma\cdot A`$
  • $`\Gamma\cdot (A_1, \cdots, A_k, B) := (\Gamma\cdot (A_1, \cdots, A_k) )\cdot B`$

包括クラン $`\cat{C}`$ のコンテキスト〈対象〉 $`\Gamma`$ 上のテレスコープを対象とする圏 $`\mrm{Teles}(\cat{C})[\Gamma]`$ を定義できます。$`(A_1, \cdots, A_n)`$ と $`(B_1, \cdots, B_m)`$ を $`\Gamma`$ 上のテレスコープだとして、そのあいだの射 $`\varphi`$ は、以下の図式を可換とする $`\cat{C}`$ の射として定義します。

$`\quad \xymatrix{
{\Gamma\cdot (A_1, \cdots, A_n)} \ar[r]^\varphi \ar[d]
&{\Gamma\cdot (B_1, \cdots, B_m)} \ar[d]
\\
\Gamma \ar@{=}[r]
&\Gamma
}\\
\quad \text{commutative }\In \cat{C}
`$

上図において、ラベルがない縦方向の2本の射は、標準射影〈canonical projection〉達の結合〈composition〉で作られる射です。

$`\mrm{Teles}(\cat{C})[\Gamma]`$ が圏になることはほとんど自明でしょう。この圏を、包括クラン $`\cat{C}`$ のコンテキスト $`\Gamma`$ 上のテレスコープ圏〈telescope category | テレスコープ達の圏 | category of telescopes〉と呼びます。

カートメルツリー構造を持たない包括クランにおいては、対象〈コンテキスト〉がリストで書けるとは限りません。しかし、テレスコープ圏の対象は定義からリストです。リストには長さがあるので、長さに沿った帰納的・再帰的な手法が使えます。C-システムに関する議論の一部を一般の包括クランにも適用できます。

テレスコープ圏は、もとになる包括クランに構造を追加したわけではありません。任意の包括クランに対してテレスコープ圏を定義できます。$`\mrm{Teles}(\cat{C})[\Gamma]`$ の $`\Gamma`$ を動かすと次のような写像になります。

$`\quad \mrm{Teles}(\cat{C}) : |\cat{C}| \to |\mbf{Cat}| \In \mbf{SET}`$

$`\mrm{Teles}(\cat{C})`$ は包括クラン $`\cat{C}`$ の外部で構成したものであり、$`\cat{C}`$ を調べたり使ったりするときの道具として便利なのです。

テレスコープ圏のアイディアは、パルムグレンの複前層モデル（「パルムグレンによる、型理論の複前層モデル」参照）に既に含まれています。つまり、複前層モデルはテレスコープ圏の典型的事例となります。包括クランとテレスコープ圏の枠組みで、パルムグレンの複前層モデルをより良く理解できる、とも期待できます。