「指標の圏はコンテキストの圏の反対圏」で述べたように、指標の圏とコンテキストの圏は互いに反対圏です。まさに表裏一体の関係にあります。となると、コンテキストの圏に関する知見を用いて指標の圏を調べる、あるいは逆に、指標の圏に関する知見を用いてコンテキストの圏を調べることが出来ることになります。
指標の圏には包含構造を載せることが多いです。包含構造には幾つかの種類があるのですが、コンテキストの圏のディスプレイクラスを双対化して新種の包含構造を定義してみます。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\hyp}{\text{-} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\ot}{\leftarrow}
%\newcommand{\op}{\mathrm{op}}
%\newcommand{\Imp}{\Rightarrow }
`$
内容:
包含構造
圏の包含構造については次の過去記事で述べています。
この過去記事で紹介している参考文献は以下の3つです。
- [GR04-]
- Title: Composing Hidden Information Modules over Inclusive Institutions
- Authors: Joseph Goguen, Grigore Rosu
- Year: 2004
- Pages: 25p
- URL: https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf
- [Dia05-]
- Title: Grothendieck Inclusion Systems
- Author: Razvan Diaconescu
- Pages: 18p
- Year: 2005
- http://www.imar.ro/~diacon/PDF/gis.pdf
- [CR00]
- Title: Weak Inclusion Systems: Part Two
- Authors: Virgil Emil Cazanescu, Grigore Rosu
- Year: 2000
- Pages: 17p
- URL: https://www.jucs.org/jucs_6_1/weak_inclusion_system_part/Cazanescu_V_E.pdf
包含構造の定義は少しずつ違いますが、共通する部分を抜き出すと、圏 $`\cat{C}`$ 上の包含構造〈inclusion structure〉、あるいは包含系〈inclusion system〉$`\cat{I}`$ とは次のようなものです。
- $`\cat{I}`$ は $`\cat{C}`$ の広い部分圏である。
- $`\cat{I}`$ は $`\cat{C}`$ のやせた部分圏である。
- $`\cat{I}`$ は $`\cat{C}`$ の骨格的部分圏である。
カザネスク/ロスは「広い」を入れてませんが、「広い」を入れても事情は変わらないし少し便利なので入れておきます。ゴグエン/ロスは束論的な条件を幾つか付けていますが、ここでは考えません。ダイアコネスクは因子分解〈factorization〉の条件を付けていますが、それも考えません。より詳しくは過去記事「圏の束構造と包含的圏」と原論文を参照してください。
注意すべきことは、$`\cat{I}`$ の射が $`\cat{C}`$ のモノ射であることは仮定してないことです。呼び名は「包含」ですが、直感的に包含かどうかはわかりません。呼び名に影響されて、モノ射であると勝手に仮定しないように注意してください。(実際にモノ射のこともありますが、それはまた別な話です。)
指標の圏には包含構造を仮定する場合が多いです。包含構造を持たないノッペラボーの圏だと、やりたいことがなかなか出来ないのです。
ディスプレイクラス
ディスプレイクラスについては過去記事「拡張包括構造のもうひとつの定式化」で述べています。
ファイバー引き戻しに関して閉じた射のクラスをディスプレイ射のクラス〈class of display {maps | morphisms}〉、あるいはディスプレイクラス〈display class〉と呼びます。
ディスプレイクラスの条件として次も付け加えておきます。
- すべての恒等射を含む。
この条件は、部分圏に対する「広い」と同じ条件で、入れても事情は変わらないし少し便利なので入れておきます。
ディスプレイクラスが、圏の結合〈合成〉に対して閉じているとき合成的ディスプレイクラス〈compositional display class〉と呼ぶことにします。「合成的」を使っているのは「結合的」だと associative と区別できないからです。
合成的ディスプレイクラスは、もとの圏の広い部分圏を定義します。その広い部分圏は、もとの圏の任意の射に対するファイバー引き戻し〈プルバック〉に関して閉じています。
分裂ディスプレイクラスは「拡張包括構造のもうひとつの定式化」で定義したとおりです。
分裂子を持つディスプレイクラスを分裂可能〈splittable〉、分裂可能なディスプレイクラスと“特定された分裂子”の組を分裂ディスプレイクラス〈split display class〉と呼びます。
余ディスプレイ包含構造
ディスプレイクラスの双対概念を余ディスプレイクラス〈codisplay class〉と呼びます。より具体的には、圏 $`\cat{C}`$ の射の部分集合 $`\cat{I}\subseteq \mrm{Mor}(\cat{C})`$ が余ディスプレイクラスだとは:
- $`\cat{I}`$ は、$`\cat{C}`$ のすべての恒等射を含む。
- $`\cat{I}`$ は、$`\cat{C}`$ の射による余ファイバー押し出し〈cofiber pushout〉に関して閉じている。
二番目の条件は、次の図式の点線の射が常に存在することです。$`\text{p.o}`$ は、四角形が押し出し四角形であることを示します。
$`\quad \xymatrix{
A \ar[r]^{i} \ar[d]_{f}
\ar@{}[rd]|{\text{p.o}}
& B \ar@{.>}[d]
\\
X \ar@{.>}[r]
& \cdot
}\\
\quad \text{commutative in }\cat{C}\\
\quad \text{where } i \in \cat{I}
`$
余ディスプレイクラスに所属する射は余ディスプレイ射〈codisplay morphism〉と呼びます。
圏 $`\cat{C}`$ の余ディスプレイクラス $`\cat{I}`$ が合成的(結合で閉じている)なら、合成的余ディスプレイクラス〈compositional codisplay class〉と呼びます。合成的余ディスプレイクラスは広い部分圏とみなせます。
ここから先、$`\cat{I}`$ は合成的余ディスプレイクラスと仮定して、圏 $`\cat{C}`$ の広い部分圏とみなします。圏 $`\cat{C}`$ の広い部分圏 $`\cat{I}`$ が、さらに以下の条件を満たすとき、$`\cat{I}`$ を余ディスプレイ包含構造〈codisplay inclusion structure〉または余ディスプレイ包含系〈codisplay inclusion systeme〉と呼びます。
- 部分圏 $`\cat{I}`$ はやせた部分圏である。
- 部分圏 $`\cat{I}`$ は骨格的部分圏である。
別な言い方をすると、余ディスプレイ包含構造は、余ファイバー押し出しに関して閉じた包含構造のことです。
やせた骨格的(とてもやせた〈very thin〉)という条件は非常に強い条件です。余ディスプレイ包含構造を使うと、話が劇的に単純化されることがあります。
おわりに
この記事は、余ディスプレイ包含構造を定義しただけです。この構造は、合成的ディスプレイクラスの双対概念と包含構造を組み合わせたものです。ディスプレイクラスは型理論に由来し、包含構造はインスティチューション理論に由来します。2つの理論からの手法を受け継いだハイブリッドな概念です。
コンテキストの圏と指標の圏が表裏一体であるという事実を利用すれば、色々とハイブリッドな概念を構成可能です。型理論とインスティチューション理論の知見・手法を互いに融通しあうことが出来そうです。