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

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

圏の束構造と包含的圏

先週の記事では、型理論をホストする圏について考えてみました。ある程度の極限・余極限を持つデカルト閉圏があれば、そこで型理論を展開できそうです。が、対象のあいだの包含関係が欲しくなることがあります。集合圏なら集合の包含関係がありますが、一般的な圏に包含関係があるとは限りません。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
`$

包含関係を持つ圏としては、ゴグエン〈Joseph Goguen〉達が定義した包含的圏〈inclusive category〉が使いやすそうです。次の論文の5ページから6ページにかけて(分量は半ページ分くらい)書いてあります。

次の論文にも包含系〈inclusion system〉と包含的圏に関する記述があります。

包含的圏とは、圏の一部として最小元を持つ束〈lattice〉構造が組み込まれている圏のことです。その束構造は、圏 $`\cat{C}`$ の部分圏 $`\cat{I}`$ で与えられます。まず、$`\cat{I}`$ が順序構造になっていることは次の条件で規定されます。

  1. $`\cat{I}`$ は、$`\cat{C}`$ の広い部分圏である。
  2. $`\cat{I}`$ は、$`\cat{C}`$ のやせた部分圏である。
  3. $`\cat{I}`$ は、ガリガリな圏である。

ガリガリな圏〈gaunt category〉とは、同型な対象が同一になる圏です。それぞれの条件を論理式で書けば:

  1. $`|\cat{I}| = |\cat{C}|`$
  2. $`\forall A, B \in |\cat{I}|.\, \cat{I}(A, B) = \emptyset \lor \cat{I}(A, B) \cong {\bf 1}`$
  3. $`\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`$ を持つ必要があります。ジョインとミートを圏論の言葉で表現すれば:

  1. $`A\wedge B`$ は、$`\cat{I}`$ における直積である。
  2. $`A\vee B`$ は、$`\cat{I}`$ における直和である。
  3. $`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="翌日"]
次の論文では、ちょっと違った定義をしています。

上記論文においては、$`\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〉の公理を満たすものです。
[/追記]