inductive foo : Type := | bar : foo | baz : foo と書きたくなるが、:= は要らない。なぜなのだろう？[追記]match/with/end の省略と同じみたいだ。[/追記]

演算子の構文 前置： ￢A, -x 後置： n!, f' 微分 中置： いくらでも例はある 右項囲み： f(x) 適用 a[i] インデックス適用 両項囲み： (x, y) 内積, (x|y) 内積, <x|y> スカラー積, (C, D) 旧カンマ圏 右上付き： x2, f*, AT, x-1, f' 微分 右下付き： f*, f∪ 三</x|y>…

内積を持つ3次元空間の特殊事情がある。 V*の要素（コベクトル）が、内積によりVの要素とみなせる。 外積空間 V∧V の要素が、ホッジ双対によりVの要素とみなせる。 SO(3)のリー環である歪対称行列〈反対称行列 | 交代行列〉の空間がたまたま3次元なので、適…

集合・構造 要素 ゲージ群 ゲージ群元 ゲージ変換群 ゲージ変換 ゲージ関数群 ゲージ関数 主バンドルアトラス ゲージ（チャート） バンドルセクション空間 ゲージ（セクション） 集合とその要素がゴチャゴチャ、局所的な議論と大域的な議論が区別されてない…

けっこう深刻。 線形代数 多様体 線形写像 なめらかな写像 部分ベクトル空間 部分多様体 線形同型射 なめらかな同型射 線形埋め込み なめらかな埋め込み 線形ベクトル場 ベクトル場 線形コベクトル場 コベクトル場 線形フロー フロー ベクトル場／コベクトル…

とあるテキストによると: ウーム、、、これで誰が分かるのか？とりあえず、点Pは多様体上の点だから、それを書けば： 分子の が意味不明。詳しく言えば： とは何か？ このたし算はいったいなんだ？ 引き算はなんだ？ 要するに、たし算記号／引き算記号という…

雑多だが大事だと思うことを順不同で。 多様体とアトラス Mが多様体だとは、M = (UM, AM) と書ける。UMはMの台位相空間〈underlying topological space〉で、AMはMのアトラス集合。次のようにも書く。 M = (X, Atlas(M)) Xは次のような性質が要求される。 ハ…

Fが共変関手、Gが反変関手のとき、F(f) = f*, G(f) = f* という略記を、F, Gが何でもお構いなしに使う。 例：接関手をTとすると、T(f) = f*、前送りもf*、引き戻しは f* F(f)は単にfと書くこともある。f:X→Y, g:Y→Y として、gによる前送りg*を単に g とかい…

接写像とヤコビ行列（微分係数）の関係を、一般のバンドル射と微分形式に拡張する。バンドルの底空間の写像fで誘導される引き戻しバンドルを f#F で表す。f= (ftop, fbase):(E→X)→(F→Y) がバンドル射とする。このとき、fのヤコビ表示〈Jacobian presentation…