先週の記事では、型理論をホストする圏について考えてみました。ある程度の極限・余極限を持つデカルト閉圏があれば、そこで型理論を展開できそうです。が、対象のあいだの包含関係が欲しくなることがあります。集合圏なら集合の包含関係がありますが、一般的な圏に包含関係があるとは限りません。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
`$
包含関係を持つ圏としては、ゴグエン〈Joseph Goguen〉達が定義した包含的圏〈inclusive category〉が使いやすそうです。次の論文の5ページから6ページにかけて(分量は半ページ分くらい)書いてあります。
- Title: Composing Hidden Information Modules over Inclusive Institutions
- Authors: Joseph Goguen, Grigore Rosu
- Pages: 25p
- URL: https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf
次の論文にも包含系〈inclusion system〉と包含的圏に関する記述があります。
- Title: Grothendieck Inclusion Systems
- Author: Razvan Diaconescu
- Pages: 18p
- http://www.imar.ro/~diacon/PDF/gis.pdf
包含的圏とは、圏の一部として最小元を持つ束〈lattice〉構造が組み込まれている圏のことです。その束構造は、圏 $`\cat{C}`$ の部分圏 $`\cat{I}`$ で与えられます。まず、$`\cat{I}`$ が順序構造になっていることは次の条件で規定されます。
- $`\cat{I}`$ は、$`\cat{C}`$ の広い部分圏である。
- $`\cat{I}`$ は、$`\cat{C}`$ のやせた部分圏である。
- $`\cat{I}`$ は、ガリガリな圏である。
ガリガリな圏〈gaunt category〉とは、同型な対象が同一になる圏です。それぞれの条件を論理式で書けば:
- $`|\cat{I}| = |\cat{C}|`$
- $`\forall A, B \in |\cat{I}|.\, \cat{I}(A, B) = \emptyset \lor \cat{I}(A, B) \cong {\bf 1}`$
- $`\forall A, B \in |\cat{I}|.\, (A \cong B \text{ in }\cat{I}) \Imp A = B`$
$`\cat{A}`$ の($`\cat{I}`$ の)対象 $`A, B`$ に対して関係 $`\sqsubseteq`$ を次のように定義します。
$`\quad A \sqsubseteq B :\Iff \cat{I}(A, B) \ne \emptyset`$
すると、$`(|\cat{C}|, \sqsubseteq)`$ は順序集合になります。部分圏 $`\cat{I}`$ に属する射を包含射〈inclusion morphism〉、または単に包含〈inclusion〉と呼びます。
さらに、束であるために、ミート〈meet〉 $`A\wedge B`$ とジョイン〈join〉 $`A \vee B`$ を持つ必要があります。ジョインとミートを圏論の言葉で表現すれば:
- $`A\wedge B`$ は、$`\cat{I}`$ における直積である。
- $`A\vee B`$ は、$`\cat{I}`$ における直和である。
- $`A\wedge B`$ の射影スパンに対する押し出し〈pushout〉は、$`A\vee B`$ の入射コスパンを与える(以下の図)。
$`\xymatrix{
{} & {A\wedge B} \ar[dl]_{\pi_1} \ar[dr]^{\pi_2}
& {}
\\
{A} \ar[dr]^{\iota_1} & \text{po.} & {B} \ar[dl]_{\iota_2}
\\
{} & {A \vee B} & {}
}\\
\text{ in }\cat{I}`$
さらに、順序集合 $`(|\cat{C}|, \sqsubseteq)`$ は最小元 $`{\bf 0}`$ を持っており、それは $`\cat{C}`$ の始対象に一致します。
包含的圏は、$`(\cat{C}, \cat{I}, \sqsubseteq, \wedge, \vee, {\bf 0})`$ のように書くべきかも知れませんが、短く $`(\cat{C}, \cat{I})`$ で済ませます。
$`(\cat{C}, \cat{I})`$ と $`(\cat{D}, \cat{J})`$ が2つの包含的圏のとき、関手 $`F:\cat{C} \to \cat{D}`$ が、$`\cat{I}`$ の射を $`\cat{J}`$ の射に移すとき包含的関手〈inclusive functor〉といいます。
$`\cat{I}`$ が分配束になるとき、包含的圏 $`(\cat{C}, \cat{I})`$ は分配的包含的圏〈distributive inclusive category〉と呼びます。集合圏は分配的包含的圏になっています。
包含的圏に他の条件を課すときもありますが、それは必要になったときに述べることにします。
[追記 date="翌日"]
次の論文では、ちょっと違った定義をしています。
- Title: Weak Inclusion Systems: Part Two
- Authors: Virgil Emil Cazanescu, Grigore Rosu
- Pages: 17p
- URL: https://www.jucs.org/jucs_6_1/weak_inclusion_system_part/Cazanescu_V_E.pdf
上記論文においては、$`\cat{C}`$ の部分圏 $`\cat{I}`$ が広くてガリガリでやせているとき、$`(\cat{C}, \cat{I})`$ を包含系〈inclusion system〉を持つ圏といいます。$`\cat{I}`$ が束になっているとき、$`(\cat{C}, \cat{I})`$ を強い包含系〈strong inclusion system〉を持つ圏といいます。
$`\cat{C}`$ の弱い包含系〈weak inclusion system〉は、包含系 $`\cat{I}`$ と広い部分圏 $`\cat{E}`$ の組で、ある種の分解〈factorization〉の公理を満たすものです。
[/追記]