以下の過去記事達で指摘した問題の一部に対する対策をします。
ファイバー積の場合の第一射影と第二射影で使う記法を新たに約束します。双対であるコファイバー和についても論じます。$`\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
%\newcommand{\mbf}[1]{\mathbf{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\Imp}{\Rightarrow}
%\newcommand{\Iff}{\Leftrightarrow}
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{ \mathrm{op} }
\newcommand{\hyp}{\text{－} }
\newcommand{\proj}{\twoheadrightarrow}
\newcommand{\NFProd}[3]{ \mathop{_{#1} \!\underset{#2}{ \times }\,\!_{#3} } }
\newcommand{\Vtimes}{\mathop{!\!{\times}} }
\newcommand{\Vplus}{\mathop{!\!{+}} }
\newcommand{\timesDot}{ \mathop{\times_\bullet} }
\newcommand{\plusDot}{ \mathop{+_\bullet} }
\newcommand{\P}{\mathsf{P}}
\newcommand{\Q}{\mathsf{Q}}
\newcommand{\I}{\mathsf{I}}
\newcommand{\J}{\mathsf{J}}
`$
内容：
標準射影、標準第二射影、標準プルバック四角形
「型理論に出てくる第一射影と第二射影」において、次の3つの場合に、「第一射影・第二射影」の意味がまったく違うことを指摘しました。
- ファミリー付き圏〈CwF〉の場合
- ファイバー積の場合
- 射影分解の場合
型理論で出てくるほとんどの圏は、コンテキスト拡張〈context extension〉に伴う標準射影〈canonical projection〉と標準プルバック四角形〈canonical pullback square〉を備えています。
一時的に（この記事内では）、標準射影を $`\proj`$ で示します。圏 $`\cat{C}`$ 内の標準射影は次のどちらかの形で書きます。
拡張されたコンテキストからの標準射影：
$`\quad \xymatrix{
X\cdot A \ar@{->>}[d]^{\rho^{X, A}}
\\
X
}\\ \In \cat{C}
`$
子から親への標準射影：
$`\quad \xymatrix{
X' \ar@{->>}[d]^{\rho^{X'}}
\\
X
}\\ \In \cat{C}
`$
冗長に $`\rho^{X, A}_X, \rho^{X'}_X`$ と書いてもかまいません。
ファミリー付き圏〈CwF〉の場合、標準射影に伴う第二射影があります。これは標準第二射影〈canonical second projection〉と呼ぶことにします。ファミリー付き圏以外の型理論的圏では、標準第二射影が在るとは限りません。
圏 $`\cat{C}`$ 内の標準射影と標準プルバック四角形は次のように描けます。
$`\quad \xymatrix{
\cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{c.p.b.}}
& \cdot \ar@{->>}[d]^\rho
\\
\cdot \ar[r]_f
& \cdot
}\\
\quad \In \cat{C}
`$
$`\text{c.p.b.}`$ は、この四角形が標準プルバック四角形であることを示します。
射 $`f`$ と標準射影 $`\rho`$ がコスパンになっているとき、このコスパンのプルバック四角形（あるいは極限錐）はたくさんあるかも知れません。ひとつのプルバック四角形を選ぶ写像を $`\mrm{CPBS}`$ （Canonical PullBack Square）とすると、上の図は $`\mrm{CPBS}(f, \rho)`$ を描いたものです。$`\mrm{CPBS}`$ は、型理論的圏の構造の一部になっています。
ファイバー積
次のようなプルバック四角形があるとします。
$`\quad \xymatrix{
Y \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b.}}
& B \ar[d]^g
\\
A \ar[r]_f
& X
}\\
\quad \In \cat{C}
`$
このとき、$`Y`$ はファイバー積〈{fibered | fiber} product〉です。通常、ファイバー積を次のように書きます。
$`\quad Y = A\times_X B`$
しかし、これでは $`f, g`$ の情報が抜けています。僕は次の記法を使っています。
$`\quad Y = A \NFProd{f}{X}{g} B`$
ヴォエヴォドスキーは $`(A, f)\times_X (B, g)`$ と書いています（例えば、下の論文のp.26）。
- [Voe14-15]
- Title: A C-system defined by a universe category
- Author: Vladimir Voevodsky
- Submitted: 28 Sep 2014 (v1), 29 Jul 2015 (v3)
- Pages: 33p
- URL: https://arxiv.org/abs/1409.7925
すべての情報を書くと長ったらしいので省略したくはなります。が、省略するなら $`f, g`$ ではなくて、むしろ $`A, B`$ のほうでしょう。今後、次の記法も使うことにします。
$`\quad Y = f \times_X g`$
$`X`$ も省略したいときがあります。しかし、単に $`f\times g`$ だと、射のデカルト積と区別できません。$`X`$ の位置にドットを置くことにします。
$`\quad Y = f \timesDot g`$
この記法で次のように書けます〈描けます〉。
$`\quad \xymatrix{
{f\timesDot g} \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b.}}
& \cdot \ar[d]^g
\\
\cdot \ar[r]_f
& \cdot
}\\
\quad \In \cat{C}
`$
ファイバー積の射影
デカルト積やファイバー積の射影は、$`\pi`$ を使って書かれます。例えば次のように書けるでしょう。'$`\cdot`$' は、文脈から分かるであろう無名の対象を表します。
$`\quad \pi^{f, g}_1 : f \timesDot g \to \cdot \\
\quad \pi^{f, g}_2 : f \timesDot g \to \cdot
`$
添字を避けるために、次の記法を約束します。
$`\quad \P(f, g) : f \timesDot g \to \cdot \\
\quad \Q(f, g) : f \timesDot g \to \cdot
`$
この記法で次のように書けます〈描けます〉。
$`\xymatrix{
{f \timesDot g} \ar[r]^-{\Q(f, g)} \ar[d]_{\P(f, g)}
\ar@{}[dr]|{\text{p.b.} }
& \cdot \ar[d]^g
\\
\cdot \ar[r]_f
&\cdot
}\\
\quad \In \cat{C}`$
「最近の型理論のハマリ所」では、射影分解して第一成分・第二成分を取り出す写像を $`\mathfrak{p}, \mathfrak{q}`$ を使う約束をしました。$`\P, \Q`$ と $`\mathfrak{p}, \mathfrak{q}`$ を使い分ければ混乱の心配はなくなります。
ファイバー積の別な記法
「シグマ型とパイ型の短縮記法（便利）」において、シグマ型に $`\ltimes`$ を使う記法を紹介しました。“掛け算記号の左に縦棒”ですね。しかし、“足し算記号の左に縦棒”の記号がないようなので、以下のように二文字組み合わせで記号を作ることにします。
- 掛け算記号の左に縦棒（感嘆符）： $`\Vtimes`$ （
\mathop{!\!{\times}}） - 足し算記号の左に縦棒（感嘆符）： $`\Vplus`$ （
\mathop{!\!{+}}）
掛け算記号の左に縦棒（感嘆符）は次のように使います。$`p`$ は圏 $`\cat{C}`$ に備わった特別な射です。
$`\xymatrix{
{X \Vtimes f} \ar[r]^-{\Q(f)} \ar[d]_{\P(f)}
\ar@{}[dr]|{\text{p.b.} }
& \cdot \ar[d]^p
\\
X \ar[r]_f
&\cdot
}\\
\quad \In \cat{C}`$
この書き方は、「ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層」で述べたような状況で便利に使えます。$`X \Vtimes f`$ は、ファミリー $`f`$ のグロタンディーク構成〈平坦化〉と解釈できます。
$`\quad X \Vtimes f = \int_X f = \int (X\mid f)`$
コファイバー和
ファイバー積の双対はコファイバー和〈cofiber sum〉です。スパンのプッシュアウト四角形の頂点（下の図で左上）がコファイバー和となります。
$`\xymatrix{
\cdot
\ar@{}[dr]|{\text{p.o.} }
& \cdot \ar[l]
\\
\cdot \ar[u]
&\cdot \ar[l]^f \ar[u]_g
}\\
\quad \In \cat{C}`$
ファイバー積 $`f\timesDot g`$ の双対として、$`f \plusDot g`$ を使います。コファイバー和の入射〈injection〉には $`\I, \J`$ を使います。
$`\xymatrix{
{f \plusDot g}
\ar@{}[dr]|{\text{p.o.} }
& \cdot \ar[l]_-{\J(f, g)}
\\
\cdot \ar[u]^-{\I(f, g)}
&\cdot \ar[l]^f \ar[u]_g
}\\
\quad \In \cat{C}`$
$`X \Vtimes g`$ の双対として、$`Y \Vplus f`$ を使います。$`i`$ は圏 $`\cat{C}`$ に備わった特別な射です。
$`\xymatrix{
{Y \Vplus f}
\ar@{}[dr]|{\text{p.o.} }
& \cdot \ar[l]_-{\J(f)}
\\
Y \ar[u]^-{\I(f)}
& \cdot \ar[l]^f \ar[u]_i
}\\
\quad \In \cat{C}`$
まとめ
次の記法を使います。
- $`\rho^{X, A}, \rho^{X, A}_X`$
- $`\rho^{X'}, \rho^{X'}_X`$
- $`\mrm{CPBS(f, g)}`$
- $`f\timesDot g`$
- $`\P(f, g)`$
- $`\Q(f, g)`$
- $`X\Vtimes f`$
- $`f \plusDot g`$
- $`\I(f, g)`$
- $`\J(f, g)`$
- $`Y\Vplus f`$
