globular
本編で次の記事を書いた。 Globularのサンプルを追加： 随伴関手対と双対ベクトル空間対 - 檜山正幸のキマイラ飼育記 このての話のベースは、メイト定理だ。 https://ncatlab.org/nlab/show/mate nLabのこの記述は分かりにくいが、2-セルに関する絵を描けば…
tensoratorって、モノイド圏における交替律の制限された形を与える同型射（自然同型）のことなんだね。http://arxiv.org/pdf/q-alg/9703033.pdf の3ページの後半にある式を見ながらGlobularでtensoratorの絵を描いてみた。一番下のサムネイルを見れば、何を…
結合律、フロベニウス律、特殊性（no-hole条件）からパヒナー（Pachner）移動が出てくることは、このダイアリーのどこかに書いておいたと思う。[追記]三角形を細分しても計算結果は同じにできる - 檜山正幸のキマイラ飼育記 メモ編 だった。[/追記]結合律の…
クリックでリライトが発生することがあるが、何が起きたか分からないことがある。リライトを引き起こすセルを、そのリライトのトリガーセルと呼ぶことにすると、リライトとトリガーセルの関係は分かりにくい。トリガーセルはあくまでトリガーであって、その…
例： Create A, B, C, D Create f:A->B, g:B->C, h:A->C, k:C->D, j:B->D Create α:: f*g => h : A->C Create β:: j => g*k : B->Dβにヒゲ結合で、fを付ける。 f*β:: f*j => f*g*k f*βのターゲットの右部分 f*g と αのソース全体 f*g が一致する。 βの境界の…
双対的に反転してコピーする機能 方向の切り替え。やっぱり、上から下がいい。 描画次元が0のセルを有限な大きさ（矩形、方体）で表示する。 交替律の適用の自動的な最適化 より一般的なペースティング可能箇所の検出 プレースホルダを含むテンプレート図形…
「globular, 課題」というタグの組み合わせで、あると良さそうな機能を書く。具体的にどうするかは分からなくても、とにかくメモしていく。 ラベル以外に何らかのコメント、ドキュメンテーション 記録したワークスペースのソート、特に日付順。今、日付がよ…
描いた図形を一時的に保存して後で使いたいとき。 Theoremでパレットに入れる。 一時的だから名前を付けなくてもいい。 パレットに入ったサロゲートをSelectする。 サロゲートをクリックすると、リライターが動いて定義が展開される。 Restrictで見えている…
Projectカウンターの番号は、射影のファイバーの次元となる。これは、元図形と射影図形の次元の差。埋め込みではないので余次元というのはオカシイ。適切な言葉がないが、情報がどの程度落ちるかを示す。数が多くなると、それだけ情報が落ちて粗雑になる。Pr…
主結合 -- target(S) = B = source(T) のときに、Bを接着セルとして結合する。 複結合 -- targetk(S) = B = sourcek(T)、k＜(n - 1) のときに、Bを接着セルとして結合する。 ヒゲ結合 -- 次元の異なるセルの結合。次元の小さいセルからは主結合に見える。つ…
あ、そうそう。Globularの物凄くイライラするところ - 檜山正幸のキマイラ飼育記 メモ編 -- なんでそう思ったかを書く。ニョロニョロ関係があるとき、ホムセットの同型としての随伴が出る。それを証明する。n-セルであることを :n で示す。-[-]- はペーステ…
「なにかチョットやってみた」とかのスニペットをブログ・エントリーに貼り付けたり出来ないこと。そもそもソースコードとかスクリプトというものがなくて、ワークスペースのスナップショットを保存出来るだけ。publishすればワークスペースのスナップショッ…
Globular探り 16：可換モノイド - 檜山正幸のキマイラ飼育記 メモ編 定理が正しいことの確認はたぶん次の2つの段階がある。 行為として、前提から結論に至る遷移系列を経験する。 その行為の経験を、空間化／図形化／対象化する。 これは、 カメラが回ってな…
n-キューブ＝[0, 1]nをn-キャンバスとも呼び、n-キャンバスに描かれた図形＝ダイアグラムを考える。n-キャンバスの座標のひとつ（1≦i≦n である番号iで識別）を選んで、それを時間軸とみたとき、時間軸とダイアグラムの組をストーリーと呼ぶ。x = (x1, ..., x…
イントネーションの関係から、「グロービュラー」より「グロビューラ」のほうが近いみたい。「ビュ」のあたりを強く発音する。
http://globular.science/1601.004v1 随伴対の左側にコモナド構造があるとき、右側にモナドを作れる。[追記] http://globular.science/1601.004v2 （間違いの訂正） [/追記]
日本語を入れるとダメだった。日本語なしに書き換えて公開したらロードできた。 http://globular.science/1601.003v2 http://globular.science/1601.003v3 v2は公理のみ、v3は定理をひとつだけ証明。v2の公理群は見ればわかると思うが、定理の証明がすぐに忘…
試しにpublishしてみたが、 http://globular.science/1601.003 http://globular.science/1601.003v1 保存したワークスペースのロードができない。
Globular探り 10：定理と証明 - 檜山正幸のキマイラ飼育記 メモ編で「定理と証明」の話をしたけど、あれは伝統的な「定理と証明」の枠組みに依拠している。ほんとのところ、Globular内では伝統的な「定理と証明」なんてありゃしない。伝統的な概念に慣れてい…
globularタグを付けたので、今後はタグでglobular関係を識別する。
次の論文がけっこう参考になりそう。絵が豊富だし、説明も丁寧。 Title:Higher-dimensional categories with finite derivation type Authors: Yves Guiraud, Philippe Malbos URL: http://arxiv.org/pdf/0810.1442v2.pdf Pages: 54p Yves Guiraudってどこか…
モースレベルがシーン（スチル、フレーム）の順序番号を与え、トランジションが隣り合うシーンの移動（move）となる。よって、シーンは証明過程の各段階のスナップショットであり、トランジションは証明ステップとなる。基本トランジションは基本推論、アニ…
定理と証明の関係がよく分からなかったが、そもそもが曖昧だった。ハッキリさせる。定理に関連して3つの概念を導入する。 あるnに対するn-セル（n-ダイアグラム）を命題と呼ぶ。 A, Bを命題として、s:(n + 1) A→B という(n + 1)-セルをステートメントと呼ぶ…
モノイド圏のなかのフロベニウス代数の公理を全部書いてパレットに入れて、フロベニウス代数電卓みたいのは作れそうだ。だいたいはやってみた。現状だと、Workspaceの保存とエクスポートはできるが、リジューム／インポートが動かない、と。これだと、なんと…
参考になるかも。 http://d.hatena.ne.jp/m-hiyama-memo/20070426
n-キューブは、単にn次元ユークリッド空間の標準的なキューブ [0, 1]n のこと。n-キューブを同時に一挙に把握できる幾何学的な空間と捉えるときキャンバスと呼ぶことにする。キャンバス内で時間は流れない。一方、[0, 1]n-1×[0, 1] と分解して、最後の次元を…
射影した図の色塗りに間違いがあるようだ。どっちにしても、射影図のキャンバスと同じ次元の部分は全く当てにならない。余次元が1以上の骨格は、元の空間では余次元2以上だから、ある程度はトポロジーを反映している。
http://tigger.uic.edu/~rgl/shrtknots.pdf を読んだが、定義が細かすぎると思った。次のように簡略化してよいだろう。 基本イベント（elementary event）→基本1-セル 縁付き基本イベント（framed (elementary) event）→縁付き基本1-セル スチル→直列1セル＝…
1次元以上のキャンバスは、[0, 1]n になる。通常のユークリッド空間内の単位矩形だと思ってよい。このキャンバスはn個の軸を持ち、主方向を持つ。 キャンバス次元 軸 主方向 0 なし なし 1 x x方向 2 x,y y方向 3 x,y,z z方向 4 x,y,z,w w方向 n x1,...,xn x…
定理（theorem）は、公理や定義も含む。名前式 の形に対応する。右辺にも名前が出現するが、その名前はセルの名前。右辺に出現する名前のなかでひとつだけが主セルの名前として特定されている。「名前→式」の展開と「式→名前」の縮約がクリック操作で可能だ…
