…スラッシュ 4種類のグロタンディーク構成 同語反復ファイブレーション ファイバー反変スードスライシング関手 アスタリスクスラッシュとアスタリスクで何でもかんでも表そうとするのは、僕は嫌いなんですが、その気持ちは脇に置いて、実際に使われているアスタリスクの用法を紹介します。以下、出てくる圏は、すべてプルバック〈ファイバー積〉を持つとします。次の図のような状況を考えます。$`\quad \xymatrix{ {} & {A'} \ar[rr]^{f''} \ar@/^/[dddl…

…リー $`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] &\c…

…らないファミリーからグロタンディーク構成をすると〈要素の圏を作ると〉、ファイブレーションはモノ射〈単射〉とは限りません。値が $`{\bf 0}, {\bf 1}`$ のときは、薄いバンドルが出来ていたのですが、厚みがあるバンドルになるかも知れないのです。しかし、$`|{\bf Bool}|`$ でも $`|{\bf Set}|`$ でも同じように論理ができるので、次の仕掛けがあるのでしょう。 $`{\bf Bool}`$ と $`{\bf Set}`$ は、何らかの意味で同…

…層です。前層に対してグロタンディーク構成、つまり要素の圏〈category of elements〉を作ります。グロタンディーク構成の標準射影と共に次のファイブレーションができます。$`\quad \pi^P : \int_A P \to A \In {\bf Cat}`$$`P`$ の値は $`{\bf 0}`$ か $`{\bf 1}`$ だったので、$`\pi^P`$ は単射になります。この状況を、$`{\bf Cat}`$ から $`{\bf Set}`$ に移します…

…$ は、実は繰り返しグロタンディーク構成でした（「パルムグレンによる、型理論の複前層モデル」参照）。0回、1回の繰り返しも含めた繰り返しグロタンディーク構成を、次の書き方をすることにします。 $`\int (\cat{C}\mid) := \cat{C}`$ $`\int (\cat{C}\mid P) := \int_\cat{C} P`$ $`\int (\cat{C}\mid P_1, P_2) := \int ( \int (\cat{C}\mid P_1) \mid…

…解釈として）普遍的なグロタンディーク構成だとみなせます。宇宙を備えた圏から作られるC-システムはパルムグレンの複前層の圏（「パルムグレンによる、型理論の複前層モデル」参照）と一致するようです。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in }}`$内容： ヴォエヴォドスキーの宇宙圏 C-システムとパルムグレンの複前層の圏 ヴォエヴ…

…ります。ところが、「グロタンディーク構成・逆構成と同値対応」において： 過去記事において、名詞 "cleavage" の翻訳語は「切開」と「亀裂」でどっちがいいか？ とか迷ってますが、名詞も形容詞も亀裂〈cleavage, cloven〉にします。 用語法の方針がずれちゃってますね。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in …

…ス付き圏とみなしてのグロタンディーク構成です。$`\int(\cat{C} \mid P)`$ は、前層 $`P`$ の要素の圏〈category of elements〉と呼ばれます。どのような前層に対しても要素の圏〈グロタンディーク構成〉を作れます。$`\cat{C}`$ が小さい圏なら、要素の圏もまた小さい圏になります。$`\cat{C}`$ が小さい離散圏、つまり単なる集合のときは、要素の圏はファミリーのシグマ型になります。自然数 $`n`$ に対して、次の圏は定義で…

…節とほぼ同じ内容が「グロタンディーク構成・逆構成と同値対応 // 記法・概念の整理： バンドル」にありますが、過去記事を参照しなくて済むように再度書きます。集合のバンドル〈bundle of sets | set bundle〉とは、単に写像のことです。 $`f`$ はバンドル $`\iff`$ $`f`$ は写像 なんでわざわざ写像のことを「バンドル」と呼ぶかというと、 写像は集合圏の射のこと バンドルはバンドルの圏の対象のこと つまり、写像を一種の構造だと考えて、その構造…

…ァイバー付き関手（「グロタンディーク構成・逆構成と同値対応」参照）を射とする1-圏を $`{_1{\bf FibCAT}}`$ とすると、次のように書けます。$`\quad (\mrm{Model}(\Sigma_1) \epito \mrm{Model}(\Sigma_0) ) \in |{_1 {\bf FibCAT}}| `$これが $`\mrm{FibModel}`$ の対象パートを与えます。つまり：$`\quad \mrm{FibModel}(\Sigma) := …

グロタンディーク構成には逆向きの構成があって、それらのペアが“インデックス付き圏の圏”と“ファイバー付き圏の圏”の圏同値を与えます。バンドル-ファミリー対応はその特殊ケースです。前層と“要素の圏”の対応も特殊ケースとなります。そのへんの事情をこの記事で整理します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\op}{ \mathrm{op} } \…

…指標のパラメータ化とグロタンディーク構成 型クラスと忘却・追憶構造 フリーモナド 1： 自由で無料な木 型クラス述語とイプシロン型 結局、指標と仕様の明示的な区別は設けずに、指標の拡大〈拡張〉を使うのが融通が効いて便利だと思います。そのためには、指標の圏には拡大〈extension〉をサポートする構造が必要になります。包含構造を持つ指標の圏等式的関手インスティチューションでは、指標は有向グラフ、またはパス同値関係の集合を追加した有向グラフだと具体的に定義しています。これは具体…

…インデックス付き圏 グロタンディーク構成とファイブレーション 依存アクテゴリー モノイド法則 環境付き計算ペアのミックス操作 ベース射の自明持ち上げ 自明持ち上げの法則 2-圏内のスパンのあいだの射 関連記事： 依存アクテゴリーが面白い 依存アクテゴリーに向けて 依存型理論の圏論的セマンティクスの資料 環境付き計算と依存アクテゴリー 1/n （この記事） 環境付き計算と依存アクテゴリー 2/n 環境付き計算と依存アクテゴリー 3/n 2-圏のなかのスパンのあいだの射 環境付き…

…ンディーク対応から（グロタンディーク構成の逆向きの構成から）インデックス付き圏を作れます。通常の圏で言えば、左脚に対してバンドル-ファミリー対応（「バンドル-ファミリー対応 再考」と、そこからリンクされている記事達を参照）によりファミリーを作ったことになります。左脚（$`\mrm{dom}`$）または右脚（$`\mrm{cod}`$）から作ったファミリー？ そう、それは有向コンテナ、または余有向コンテナですよね（以下の記事参照）。 有向コンテナと多項式コモナド 続・有向コンテ…

…yp)`$ に対するグロタンディーク構成を施します。これが $`\cat{S}`$ の（大域的な）ファミリー構成です。$`\quad \mrm{Fam}^\cat{S}(\cat{S}) := {\displaystyle \int_\cat{S}} (\cat{S}^\hyp)`$$`\mrm{Fam}`$ の右肩に $`\cat{S}`$ が乗っている事情は次の過去記事を参照してください。 Diag構成： 圏論的構成法の包括的フレームワークとして ファミリー構成に関しては…

…ファミリー対応は、“グロタンディーク構成によるファイバー付き圏とインデキシング付き圏の対応”の0-圏バージョンです。ファイバー関手この節では三種類のファイバー関手〈fiber functor〉*2を定義します。まず、前節のバンドル-ファミリー対応から次のような関手が得られます。バンドルにそのファイバーファミリーを対応させます。$`\quad R_K : \cat{S}/K \to \cat{S}^K \In {\bf CAT}\\ \text{For } \obj{g} \i…

…インデックス付き圏のグロタンディーク構成 スライシング関手 スライス圏$`\cat{C}`$ は小さい圏とします。$`\cat{C}`$ の対象は、ラテン文字小文字の最初のほう $`a, b, \cdots`$ で表します。$`\cat{C}`$ の射は、ラテン文字小文字の中間あたりの $`f, g, \cdots`$ で表します。$`\cat{C}`$ の対象 $`c\in |\cat{C}|`$ に対して、スライス圏〈slice category | オーバー圏 | ov…

…ン $`(k, f)`$ に対する右カン拡張1-射〈right Kan extension 1-morphism〉です。解の2-射 $`\rho`$ に名前が付いてないのは単に偶発的・歴史的事情です。 *1:くぼみの意味です。英語だと「ニーシ」に近い発音です。 *2:https://pixabay.com/vectors/water-rain-teardrop-liquid-drop-1560478/ *3:前層・余前層からグロタンディーク構成をして得られる“要素の圏”です。

…インデックス付き圏とグロタンディーク構成に関する過去記事を2つだけ挙げておくと： インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 小さい1-圏 $`\cat{I}`$ に、自明な2-射（1-射のあいだの等式）を追加した2-圏を $`\dimU{ \cat{I} }{2}`$ として、以下の $`F`$ のようにインデックス付き圏を定義すると、一般化されたインデックス付き圏の概念になります。$`\quad F: (\dimU{\cat{I}}{2})^…

…の射です。要素の圏はグロタンディーク構成によるファイバー付き圏〈{fibred | fibered} category〉の特別なもので、ファイバーが離散圏（事実上、単なる集合）であるものです。グロタンディーク構成については、次の過去記事に説明があります。 インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 プロ関手 $`P`$ の場合は、状態空間であるインデックス付き集合のインデキシング集合は次の形になります。$`\quad |\cat{C}^\op\t…

…Groth}`$ はグロタンディーク構成です。本来のグロタンディーク構成の退化バージョンで、コンテナ $`A = (X \mid A[\hyp])`$ に次のようなパイ型で作ったバンドルを対応させます。$`\quad \pi : \sum_{x\in X}A[x] \to X \In {\bf Set}`$バンドルの構成素名を $`\mrm{Tot}`$（全空間）、$`\mrm{Base}`$（底空間）、$`\mrm{proj}`$（射影）とすると：$`\Let B = \m…

…。（以下の積分記号はグロタンディーク構成です。）$`\quad \doct{D}\text{-}\mrm{CoDiag}^{\cat{D}, J}(\cat{C}) := \Int{\cat{D}} \doct{D}(J(\hyp)^\op, \cat{C}) `$$`\doct{D}`$ がデフォルトの $`{\bf CAT}`$ である場合は：$`\quad \mrm{CoDiag}^{\cat{D}, J}(\cat{C}) := \Int{\cat{D}} {\bf …

…インデックス付き圏にグロタンディーク構成をほどこすと平坦化圏ができます。それがDiag構成の結果〈成果物〉です。$`\quad \doct{D}\text{-}\mrm{Diag}^\cat{S}(\cat{D}) := \Int{\u{\cat{S}}} \doct{D}\text{-}\mrm{Diag}^\cat{S}[\hyp](\cat{D}) \;\in |{\bf CAT}| `$グロタンディーク構成はファイバー付き圏〈{fibred | fibered} ca…

…。以下で、積分記号はグロタンディーク構成です。$`\quad \mrm{Diag}^{\cat{C},J }[\hyp_1](\hyp_2) := {^{\cat{C},J} \doct{D}}(\hyp_1, \hyp_2) = \doct{D}(J(\hyp_1), \hyp_2)\\ \quad \mrm{Diag}^{\cat{C},J }(\cat{D}) := \int_{\cat{C}} \mrm{Diag}^{\cat{C},J }[\hyp](\cat{D}…

…インデックス付き圏のグロタンディーク構成〈Grothendieck construction for indexed category〉の特殊ケースです。前層 $`F`$ の要素の圏を $`\mrm{El}(F)`$ と書きます。圏 $`\mrm{El}(F)`$ の対象の集合は、次の集合論的シグマ型で与えます。$`\quad |\mrm{El}(F)| := \sum_{X\in |\cat{C}|} F(X)`$要するに、$`F(X)`$ 達をすべて寄せ集めた集合です。た…

…ックス付き圏なので、グロタンディーク構成〈Grothendieck construction〉ができます。グロタンディーク構成によって出来上がる平坦化圏には順方向と逆方向があります。インデックス付き圏の場合と余インデックス付き圏の場合で合計4種類の平坦化圏があります（グロタンディーク構成と積分記号）。4種類の平坦化圏と対応する積分記号（平坦化のオペレータを表す）は： $`\int_\rightarrow`$ ： インデックス付き圏の順方向平坦化圏 $`\int_\leftar…

…インデックス付き圏のグロタンディーク構成のトータル圏（「最近の型理論： 拡張包括構造を持ったインデックス付き圏」の最初の節参照）の射です。関手コボックスとスプリッター図ロブスキ／ザンサイの描画方向は、射の方向が右から左、モノイド積の方向が上から下ですが、僕の説明は射の方向が上から下、モノイド積の方向は左から右です。描画方向やその変換は次の記事を参照してください。 絵算（ストリング図）における池袋駅問題の真相 双対や随伴に強くなるためのトレーニング ストリング図、関手ボックス、…

…インデックス付き圏のグロタンディーク構成 $`\cat{P}`$ は関手ですが、引数渡しはブラケットを使って $`\cat{P}[X], \cat{P}[f]`$ のように書くことにします。「インデックス・アクセスはブラケットで書く」という習慣からです。次の用語を使います。 関手 $`\cat{P}`$ の域である圏 $`\cat{C}`$ を、インデキシング圏〈indexing category〉またはベース圏〈base category〉と呼びます。インデックス付き圏とイ…

…at{P}`$ からグロタンディーク構成した平坦化圏〈flattened category〉を $`\int_\cat{C} \cat{P}[\hyp]`$ 、あるいはより短く $`\int \cat{P}`$ と書くことにします。$`X\in |\cat{C}|`$ と $`p\in |\cat{P}[X]|`$ のペア $`(X, p)`$ が平坦化圏 $`\int \cat{P}`$ の対象となります。次の形の射は、ひとつのファイバー内に収まる“垂直な射”なので、ファイ…

…ンデックス付き圏にはグロタンディーク構成ができるので、グロタンディーク平坦化圏とグロタンディーク・ファイブレーション（すぐ下）を構成できます。$`\quad \pi : \int_\cat{C} \cat{P}[\hyp] \to \cat{C} \In {\bf CAT}`$グロタンディーク構成については、例えば次の記事を参照してください。 インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 射影と随伴トリプル系$`X, A \in |\cat{C}|…