気休め語〈consolation word〉で印象が変わる、という大問題。逆に、気休め語を分析する。 キーワード無し構文 - (新) 檜山正幸のキマイラ飼育記 メモ編 列挙。随時追加予定。 オフィシャル構文 気休め語 1-σ signature, class, typeclass, specification, i…

反変ベクトルと共変ベクトル -- これはイカンわ、ダメなヤツだわ。因習的微分幾何や物理で出てくるヤツ。まったく分からんヤツ。とりあえずは、特定のベクトル空間Vに対して、Vの要素が反変ベクトル、Vの双対空間の要素が共変ベクトル。が、ベクトル空間はフ…

多様体上では、「変数xに関する微分」は意味を持つ。が、「変数」は「関数」の意味で、「多様体上の座標成分関数xに対する微分」が意味を持つ。 変数＝座標成分関数 という記号はダメな記号だ。もう使わないほうがいい。 でよい。の使い所は限定的で： 標準…

既存の記法が酷すぎる。代替記法。 例1 → 例2 → 例3 → は、C∞(Rn, R)→C∞(Rn, R) という作用素（関数を入力して関数を出力する）。代替記法の略記とメリット： は、 でもよい。 のnは省略してもよい。例： 。 は、 でもよい。 は導関数、 は微分係数（導関数…

関数、写像、演算{子}?、作用{素}?、変換、{値}?割り当て、インデックス族、対応

X, Y∈Der(A)、f, g∈A のような記号を使う。X:A→A で、ライプニッツ法則を満たす。微分適用Dとリー括弧Lは、 D:Der(A)×A→A, D(X, f)∈A L:Der(A)×Der(A)→Der(A), L(X, Y)∈Der(A) 一般に、f:A×B→C が二項演算のとき、 f = f(-, -) 右カリー化 f∩(-) = f(-):A→[B…

[n] = {1, ..., n} が作る集合・写像の圏 アミダ図の圏と置換（代入ではない）の圏 1,0を持つ半環係数の行列圏 ラベル付き boxes-and-wires 図の圏 ルシアン・アーディ図〈Lucian Hardy〉 一般論 インデックス付き圏としてのブール行列圏 弱いトポスとしての…

ベクトル場と導分の対応は、可微分性補題が鍵だと分かった。まず、言葉の準備。 {偏}?微分係数 {偏}?導関数 {偏}?微分作用素 点導分 P, Q 領域導分 X, Y 対応は、 代数的・公理的 解析的・具体的 点導分 微分係数汎関数 領域導分 微分作用素 古臭いが、 汎関…

ベクトルバンドルの手前の概念で、ベクトルファミリーを定義する。 位相空間の各点にベクトル空間が付いている。 各ベクトル空間は有限次元ですべて同型（標準的同型ではない！） 個々のベクトル空間には位相があるが、全体としての位相はない。 ベクトルフ…

単なる集合からグラフを作る方法。 一端アロー化： Aに⊥を加えて、⊥→a （a∈A） をアロー＝有向辺 として足す。Aとアローは1:1に対応。 ニ端アロー化： Aに⊥, T を加えて、⊥→a→T （a∈A） をアロー＝有向辺 として足す。Aとアローは1:1に対応。 ループ化： ⊥を…

本編の 微分はライプニッツ法則に支配されている - 檜山正幸のキマイラ飼育記 (はてなBlog) の拡張として、ベクトル場と関数環の導分の対応がある。しかし、単なる代数的導分ではどうもうまくいかない。「導分←→ベクトル場」対応ではなくて、「導分層←→ベク…

アダマールの補題ってのがある。 https://ncatlab.org/nlab/show/Hadamard+lemma これは、テイラー／マクローリン展開の精密化になっているから、アダマール形式のテイラー／マクローリン展開と言っていいと思う。アダマール商を作用とみなして、アダマール…

Sets-as-Types, Functions-as-Terms Algebra-as-Types, Morphisms-as-Terms Coalgebra-as-Types, Morphisms-as-Terms Categories-as-Types, Functors-as-Terms Propositions-as-Types, Proofs-as-Terms Sets-as-Types と (Co)Algebras-as-Types は、単純型＝…

親子関係で入れ子になった指標＝ジニアロジーの書き方はまだ試行錯誤だけど、ともかくも、いくつかの論理的概念の定義を試みる。 3-signature { sort LoicalCat 2-signature { /* Cは論理的圏の構造を持った圏 Cでは、対象定数_Bや指数ベキが意味を持つ。 */…

備忘録。kは0以上の整数とする。使う記号。 記号 意味 in アンビエントアビタを示す from 構成のソース指標 to 構成のターゲット指標 k-σ k-指標 k-γ k-構成 k k-射の宣言 :k k重のコロン →k k重の矢印 := 割り当て記号 ( ) パラメトライズ ( ) 気休め語〈co…

備忘録。指標内で項を使ってよい。項は、プロファイルのなかで使える。ただし、当該の宣言文が出現する前に登場した（提供された）基本記号と、メタ指標（指標の指標＝親指標）のメタ記号を使って構成される項に限る。一方で、構成〈construction〉でも項は…

超越的等号： 実質的に集合論の等号 (n+1)-射：n-圏の(n+1)-射としての等号 述語 ： トポスにおいて、対角射 ΔA:A→A×A の特性射 eq:A×A→Ω。

後で追加修正するかも。指標の一覧： 名前 提供記号 ひとこと Magma * 乗法記号使ったマグマ UnitalMagma *, 1 単位的マグマ MonoidAste *, 1 モノイド MonoidPlus +, 0 モノイド Group *, 1, ~ 群 AbGroupPlus +, 0, - アーベル群 Ring +, 0, -, *, 1 可換…

あまりにも車輪の再発明が凄まじ過ぎて、用法や雰囲気（だけ）が違う同義語が山のようだ。少し整理しておく。基本レベルとは圏の次元を基準としたレイヤー番号のこと。基本レベルが1の存在物〈スタッフ〉はレイヤー1にいて、存在物の圏論的次元は1。 基本レ…

_R のような下線で始まる語は太字の代替で、固有名詞（特定インスタンスを指す名前）となる。次元ごとに付けるキーワードは恣意的なので括弧に入れることにした。 1-sinature movable { 0(sort) S in _Set 1(mathod) moveBy:S×_R→S in _Set 2(equation) assc…

型階層を考える上で、型を分類する必要がある。 型と種 無構造型（集合）と構造付き型 単純型〈基本型 | 組み込み型〉と複合型〈構成型 | 複雑型〉 全域型と部分型〈制約型〉 型と種は縦階層。縦階層は、オブジェクトレベル、メタレベル、メタメタレベルのよ…

また裏紙に描いた絵。これは、型付け〈タイピング〉を一般的に考えるときのテンプレートで、kを決めて使う。kをズラしながら使うこともある。これで、無限階層の型理論が考えやすくなるぞ。だいぶ分かりやすい。

カテゴリー「セオリー論」 カテゴリー「インスティチューション」 「インスティチューション」の検索 「ハイパーインスティチューション」の検索 「リテラチャ」検索

階層的世界のレイヤー0がハッキリしてきた（0-指標＝集合の内包的記法 ！ - (新) 檜山正幸のキマイラ飼育記 メモ編参照）ので、自分の世界観（世界観と世界の中心線 - (新) 檜山正幸のキマイラ飼育記 メモ編参照）に確信がわいた。セオリーは世界のなかにラ…

分かったぞ！！ レイヤー1 1-指標 1-モデルの1-圏 アンビエントの1-圏 レイヤー0 0-指標 0-モデルの0-圏 アンビエントの0-圏 レイヤー0が不明だったが、 0-指標とは、集合の内包的記法 アンビエント 0-圏とは、内包的記法のコンテキスが定義するドメイン 0-…

世界がどうなっているのか、に対する期待、想定、要求などが世界観だ。世界観は多様であってよい。世界に、その中心線、あるいは幹、あるいは中心タワー〈ユグドラシル〉があると想定する。中心線の選び方も恣意的だ。が、利便性から選ぶと、 デカルトモノイ…

n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編に書いてあることが我ながら凄いな。なんで気付いたのだ？最近とは用語法・記法が違うので対応表。 過去 最近 Σk kΣ Ak kA k-Spef[-] (-)-kSig k-Mod[-] (-)-kAlg Ck なし Ck…

[追記]今まで、記号／スタッフのアビタ（直接所属する圏）とアンビエント（アビタのアンダーライイング圏）を識別できてなかった気がする。[/追記][さらに追記]アビタはやめて「クラス」というありきたりの用語にした。「クラス」と「インスタンス」をペアで…

紛らわしい！ habitat 生息地 アビタ(仏) habitant 住人, 居住者 アビトン(仏) 住人はinhabitant（英語）でも同じだから、「インハビタント」を使う。 生息に関して habitat 生息地, 生息域 アビタ habitation 居住, 住所, 居住地, 集落 アビタシオン 居住に…

裏紙にテキトーに書いたから汚いのだが：(http://www.chimaira.org/img4/algebraic-ladder.png)いくつか間違っている： Σ3, Σ2, Σ1 は、3Σ, 2Σ, 1Σ 。 2C, 1C, 0C は、3A, 2A, 1A のほうが良かった。 下から、レイヤー1、レイヤー2、レイヤー3の代数的レイヤ…