線形等式的法則〈linear equational law〉に関しては、障害子〈obstructor〉を考えることができる。あらゆる法則に関して障害子を考えてみる。たぶんいいことある。階付きベクトル空間の自己射で、次数1のものをアップ作用素と呼ぶ。アップ作用素を備えた階…

例： 交換法則に対する障害子は交換障害子＝交換子例：ライプニッツ法則に対する障害子はライプニッツ障害子〈Leibniz obstructor〉

これまたグロタンディーク起源らしいが、http://www.kurims.kyoto-u.ac.jp/EMIS/journals/AM/09-4/roger.pdf に何気なくちょっと書いてあった代数的微分作用素〈algebraic differential operator〉。Aは階付き可換代数とする。次数〈階数 degree | grade〉r…

https://www.youtube.com/watch?v=d0i5TItVc0E インポルタント important パルテチオン partition アクシオン action フォルエクサンプル for example チャプタル chapter インパルティクラ in particular スタンダル standard フォルマル formal

紆余曲折の結果、座標 に伴う微分を と書くことにした。紆余曲折は、 フレーム成分とフレーム全体の関係は： 接ベクトル場と微分作用素のオーバーロードが非常に紛らわしいのだけど、次のルールで区別する。 単に と書いたときは、接フレーム場／接ベクトル…

Twitterでつぶやいていた内容の一部をメモにしておこう。無名指標と入れ子指標無名指標または指標リテラルは、sig {...} の形で書く。 sig { sort U operation e:ε → U operation m:(U, U) → U }これはモノイド指標（monoidal signature、「モノイドの指標」…

"Canonical Structures for the working Coq user" by Assia Mahboubi, Enrico Tassi （https://hal.inria.fr/hal-00816703v1/document）の最初の段落： One of the key ingredients to the concision, and intelligibility, of a mathematical text is the …