…たくさん出てきます。グロタンディーク宇宙達／型宇宙達／型銀河達の全体の“形状”を記述する有向グラフがユグドラシルです。（北欧神話に登場するユグドラシル〈世界樹〉は、「世界を体現する巨大な木」とのことです。）様々な宇宙達／銀河達は、何本かの塔に編成されます。主要な塔は6本です。 グロタンディーク宇宙の塔 コア銀河の塔 族銀河の塔 述語銀河の塔 データ型宇宙の塔 命題宇宙の塔 この記事では、グロタンディーク宇宙の塔とコア銀河の塔の2本の塔だけを説明します。2本の塔と、それらを“横…

…解釈 その2 // グロタンディーク宇宙」で例に挙げたように、「集合」という言葉の意味・用法を、デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の小さい集合だと合意している文脈を $`V`$ とします。この文脈においては：$`\quad \BR{\T{集合 as 一般名 w.r.t }V } = \BRG{\T{集合 w.r.t }V} = \mbb{U}`$ 文脈 $`V`$ において、一般名「集合」の意味・用法はハッキリしています。では、「要素」という言葉はどう…

…o } `$内容： グロタンディーク宇宙 名前の意味関数とは？ 文脈の考慮 意味領域の考慮 グロタンディーク宇宙「名前の解釈： 正確なコミュニケーションのために」で意味関数〈解釈 | 意味割り当て〉を導入しました。意味関数も関数なので、域と余域を持ちます。まず余域を考えます。意味関数の余域はグロタンディーク宇宙（と呼ばれる集合）と考えます。ひとつのグロタンディーク宇宙で足りないときは、幾つかのグロタンディーク宇宙を一緒に考えます。グロタンディーク宇宙の直積やベキ集合も使ってか…

…、選ばれて固定されたグロタンディーク宇宙 $`\mbb{U}`$ だと思えばいいでしょう。例えば、$`\BRP{\T{実数} \sqrt{2}}`$ や $`\BRP{\T{自然数全体の集合}}`$ は、グロタンディーク宇宙 $`\mbb{U}`$ のなかに固有特定のモノとして存在しています。$`\quad \BRP{\T{実数} \sqrt{2}} \in \mbb{U}\\ \quad \BRP{\T{自然数全体の集合}} \in \mbb{U} `$ 名前 $`\sig…

…在の（デフォルトの）グロタンディーク宇宙 を $`\mbf{U}`$ とします。グロタンディーク宇宙については以下の過去記事達を参照してください。 グロタンディーク宇宙って何なんだ？ （導入的解説） 贅沢主義者のグロタンディーク宇宙 ZF宇宙、グロタンディーク宇宙、型宇宙 （型理論との関係） 構文コンストラクタ〈syntactic constructor〉 $`C`$ は、現在のグロタンディーク宇宙の直積上で定義された部分関数です。$`\quad C : \mbf{U}^n …

… `$内容： 設定 グロタンディーク宇宙と論理式の相対化 等力関係 順序数の復習 誘導充満部分圏、本質的に広い部分圏 基数の定義と性質 基数達の圏と基数割り当て おわりに 設定設定は「順序数と集合圏」と同じなので、「順序数と集合圏 // 設定と基本概念と注意事項」を読んでください。以下、幾つかの追加事項を書きます。「順序数と集合圏」と同様、重要な概念・用語だがこの記事内では説明してないものを青い文字で書きます。カレントのグロタンディーク宇宙 $`\U`$ の外側の宇宙を $`…

…出した小宇宙、つまりグロタンディーク宇宙（「贅沢主義者のグロタンディーク宇宙」参照*1）を使います。適当なグロタンディーク宇宙を選んで固定します。選んだグロタンディーク宇宙を目立つフォントで $`\U`$ と書くことにします。$`\U`$ は、デフォルトあるいはカレントの作業宇宙〈working universe〉となります。$`\U`$ をホストしている外側の宇宙（$`\U \in \mathbb{U'}`$ 「曖昧性を減らす： Diag構成を事例として // 世界の構造」…

…います。階層化されたグロタンディーク宇宙達を使って合理化〈正当化〉できなくもないですが、サイズを縮めたい。以下にサイズ縮小法を書きますが、サイズ問題が気にならないなら無視してください*1。小さい部分集合だけからなるベキ集合（むしろベキクラス）を $`\mrm{SmallPow}(\hyp)`$ とします。無条件の $`\mrm{Pow}(\hyp)`$ よりは $`\mrm{SmallPow}(\hyp)`$ のほうが不安感は少ないのでコッチを使います。$`\T{functi…

…達の集合を含む最小のグロタンディーク宇宙のサイズを 0 とします。上の表の $`\mbf{Univ}`$ がサイズレベル 0 のグロタンディーク宇宙です。$`|\mbf{Set}| = \mbf{Univ}`$ です。さて、圏論的世界のグリッドの対角線*1をたどっていきます。$`\quad 0\mbf{Cat}_{\#0},\;1\mbf{Cat}_{\#1},\;2\mbf{Cat}_{\#2},\;3\mbf{Cat}_{\#3},\; \cdots`$ 最初の3つだけを…

…作業用の小さな宇宙〈グロタンディーク宇宙〉の中で議論するので、現状の作業用宇宙〈current working universe〉を $`U`$ として、次のようにも書けます。$`\quad \forall z\in U.\, z\in x \Iff z \in y`$ イコールがこの定義だと、「$`x, y`$ が集合でない場合はどうなるんだ？」と心配になりますが、現在の公理的集合論では「すべてのモノは集合」なので、そもそも「集合でない場合」は起こりえません。自然数の $`…

…てください。 贅沢なグロタンディーク宇宙とPropositions-As-Types Propositions-As-Typesを曲解しないで理解するために 手っ取り早く解釈したいなら、二値ブーリアンの順序集合 $`\mbf{B}`$ を圏だとみなして、次のように思えばいいです。キーワード $`\T{law}`$ はお気持ち表明なので無視していいです。$`\quad \T{law }\T{i_is_not_next} : 1 \to (\forall x\in U.\, s(…

公理的集合論やグロタンディーク宇宙の公理系では、順序を持たないペアが作れることは保証しています。が、順序を持つペアは頑張って作るのが普通です。作り方は一通りではありません。典型的な順序ペアの作り方を見ておきましょう。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarro…

…いています。 贅沢なグロタンディーク宇宙とPropositions-As-Types Propositions-As-Typesを曲解しないで理解するために 要約しておくと： $`|\mbf{Logic}| = |\mbf{Set}|`$ 、したがって、対象は集合 $`\mbf{Logic}`$ はやせた圏。したがって、2つの対象のあいだの射はあってもひとつ。 $`X \ne \emptyset`$ のとき $`\mbf{Logic}(X, \emptyset)`$ は空集合…

…にサイズが大きくなるグロタンディーク宇宙の系列と、各グロタンディーク宇宙に対する集合圏、さらにはn-圏達の(n + 1)-圏達がグリッド状（下の表のよう）に配置されて世界〈world〉が形成されます。サイズレベルが $`r`$ であるn-圏達を対象とする(n + 1)-圏は $`n\mbf{Cat}_{\# r}`$ と書きます。また、宇宙達は次のように書きます。$`\quad \mbf{Univ}_{\# r} := |0\mbf{Cat}_{\# r}|`$$`r, n`…

…ものと、集合の宇宙〈グロタンディーク宇宙〉を余域とするものがある。 警告は、語彙エントリー内に書くのもありでしょう。複数の用語の組み合わせに関する注意事項は、特定の語彙エントリー内には書きにくいので別ファイルとなるでしょうが。用法や警告以外にも、用語を憶える助けなるエピソードや、関連する人物の情報なども語彙エントリーとは別種のファイルとしてリンクしておけば役に立つかも知れません。学習の方法としての語彙目録作成Obsidianを使って試しに幾つかの語彙エントリーを作ってみたので…

…台集合も許すならば、グロタンディーク宇宙も一種の代数系とみなせます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } %\newcommand{\mbb}[1]{\mathbb{#1} } %\newcommand{\u}[1]{\underline{#1} } \newcommand{\Imp}{\mathre…

…日の記事「非継承的なグロタンディーク宇宙」の最後の節に、ZF集合論の公理達を並べているのですが、あまり読みやすくないですね。論理式も、記法やレイアウトを工夫すると可読性が向上することがあります。やってみましょう。$`\newcommand{\Uin}{\mathrel{\epsilon} } \newcommand{\mbf}[1]{\mathbf{#1} } `$試してみることは： 限量子の直後の '$`\in U`$' の省略 限量子記号 '$`\forall`$' の省…

ここ最近、グロタンディーク宇宙の話をしています。 贅沢主義者のグロタンディーク宇宙 (7月20日) 型・インスタンス・宇宙とタルスキ宇宙系列 (7月22日) 贅沢なグロタンディーク宇宙とPropositions-As-Types (7月24日) ZF宇宙、グロタンディーク宇宙、型宇宙 (7月27日) 今日もグロタンディーク宇宙の話です。通常のグロタンディーク宇宙は、ZF集合論における普通の集合 $`U`$ です。が、$`U`$ のなかでZF集合論ができる集合です。$`U`$ …

…論のなかで定義できるグロタンディーク宇宙でおおよそモデル化できます。が、型宇宙はグロタンディーク宇宙そのものだ、とは言いにくいです。なんか食い違いがある。この食い違いについて考えてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } %\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\u}[1]{\underline{#1} } \…

「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\In}{\text{ in }} `$内容： 「命題」を排除したい！ ベリティ型とその型宇宙 述語 ＝ ベリティ型ファミリー 同義語・曖昧多義語 「命題」を排除したい！「贅沢なグロタンディーク宇宙とPr…

…です。 贅沢主義者のグロタンディーク宇宙 型・インスタンス・宇宙とタルスキ宇宙系列 Propositions-As-Typesというよく知られたキャッチフレーズを、グロタンディーク宇宙の観点からなるべく明確にします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in }} \newcommand{\mbf}[1]{\mathbf{…

「贅沢主義者のグロタンディーク宇宙」でグロタンディーク宇宙の話をしました。贅沢主義か節約主義かは、公理系を設定するときの態度であって、どちらの態度で公理系を設定しても、得られる概念は同じです。ところで、単一のグロタンディーク宇宙ではなくて、宇宙の無限系列を考えることがあります。$`\quad U_0 \in U_1 \in U_2 \in \cdots`$番号を 0 から始めましたが、1 から始めることもあります。番号付け方式の違いはどうでもいい違いです。宇宙の無限系列を、集…

…することがあります。グロタンディーク宇宙の公理系を節約と経済性の原則を無視して再定義してみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\Imp}{\Rightarrow} \newcommand{\hyp}{\text{－} } \newcommand{\dtimes}{\mathop{!…

… U'`$ を2つのグロタンディーク宇宙とします。2つのグロタンディーク宇宙から作られた2つの集合圏を次のように書きます。$`\quad {\bf Set}_U\\ \quad {\bf Set}_{U'} `$デフォルトの宇宙を $`U`$ 、デフォルトより一段大きな宇宙を $`U'`$ と考えて、次の略記をします。$`\quad {\bf Set} := {\bf Set}_U\\ \quad {\bf SET} := {\bf Set}_{U'} `$大きな集合圏 $`…

…ワーキング宇宙であるグロタンディーク宇宙 $`{\bf U}`$ のなかで考えます。つまり：$`\quad |{\bf Odnl}| \subseteq {\bf U}`$$`|{\bf Odnl}|`$ はグロタンディーク宇宙 $`{\bf U}`$ のなかに閉じ込められていますが、$`|{\bf Odnl}|\in {\bf U}`$ ではないので小さい集合ではありません。順序数全体の集合は、$`{\bf U}`$-小集合ではなくて$`{\bf U}`$-クラス（真のクラ…

…書いています。適当なグロタンディーク宇宙を設定するにしても、$`|{\bf Odnl}|`$ は非常に大きな集合（むしろ、非常に長い集合）です。$`|\cat{I}|`$ は小さい集合なので、次の性質を持つ順序数 $`\gamma`$ が存在します。$`\quad \forall i\in |\cat{I}|.\, \mrm{dim}_\cat{I}(i) \le \gamma`$このような順序数 $`\gamma`$ のなかで最小な順序数が一意に存在するので、それを $`\…

…\#r`$ は宇宙〈グロタンディーク宇宙〉のレベルです。大きなサイズが必要なときは、$`r`$ の値を大きくとります。 $`j`$ は切り落とし次元〈truncation dimension〉です。デフォルトは $`j = 1`$ 。$`j = 0`$ のときモデル空間は単なる集合になります。 例えば、モノイドを「指標」と呼ぶことにして、編入子は、モノイドを単一対象の圏とみなす関手だとします。$`\quad J : {\bf Mon} \to \dimU{\bf CAT}{1…

…ズに関しては、宇宙〈グロタンディーク宇宙〉のレベルを $`r`$ として、レベル $`r`$ の宇宙で定義された“n-圏達の(n+1)-圏”は次のように書きます。$`\quad n{\bf Cat}_{\#r}`$デフォルトの宇宙レベルを決めて、文字種〈フォント〉により宇宙レベル（サイズの基準）を区別する書き方も使います。以下は、「ファミリー構成モナド： 大規模構造の事例として // 一般化されたファミリーとその圏」からコピーした表です。 $`r = d `$ $`r = d…

…。圏のサイズについてグロタンディーク宇宙の系列（「最近の型理論： 宇宙・世界・銀河 もう少し」の前半参照）から、デフォルトの宇宙 $`U`$ と、$`U`$ の次の宇宙 $`U'`$ を取り出して考えます。$`U`$ の要素を小さい集合〈small set〉といいます。$`U'`$ の要素を大きい集合〈large set〉といいます。次は成立しています。$`\quad U \in U'\\ \quad U \subset U' `$定義より、「小さい集合は大きい集合です」。自…

…。つまり、どの宇宙〈グロタンディーク宇宙〉のなかでも関手という概念は一律に通用するのです（宇宙多相〈universe polymorphic〉な定義が可能）。言い方を変えると、関手を定義する行為には、サイズの違いは影響しません。関手 Fam特定固有な関手 $`\mrm{Fam}`$ を定義するために、その対象パート $`\mrm{Fam}_0`$ から定義します。何を定義すべきか（主題）を、先に $`\Subject`$で宣言して、それに続けて実際の定義を書くことにします。$…