i, j, k, l, m, n は 自然 数 とする。 このとき i + k = j + k ならば i = j 証明: まず 述語を定義する: P[自然 数] とは i + $1 = j + $1 ならば i=j であること。 (A1): P[0] ※帰納法のベース 証明: 次を仮定する: (B0): i + 0 = j + 0 。 このとき (B1)…

http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…

名前がないからどうにもならないが、名無し／メタ情報なしでも、 特定シンボル（述語名、関数名、モード名、属性名）を含む定理 特定のプロファイルの特定のシンボルを含む定理 特定のアーティクルで定義された特定のシンボルを含む定理 存在命題、全称命題…

http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、 :: The drinker's principle reserve x for object; ex x st P x implies for y holds P y proof per cases; suppose A0: ex x st not P x; consider a such that A1: not P a by …

the system Declare by D. Syme ？？ 不明 the Mizar mode for HOL by J.Harrison http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html the Isar language for Isabelle by M. Wenzel http://isabelle.in.tum.de/Isar/ Mizar-light for HOLlight by F. Wiedij…

地獄の作業例。 reserve i,j,k,l,m,n for natural number; i+k = j+k implies i=j; proof defpred P[natural number] means i+$1 = j+$1 implies i=j; A1: P[0] proof assume B0: i+0 = j+0; B1: i+0 = i by INDUCT:3; B2: j+0 = j by INDUCT:3; hence thesi…

論理 Mizar ⊥ contradiction ¬φ not φ φ ∧ ψ φ & ψ φ ∨ ψ φ or ψ φ ⇒ ψ φ implies ψ φ ⇔ ψ φ iff ψ ∃ x. ψ ex x st ψ ∀ x. ψ for x holds ψ ∀ x.(φ ⇒ ψ) for x st φ holds ψ nonは形容詞の否定、andとsuch thatはスクリプト言語のキーワード。

Mizarでは同義語はほとんどない。beとbeing, hence（従って）、hereby（これによって）が次の意味。 then + thus = hence thus + now = hereby 英語としてはthus（よって）とhence（従って）はたいして差はない。

連続 離散二値 R, C B 可換環（スカラー） ベキ等可換半環 空間S 単なる集合X 確率分布 ポッシビリティ分布 S上の状態ベクトル空間 Xのベキ集合に合併 バンドル 依存和 バンドルのセクション空間 依存積集合 連続群 モノイド 群代数 モノイドのベキ集合 群代…

Frobenius algebras and monoidal categories Ross Street Annual Meeting Aust. Math. Soc. September 2004 http://maths.mq.edu.au/~street/FAMC.pdf フロベニウス代数の圏でも、ニョロニョロは成立して、それによりフロベニウス代数射が可逆であることが…

ネーミングの選択が難しいのだが、 N値の1-形式＝1-コチェインが問題。一応C1(A, N)でN値の形式＝コチェインを表す。 三角ハイブ上で1-コサイクルを考えることが出来る。コバウンダリ作用素がないが、それでも等式で定義できる。コサイクルが許容状態（addmi…

吸い込み部屋と湧き出し部屋を禁止してるが、許しても議論はできる。ただし、直感性は失われるし、ややこしくなる。許した場合は、乗法と余単位、単位と余乗法の相互関係が必要になるし、そもそもこの相互関係はフロベニウス代数の公理系に入れてもいいもの…

任意の曲面上の三角ハイブ理論は思ったよりも難しい。難しい理由は双対グラフが平面グラフにならないので、平面に射影すると交差が出てきてしまい、その操作に、ブレイド圏や対称圏の議論を必要とする。三角ハイブが最初から平面に埋め込まれていれば、ブレ…

発音できるアクロニム DAFTOC（ダフトック） - 檜山正幸のキマイラ飼育記 メモ編の追加。 形容詞 曲面 有限 コンパクト Directed co-directed Acyclic trended Fluent no-divergent Fat oriented Trivalent triangulated Open End in/out boundary edge/segm…

次の概念を定義する。 箙 反射的箙 s, t, i版 反射的箙 ‖, ◁, E版 半反射的箙 ‖, ◁, E版で、Eを空でもよいとする。 高次の概反射的箙Qは、Q0が半反射的箙、それ以外のQi反射的箙 (Q, ‖, ◁, E)が反射的箙だとは、 ‖はQ上の同値関係 f‖f', g‖g', f◁g ならば、f…

動機は、 任意の整数区間で次元グレーディングされた集合を考えたい。 グレーディングの制限として、上側切り落とし、下側切り落とし、シフト（ダウン／アップ）を定義したい。 同様に、上側延長と下側延長を定義したい。

http://www.cs.ox.ac.uk/people/bob.coecke/andrei.pdf の4章 A 2-Categorical Primer が良いのだが、この文書タイトルがなくて困る。oxfordのandrei君の学位論文らしいことは分かるのだけど。 https://www.cs.ox.ac.uk/people/andrei.akhvlediani/

2つの三角ハイブA, BがZ不変量で区別出来ないとする。そのとき、AからBに至る変形の列がある。その変形は、 パッヒナル移動 三角形と四角形の潰しとその逆 一点接合と切り離し で生成される。と予想している。もっと基本変形があるかもしれないが。

三角ハイブ 基本定理 - 檜山正幸のキマイラ飼育記 メモ編の続き。三角ハイブの圏（実際には単なる圏ではない）上で定義されるC標的な関手が、ある公理を満たすときC標的なZ不変量と呼ぶことにする。Zはzombieから。 Z不変量は、標的圏C内の特殊フロベニウス…

Cをモノイド圏とする。不変量の意味は、定義側の可逆2-セルである変形（deformation）が、標的圏の自明な2-セルに移ること。 三角ハイブのC-標的不変量は、双対DAFTOK図のC-標的ラベリングで、フロベニウス・パッヒナル変形で不変なもので表現できる。 三角…

三角ハイブの構造の階層： 階層1： 図形（2次元コンパクト向き付き多様体） 階層2： 間取りデザイン（三角形分割） 階層3： 一方通行ドアと鍵（双対グラフのdirectionと閉頂点） 内部構造と境界構造： 内部構造：内部の間取り、ドア、鍵 境界構造：入口、出…

文字から先に入ると、音で間違う。 らんこうげ ×ランコウカ こわだか ×コエダカ ろんげ ×ロンモウ おぼつかない ×カクソクナイ たて ×サツジン しにせ △ロウホ（可） ひきすう ×インスウ ぎんえん ×ギンシオ

関手の余域は特に標的圏（target category）と呼ぶことにする。いつもじゃないけど。余域や値という言葉を使うと混乱する場合がある。そんなときに「標的」とする。Cを標的圏とする関手は、C標的関手（C-targeted functor）と呼ぶ。

2次元のパッヒナル移動（Pachner move）は、対角フリップと星状細分／融合の二種類。外枠（ローカル変形の境界条件）となるのは四角形と三角形。これを書き換えルールと考える。ルールが適用される部分複体をリデックス、適用結果はコントラクタムと呼ぶ。こ…

有限有向グラフGに関して、次は同値である。 Gにサイクルがない。 G上の傾向関数（trend function）が存在する。 Gのユークリッド空間Rn+1への進行的埋め込み（progressive embedding）が存在する。 傾向関数の定義は、Gの2頂点a, bがこの順序で有向隣接する…

完全に区別するのは難しいが、 orientation -- 主に多様体上に決まる二値の符号、空間全体の性質。 direction -- 1次元辺に対して決まる二値の符号、辺ごとに局所的。 trend -- DAGに対して決まる、全体としての方向。これをdirectionと呼ぶこともある。 tre…

genus（ジーナス）の複数形がgenera（ジェネラ） stratum（ストレイタム）の複数形がstrata（ストラタ）

三角形ABCで、BCの中点をMとして、「単一三角形ABC」と「ABMとAMC」のあいだがパッヒナル移動で移れない、と思っていたが、これは誤解だ。実際に移れないのだが、 パッヒナル移動はローカル変形である。 ローカルとは、境界条件を指定して、境界とその外側は…

入口境界辺を含む三角形の頂点接合、境界辺は1次元的な接合＝圏的結合 入口境界辺を含まない三角形の一辺接合、または二辺接合 0次元隣接する二辺の自己接合 直和 先に直和を作っておけば、残りの操作はすべて自己接合として説明できる。それはウォーカー流…

三角分割＝パーティショニング・デザイン としての変形 隔壁（septum）の潰し（contraction） 潰しの逆。三価頂点の一辺を(1→1)部屋で置き換え、四価以上の頂点の二辺を2個の(1→1)部屋で置き換え。 対角フリップ 星状細分 星状融合 隔壁（ドアがロックされた…