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

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

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

参照用 記事

インデックス付き圏 の検索結果:

グロタンディーク構成・逆構成と同値対応

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

環境付き計算と依存アクテゴリー 1/n

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

すべての随伴系達が作る構造は?

…: 随伴系の圏の上のインデックス付き圏として (2022年) 「最近のモナド論の概観と注意事項 1/2」で紹介した文献をひとつだけ再掲しておきます。バスケス-マルケスの次の論文です。 [Vaz15-17] Title: Monad and Comonad Objects through 2-adjunctions of the type Adj-Mnd Submitted: 15 Oct 2015 (v1), 8 Jun 2017 (v3) Author: Adrian Va…

依存型理論の圏論的セマンティクスの資料

…拡張包括構造を持ったインデックス付き圏」で概要を述べた包括圏〈comprehension category〉が、依存アクテゴリーの事例になりそうです。 「最近の型理論: 拡張包括構造を持ったインデックス付き圏」は、バート・ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉というより、ファミリー付き圏と局所デカルト閉圏を若干抽象化した圏を想定して書いていたようです。 型理論では、型の意味論としてファミリー付き圏〈CwF | categ…

依存アクテゴリーに向けて

…スについては、「2階インデックス付き圏と反ラックス余錐」で述べたように: この呼び名は、どちらかの方向をラックスと決めたら、もう一方を反ラックス(あるいは余ラックス)と呼ぶだけで、逆の呼び名もありえます。また、ラックスと反ラックスを区別しないこともあります。 要はお約束の問題です。一般的・統一的ルールは無理なので、その場その場でどっちがラックスかを決めることにします。アナロジー集合〈0-圏〉上の構造と圏〈1-圏〉上の構造では、文字通り“次元が違います”。0次元ベースの構造と1…

依存アクテゴリーが面白い

…題があります。「2階インデックス付き圏と反ラックス余錐」から: この呼び名は、どちらかの方向をラックスと決めたら、もう一方を反ラックス(あるいは余ラックス)と呼ぶだけで、逆の呼び名もありえます。また、ラックスと反ラックスを区別しないこともあります。 形容詞「反ラックス」は取り去って、ここでは単に依存アクテゴリー〈dependent actegory〉と呼びます。カプチ/マイヤースは、依存アクテゴリーと一般化Para構成〈generalized Para constructio…

ファイバーの計算 全体像と色々な構成法

…^\hyp)`$ はインデックス付き圏〈indexed category〉となります。これは、単純ファミリー構成を $`|\cat{S}|`$ に制限しただけではなくて、$`\cat{S}`$ の(恒等射以外の)射に対応するファミリー射まで定義しています。さらに、インデックス付き圏 $`(\cat{S}^\hyp)`$ に対するグロタンディーク構成を施します。これが $`\cat{S}`$ の(大域的な)ファミリー構成です。$`\quad \mrm{Fam}^\cat{S}(…

スライス圏の大域的な定義: スラッシュ記号の解釈

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

変換手n-圏のブラケット記法

…密〈strict〉なインデックス付き圏〈indexed category〉達の圏を表します。それに対して弱い〈weak〉インデックス付き圏達の2-圏は次のように書けます。$`\quad [\cat{C}^\mrm{op}, {\bf CAT}]_2 := 2{\bf CAT}(\dimU{\cat{C}^\mrm{op}}{2}, \dimU{\bf CAT}{2}) = 2{\bf CAT}(\mrm{Disc2}(\cat{C}^\mrm{op}), \bf CAT)`$…

2階インデックス付き圏と反ラックス余錐

14年近く前の記事「インデックス付き圏のインデックス付き圏」において、インデックス付き圏達が形成する圏が再びインデックス付き圏の構造を持つことを書いています。しかし、インデックス付き圏達のインデックス付き圏へのインデックス付き圏をハッキリと定義することは出来ませんでした。最近、反ラックス余錐を使うと、インデックス付き圏達のインデックス付き圏へのインデックス付き圏の明瞭な定式化が得られることが分かりました。$`\newcommand{\mrm}[1]{ \mathrm{#1} …

状態遷移系としての前層・余前層・プロ関手

…に説明があります。 インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 プロ関手 $`P`$ の場合は、状態空間であるインデックス付き集合のインデキシング集合は次の形になります。$`\quad |\cat{C}^\op\times \cat{D}| = |\cat{C}^\op| \times |\cat{D}|`$もう、気分を出す必要はないでしょうから、$`|\cat{C}^\op| \times |\cat{D}|`$ のまま使います。インデックスは…

Diag構成: 圏論的構成法の包括的フレームワークとして

…u{S}}`$ 上のインデックス付き圏(実体は反変関手)です。インデックス付き圏にグロタンディーク構成をほどこすと平坦化圏ができます。それが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}| `$グロタンディーク構成…

スケマティック系のために: 雑多な予備知識

…ct{S}`$ 上のインデックス付き圏〈indexed category〉になります。Diag構成ときに関手のことを図式と呼び、関手圏を図式の圏と呼びます。この節での「図式〈diagram〉」は関手の意味です。$`\doct{D}, \doct{S}`$ は前節と同じで、ドクトリンとその部分1-圏だとします。ドクトリン $`\doct{D}`$ は了解されている(文脈で前提している)として明示しないこともあります。2-圏 $`\doct{D}, {\bf CAT}`$ の2-…

それでもカン拡張の左右を忘れてしまう

…ン拡張とラムダ計算 インデックス付き圏として 関連する関手・自然変換の名前 右カン拡張とラムダ計算まず、さすがに次は忘れない。 $`\mrm{Left}`$ $`\mrm{Center}`$ $`\mrm{Right}`$ KanのKを L, C, R に置き換えて、取り除いたKを下付きにすると: $`\mrm{Lan}_K`$ $`\mrm{Can}_K`$ $`\mrm{Ran}_K`$ Kは形状関手(後述)の「ケ」とも憶えられます。$`\mrm{Can}_K`$ は、関…

関手の表現可能性と、要素の圏の終対象・始対象

…。前層の要素の圏は、インデックス付き圏のグロタンディーク構成〈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)`$ 達をすべて寄…

レイヤー化ストリング図: スプリット図

…m〉ですが、これは余インデックス付き圏/インデックス付き圏のトータル圏(「最近の型理論: 拡張包括構造を持ったインデックス付き圏」の最初の節参照)の対象・射・等式の描画に有効です。この記事で描画法をもう少し説明します。一般的な余インデックス付き圏/インデックス付き圏を相手にするのは複雑なので、ベース圏〈インデキシング圏〉が順序集合の場合に限ります(ロブスキ/ザンサイ〈Leo Lobski, Fabio Zanasi〉論文もそのようなケースを扱っています)。また、局所圏〈ファイ…

層化ストリング図

…側だけを切り出すと、インデックス付き圏〈indexed category〉です。ただし、最初に余インデックス付き圏(共変関手)を出して、後からインデックス付き圏〈反変関手〉を追加する構成になっています。反変・共変の別で混乱しがちなので、そこを先に片付けておきましょう。明示的に次の反変関手を使います。$`\quad \mrm{Rev}_\cat{C} : \cat{C} \to \cat{C}^\mrm{op}`$ (反変関手)任意の反変関手 $`G`$ は、この反変関手(裏返…

最近の型理論: 拡張包括構造を持ったインデックス付き圏

…圏に共通する構造を、インデックス付き圏として定式化できます。ファミリー付き圏は拡張包括構造〈extension-comprehension structure〉を持ちますから、インデックス付き圏に対しても拡張包括構造を考えることにします。$`\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \ne…

前層の一般化: 述語、ファミリー、モナド、インデックス付き圏を統合

…を見ると、2-前層はインデックス付き圏〈indexed category〉の別名のようです。インデックス付き圏の定義 https://ncatlab.org/nlab/show/indexed+category を参照すると、2-圏である $`{\bf Cat}`$ を余域とする反変2-関手を2-前層と呼んでいます。ということは、単なる前層は1-前層ということになります。1-前層と2-前層の定義に倣って、n-前層は、n-圏である $`(n - 1){\bf Cat}`$ を余…

最近の型理論: デカルト閉圏の外部化・内部化とスノーグローブ現象

…もよい)、次のようなインデックス付き圏 $`\cat{P}`$ を作ります。$`\quad \cat{P}[\hyp] := {\bf CAT}(\J(\hyp), \cat{C})\;\in |{\bf CAT}|`$$`\cat{P}`$ は $`\cat{C}, \cat{D}`$ から決まるので、必要があれば次のように書きます。$`\quad \cat{P} = \cat{P}_\cat{C}^\cat{D}`$$`\cat{P}`$ を定義するために出てきた $`\…

最近の型理論: 型判断/シーケントの意味論に向けて

…ング構成 デカルト・インデックス付き圏の変形 1 デカルト・インデックス付き圏の変形 2 意味的シーケントの意味 シリーズ・ハブ記事: 最近の型理論: 宇宙と世界、そして銀河 基本概念「依存型理論で述語論理が出来てしまう理由」で導入した概念を手短に復習します。記号 $`U, \cat{C}, \cat{D}, \cat{P}`$ は、次のような意味だとします。 $`U`$ : グロタンディーク宇宙。$`{\bf Set}, {\bf SET}, {\bf Cat}, {\bf…

最近の型理論: 依存型理論で述語論理が出来てしまう理由

…完備性 ファミリーのインデックス付き圏 射影と随伴トリプル系 おわりに シリーズ・ハブ記事: 最近の型理論: 宇宙と世界、そして銀河 はじめに「階層化された宇宙達を備えた型理論」のヨーガ〈基本教義〉は、 型は宇宙の要素である です。が、「宇宙より銀河」(「最近の型理論: 型理論の構文論と意味論」参照)というキャッチフレーズにより、我々は以下の解釈を採用します。 型は銀河(という圏)の対象である 銀河はデカルト閉圏だとすれば、単純型理論〈simple type theory〉や…

一般化されたファミリーの圏

…合圏をベース圏とするインデックス付き圏〈indexed category〉になります。インデックス付き圏はグロタンディーク構成ができます。インデックス付き圏のグロタンディーク構成については過去にだいぶ書いています。 「グロタンディーク構成」のブログ内検索 2つだけ記事を挙げるならば: インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 インデックス付き圏 $`{\bf Fam}[\hyp](\cat{D})`$ の標準的なグロタンディーク構成は次のように…

最近の型理論: 宇宙と世界、そして銀河

…拡張包括構造を持ったインデックス付き圏 関連記事: 射ファミリーと圏論的コンビネータ 圏の束構造と包含的圏 一般化されたファミリーの圏 自然言語混じり形式証明の意味論と最近の型理論 宇宙と世界語感としては、世界より宇宙のほうが広い感じがしますが、ここでは、世界は宇宙(と後述の銀河)の集まりだとします。$`\mathscr{W}`$ がひとつの世界〈a world〉だとすると、世界 $`\mathscr{W}`$ のなかにはたくさんの宇宙が入っています。宇宙のなかでも特に重要な…

述語論理: シード付き二重圏 -- 訂正と再論

…論理代数を対応させるインデックス付き圏 $`\cat{P}:\cat{C} \to {\bf Cat}`$ からなります。その他の構成素もありますし、色々な条件が付きますが、主役は $`\cat{P}:\cat{C} \to {\bf Cat}`$ です。二重圏的ハイパードクトリン〈double categorical hyperdoctrine〉とは、ハイパードクトリンにおける主役を置き換える試みです。二重圏 $`\cat{D}`$ を構成し、二重圏からの2つの二重関手$`…

述語論理: 二重圏的ハイパードクトリン

…のです。 述語論理とインデックス付き圏と限量随伴性 順序集合のカン拡張と特徴述語論理 $`\cat{C}`$ をハイパードクトリンのベース圏とします。通常、$`\cat{C}`$ はデカルト圏であると仮定します。つまり、$`\cat{C}`$ は直積と始対象を持ちます。直積の第一射影 $`\pi_1`$ を単に $`\pi`$ と書くことにします。$`\quad \pi_{X, Y}: X\times Y \to X \In \cat{C}`$この射影ごとに述語論理のモデルが…

2-コンテナ

…合の総和)の代わりにインデックス付き圏のグロタンディーク構成を使います。2-コンテナ〈2-container〉とは次の形の2-関手だとします。$`\quad \cat{A} :\cat{I}\!\uparrow_2 \to {\bf CAT} \In \mathbb{2CAT}`$ここで、$`\cat{I}\!\uparrow_2`$ は、圏 $`\cat{I}`$ を2-離散2-圏(すべての2-射は恒等射)とみなした2-圏です。$`\cat{A}`$ は、とても大きい2-圏…

集合圏における依存カリー同型

…category〉とインデックス付き圏〈indexed category〉のあいだのグロタンディーク同型になります。「依存集合←→ファミリー」の対応は、グロタンディーク同型の0次元バージョンと言えます。依存カリー同型依存カリー同型の主張を先に書いてしまうと:$`\quad {\bf DepSet}[I](X \rtimes I, \sum_I F) \cong {\bf Set}(X, \prod_I F)`$$`\sum_I, \prod_I`$ は、シグマ型構成とパイ型構…

述語論理: ベース圏と論理代数の圏

…f Cat}`$ はインデックス付き圏〈indexed category〉になります。必要があれば、インデックス付き圏に関する技法、例えばグロタンディーク構成(「 インデックス付き圏のグロタンディーク構成 」参照)を使うことが出来ます。グロタンディーク構成を通じて、ハイパードクトリンをファイバー付き圏〈{fibred | fibered} category〉とみなすと、ベースの対象 $`X`$ 上の論理代数 $`\mrm{Pred}[X]`$ はファイバーになります。なので、…

モナド: 随伴系の圏の上のインデックス付き圏として

…圏を対応させる関手=インデックス付き圏の話をします。これは、10年近く前2012年4月の記事「またインデックス付き圏が出てきたけど、これはどうなっている?」のコメント欄でksさんに教えていただいたことをまとめたレポートです。とても遅れたレポートです。ksさん、その節はありがとうございました。内容: 概要 セットアップ 随伴系の圏 随伴系の圏上のEnd関手 厳密モノイド圏の内部モノイドとMon関手 モノイド/モナドの保存 モナドのインデックス付き圏の構成 概要10年前の過去記事…