…す。シグマ型形成子はグロタンディーク構成〈Grothendieck construction〉の一種なので、グロタンディーク構成の標準的な記法である積分記号を使って書くと、次の同型が得られます。$`\quad \int( (x, y) \in X \times Y) \mid G(x, y) ) \cong \int(x\in X \mid \int( (x, y) \in \{x\}\times Y \mid G(x, y) ) ) `$もう少し簡略に書くと：$`\quad…

…ンデックス付き圏にはグロタンディーク構成ができるので、次のようなファイブレーション〈ファイバー付き圏〉が得られます。$`\quad \pi : \int_{\cat{S}} \mrm{Model}[\hyp] \to \cat{S} \In \mbf{CAT}`$ こうしてできたファイブレーションが、インスティチューション理論と関手意味論が融合した世界となります*11。ホーアの世界観ゴグエンとローヴェアの教義により構成した世界は素晴らしいのですが、ホーア論理に基づきソフトウェ…

…的有向高次グラフ〉のグロタンディーク構成 2-セルラー層 上昇写像と下降写像 テレスコープ前層としての2-セルラー層 2-セルラー層の単体条件 2-セルラー層の単体条件 続き 2-セルラー層のセクション 外微分作用素 外微分作用素のベキ零性 2-セルラー層の異種混合ド・ラーム複体 単体的有向n-グラフここで扱う組み合わせ的対象物〈combinatorial object〉は半単体集合〈semisimplicial set〉です。が、より説明的な呼び名「単体的有向n-グラフ」も…

…。シグマ型、パイ型、グロタンディーク構成などを引き合いに出さず、直接的定義をします。$`\bigcup_{i\in V}\u{F_\mrm{vert}(i)}`$ は、ベクトル空間の台集合（下線で示している）達をすべて合併した集合です。ベクトル空間ファミリー $`F_\mrm{vert}`$ のセクション〈section〉とは次のような写像です。$`\quad \bs{x} : V \to \bigcup_{i\in V}\u{F_\mrm{vert}(i)} \In \mb…

…C} X`$ 右辺はグロタンディーク構成ですが、前層のグロタンディーク構成は要素の圏〈category of elements〉と呼びます。コンマ圏から要素の圏への圏同値を与える関手 $`\Phi`$ を以下で構成します。Φの対象パートコンマ圏 $`(よ\DA X)`$ の対象 $`\An{a, \varphi, X}`$ を考えます。このコンマ圏の対象を $`\cat{C}^\wedge`$ 内で考えれば：$`\quad \varphi: よ^a \to X \In \ca…

…参照してください。 グロタンディーク構成・逆構成と同値対応 ファイバー引き戻しとプレ結合引き戻し集合のバンドル $`a : A \to B`$ に対して、写像 $`\varphi:X \to B`$ によるファイバー引き戻しは次のように書きます。$`\quad \varphi^\#(a) : \o{\varphi^\#(a)} \to X \In \mbf{Set}`$ 図式では：$`\quad \xymatrix{ {\o{\varphi^\#(a)}} \ar[r] \a…

…`$ に対する2つのグロタンディーク構成の組み合わせです。 通常のグロタンディーク構成 $`\int \msc{A}(\hyp)`$ ファイバー反転のグロタンディーク構成 $`\int \msc{A}(\hyp)^\op`$ 通常のグロタンディーク構成の代わりにアロー圏構成も使えます。$`\mbf{Set}/\hyp`$ のグロタンディーク構成 $`\int (\mbf{Set}/\hyp)`$ とアロー圏構成 $`\mrm{Arr}(\mbf{Set})`$ は同じことです…

…{Pred}`$ （グロタンディーク構成） 包括圏の射影は、グロタンディーク構成の射影。 $`\pi := \pi_{\mrm{Pred}} : \int_{\mbf{Set}}\mrm{Pred} \to \mbf{Set} \In \mbf{CAT}`$ 包括圏の作用は、包括。 $`(\cdot)(\ctxpair{p}{X} ) = X\cdot p := \{X\mid p\}`$ 包括圏の包括自然変換は、包含射〈包含写像〉の族。 $`\rho_X^p := \mrm…

…シング関手）です。逆グロタンディーク構成のアットマーク記法（「包括コンテキスタッドに向けて // グロタンディーク構成と逆グロタンディーク構成」参照）を使えば次のように書けます。$`\quad f^* = \mrm{Decl}(f) = \cat{D}@(f)`$ファイブレーション〈ファイバー付き圏〉 $`\cat{D}`$ とファミリー〈インデックス付き圏〉 $`\cat{D}@`$ は相互に置き換え可能なので、デカルト持ち上げ $`f'`$ の代わりに翻訳関手（宣言関手 …

…ンデックス付き圏〉 グロタンディーク構成と逆グロタンディーク構成 ファイブレーション的プルバック四角形 デカルト持ち上げと亀裂子／分裂子 反ファイブレーション 局所ホニャララ・ファイブレーション 中置演算子記号の使い方 セクションとレトラクション トータル射の結合公式と図示 おわりに 補足： グロタンディーク対応 追記： 終対象の保存 ハブ記事： コンテキスタッド、包括圏、ハイパードクトリン ファイブレーションファイブレーションに関する過去記事達（古い順）を挙げておきます。 …

…t{C}`$ から逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）で得られたインデキシング〈インデックス付き圏〉です。 グロタンディーク構成 : インデキシング〈インデックス付き圏〉→ ファイブレーション〈ファイバー付き圏〉 逆グロタンディーク構成 : ファイブレーション〈ファイバー付き圏〉→ インデキシング〈インデックス付き圏〉 トータル射 $`F`$ のファイバーパート〈fiber part〉は $`F^\flat`$ と書くことにします。ファイバ…

…コープ閉包の作り方 グロタンディーク構成とデカルト圏に関する準備 ハイパードクトリンのグロタンディーク構成への持ち上げ Q の対象パート Q の射パート Q の射パートの対象パート Q の射パートの射パート 残っている作業 依存演算の代数系としてのコンテキスタッド 関連記事： 依存アクテゴリーが面白い 環境付き計算と依存アクテゴリー 1/n コンテキスタッドかぁ、ウーム‥‥ コンテキスタッド、包括圏、ハイパードクトリン （この記事） 型理論とコンテキスタッド： コンテキストフ…

…余表現問題 余前層のグロタンディーク構成と始対象 忘却関手でラップしたアンダー圏 おわりに ※色付きテキストは次の約束で使います。 青い文字： 重要な概念・用語だがこの記事内では定義・説明してないもの。 赤い文字： この記事内で導入・定義した概念・用語。 マゼンタの文字： この記事内の後方で導入・定義する概念・用語。 自由-忘却・随伴系とアドホック随伴系（復習）自由-忘却・随伴系〈free-forgetful adjunction〉は次の形で書きます。$`\quad \xym…

…-特性付きクランからグロタンディーク構成をしてファイバー付き圏〈グロタンディーク・ファイブレーション〉を作ります。このファイバー付き圏が包括構造〈拡張包括構造〉を載せる台になります。k-特性付きクランの構造や性質が、対応するファイバー付き圏や、その上に載る包括構造にどのような影響を及ぼすか？ k-特性付きクランのあいだの準同型射と包括クランの準同型射はどのように関係するか？ -- ここらへんがとりあえず調べるべき課題でしょう。 *1:「特性」だと characteristic…

…ンデックス付き圏は、グロタンディーク構成／逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）で対応します。別な言い方をすると、圏 $`\cat{C}`$ 上のインデックス付き圏 $`S : \cat{C}^\op \to \mrm{CAT}`$ があり、それから次の包括構造を作ったとき、関手〈インデックス付き圏〉 $`S`$ は、当該包括構造〈包括圏〉のエス関手です。$`\quad \xymatrix{ {\int_\cat{C} S} \ar[d]_{…

…テキスト拡張演算： グロタンディーク構成 $`(\Gamma, A) \mapsto \int_{\Gamma} A`$ 標準射影： グロタンディーク構成の標準射影 $`\pi^{\Gamma, A} : \int_{\Gamma} A \to \Gamma`$ 標準プルバック四角形： 関手 $`\varphi:\Gamma \to \Delta`$ と前層 $`B`$ に対して以下のような可換四角形を対応させる。 $`\quad \xymatrix{ {\int_\Gamm…

…cat{K}`$ をグロタンディーク構成したファイバー付き圏上に、ジェイコブスの意味の包括関手（アロー圏へのデカルト関手）を作れることを保証します。包括クランのテレスコープ圏記号の乱用により、包括クランと台クランを同じ記号 $`\cat{C}`$ で表します。$`\quad \cat{C} = (\cat{C}, \msc{S}_\cat{C}, \mrm{CExt}_\cat{C}, \rho_\cat{C}, \mrm{CPBSq}_\cat{C})`$ 下付きの $`{…

…msc{S}`$ のグロタンディーク構成〈要素の圏〉とその標準射影です。$`\quad \cat{E} = {\displaystyle \int_{\cat{C}} }\msc{S}`$ 包括圏の包括関手 $`\gamma : \cat{E} \to \mrm{Arr}(\cat{C})`$ は、拡張包括構造の $`\mrm{CPBSq}`$ から構成できます。$`\mrm{CPBSq}`$ から構成した包括関手 $`\gamma`$ がデカルト関手なのは定義から従います。…

…p]`$ を考えて、グロタンディーク構成すればOKです。$`\quad \mbf{Fam}_{(\mbf{Set}, P, S)} := {\displaystyle \int_{\mbf{Set}\times\mbf{Set}}} \mbf{Fam}_{(\mbf{Set}, P, S)}[\hyp]`$ 豊穣靴履きファミリー$`F`$ が、左靴 $`P`$ 、右靴 $`S`$ を履いた靴履きファミリーだとは、 $`\quad F:P(X)\times S(Y) \to |…

…だの射を定義するにはグロタンディーク構成を利用します。この定義をするには、関手圏とグロタンディーク構成の説明を事前にする必要があるので、僕は、上記のような定義を使うときが多いです。異なる集合上のファミリーのあいだの射も、グロタンディーク構成を経由しないで直接的に定義できます（以下にその記述あり）。 [/補足]$`F, G`$ は、異なる（かも知れない）集合 $`X, Y`$ 上の$`\cat{D}`$-値ファミリーだとします。$`\quad F:X \to |\cat{D}|…

…うです。この記事で、グロタンディーク構成と余極限で位相実現がほんとに出来ることを事例により極めて具体的に説明します。またこの記事により、組み合わせ幾何的対象物とは、位相化可能構造を備えた組み合わせ的構造物だということがハッキリするでしょう。組み合わせ幾何的対象物（幾何グラフとも呼ぶ）は、組み合わせパートと幾何パートに明白に分離できます。位相化可能構造を担う幾何パートは、“位相化関手を備えたリーディ圏”により提供されます。$` \newcommand{\cat}[1]{ \ma…

…前層 $`X`$ のグロタンディーク構成（要素の圏〈category of elements〉とも呼ぶ）を使うのが、直感的で素直な気がします。グロタンディーク構成は、どんな前層に対しても作れます。$`X:\cat{S}^\op \to \mbf{Set}`$ のグロタンディーク構成は次のように書きます。$`\quad \int_{\cat{S}} X \;\in |\mrm{Cat}|`$ $`\cat{S}`$ は小さい圏（と仮定）なので、グロタンディーク構成〈要素の圏〉も…

… 関手の表現可能性 グロタンディーク構成 随伴系 テンプレート充填問題〈template filling problem〉とは、以前はフレーム充填問題〈frame filling problem〉と呼んでいたものです（「圏論におけるフレーム充填問題」、「フレーム充填問題と解空間関手」参照）。フレームは、テンプレートのなかで既に決まっている部分で、埋める〈fillする〉のは、フレーム以外の未定の部分です。なので、テンプレート充填問題のほうが適切かな、と。ストリング図やペースティ…

…インデックス付き圏のグロタンディーク構成を使えば次のように書けます。$`\quad \mbf{Cont} := {\displaystyle \int_{\mbf{Set}} } \mbf{Cont}[\hyp]`$ グロタンディーク構成に伴う標準射影は $`(X, F) \mapsto X,\; (f, \varphi)\mapsto f`$ です。コンテナのあいだの射を $`\alpha = (f, \varphi)`$ と書いたときは、次の記法を使います。 $`\bas…

…t}`$ この前層にグロタンディーク構成をします。前層のグロタンディーク構成（の結果）は要素の圏〈category of elements〉と呼びます。$`\quad \mrm{El}( \mrm{Map}(\hyp, \mcl{U}) ) = {\displaystyle\int_{\mbf{FinSetG}} }\mrm{Map}(\hyp, \mcl{U}) \;\in |\mbf{CAT}|`$ 要素の圏 $`\mrm{El}( \mrm{Map}(\hyp, \mc…

…\int}`$ は、グロタンディーク構成（前層／余前層に対しては要素の圏〈category of elements〉）を表す記号。 $`{\displaystyle \sum}`$ は、シグマ型（集合達の総直和）を表す記号。 $`P\H\mbf{Bun}^\mrm{fin}_C`$ は、セル達（「一般化ハイパーグラフ → P-バンドル、P-ファミリー」参照）の集合が有限である$`P`$-バンドル達からなる $`P\H\mbf{Bun}_C`$ の充満部分圏。 $`\mrm{T…

…。 前層の要素の圏（グロタンディーク構成）を考える。 要素の圏の対象集合〈set of objects〉を再配置同値関係で割った商集合を考える。 商集合の要素が、圏 $`\cat{R}`$ が決める有限コレクション。 けっこうめんどくさい手順です。この手順による構成には次のメリットがあります。 圏 $`\cat{R}`$ を変えることにより、色々な種類の有限コレクションが得られる。 有限コレクションの集合を作る操作 $`X \mapsto \mrm{FinColl}_{\ca…

…使ってみては？ あるいは、既に小さい骨格が使われているかも知れない。 前層やインデックス付き圏を見たら、すぐにグロタンディーク構成しよう。グロタンディーク構成の平坦化圏やファイバー付き圏を使ったほうが見やすいことも多い。 二種類の射があるように思えたら、二重圏あるいは二重圏類似構造が存在するかも。 三種類の射があるように思えたら、三重圏あるいは三重圏類似構造が存在するかも。 オペラッド構造が見つかるといいことあるよ。見つけよう。 モナドが見つかるといいことあるよ。見つけよう。

…った射＝ピボット”とグロタンディーク構成 プロ関手でもピボットとサンドイッチ結合 Webのサーバーサイド処理とレンズWebのサーバーサイド処理を、2つの部分〈コンポネント〉に分けて考えます。ひとつは、サーバーサイドの出入り口側に位置するコンポネントで、変換プロセッサ〈transform processor〉と呼びましょう。もうひとつは、奥側〈アップストリーム〉に居るピボット・プロセッサ〈pivot processor〉です。この2つのコンポネントを絵に描けば次のようです。変換…

…慮しています。また、グロタンディーク構成を繰り返し適用することにより、カートメルツリー構造（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）を実現しています。カートメルツリー構造を持つことから、Presheaves-as-Types の立場の型理論を、抽象的な構造であるC-システムとみなすことが出来ます。つまり、カートメル／ヴォエヴォドスキーの一般論を適用できます。単純型理論 vs. 依存型理論あまたある型理論を分類する基準として、単純型理論と依存型理論と…