微分とベクトル/フレーム

\newcommand{\hyp}{ \mbox{-}}%
\newcommand{\sigtype}{\widetilde{\sum}}%
紆余曲折の結果、座標 x に伴う微分Dx と書くことにした。紆余曲折は、

  •  \partial_i \to \partial^x_i  \to D^x_i \to Dx_i

フレーム成分とフレーム全体の関係は:

  • Dx_i = (Dx)_i = \frac{\partial}{\partial x^i}
  •  Dx = \begin{bmatrix}Dx_1 & \cdots & Dx_n \end{bmatrix}

接ベクトル場と微分作用素オーバーロードが非常に紛らわしいのだけど、次のルールで区別する。

  • 単に Dx, Dx_i と書いたときは、接フレーム場/接ベクトル場の意味で、微分作用素ではない。
  • Dx[\hyp], Dx_i[\hyp] と書いたときに限り、微分作用素と解釈する。
  • 特に、 Dx\cdot \xi, Dx_i f などは微分してない!
  • フレームとしての Dx の逆を Dx^\triangleleft = (Dx)^\triangleleft と書く。これはゲージ。
  • Dx^\triangleleft : TM|_{def(x)} \to {{\bf R}^n}_{/def(x)}
  • 微分作用素は、自然数パラメータ k\in {\bf N} に関する多相になる。Dx[\hyp] : \forall{k\in {\bf N}}.(\, \Gamma({\bf R}^{[k]}_{/def(x)}) \to \Gamma({\bf R}[^k_n]_{/def(x)}) \,)
  • 多相パラメータを特定すると、Dx[\hyp]^k : \Gamma( {{\bf R}^{[k]}}_{/def(x)}) \to \Gamma({\bf R}[^k_n]_{/def(x)})
  • 多相パラメータを推論〈エラボレーション〉する前提なら Dx[\hyp]: \Gamma({{\bf R}^{[k]}}_{/def(x)}) \to \Gamma({\bf R}[^k_n]_{/def(x)})
  • Dx から誘導される加群射は  \Gamma(Dx) = Dx_*, \Gamma(Dx^\triangleleft) = {Dx^\triangleleft}_* = {Dx_*}^\triangleleft
  • Dx_* \cdot Dx[\hyp] \cdot (Dx_*)^\triangleleft はベクトル場の共変微分
  • \nabla x^e は、一般のベクトルバンドルのフレーム e: {{\bf R}^r}_{/def(x)} \to E|_{def(x)} から決まる共変微分。これ全体で微分作用素なので、\nabla x^e[\xi] のように作用する。

指標と型クラス 1

Twitterでつぶやいていた内容の一部をメモにしておこう。

無名指標と入れ子指標

無名指標または指標リテラルは、sig {...} の形で書く。

sig {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

これはモノイド指標(monoidal signature、「モノイドの指標」ではない!)で、宣言の区切り記号をカンマにしてもいいように構文を決めておく。プロファイルの左右は原則括弧で囲み、空リストはεでもよい。(U) は U と書いてもよい。略式記法は、

sig {U, e:ε → U, m:(U, U) → U}

カンマ区切りで1行でも書ける。

入れ子の指標〈nested signature〉の例を出す。

sig {
 sig 1 {
   sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

sig {
 sig 1 {
   sort U
   operation e:ε → U
 }
 operation m:(U, U) → U
}

sig {
 sig 1 {
   sig 2 {
     sort U
   }
   operation e:ε → U
 }
 operation m:(U, U) → U
}

規則と注意は:

  1. 部分指標には、1始まりの番号を付ける。欠番はダメ。
  2. 一番外の全体は番号0とする。番号0は書いても書かなくてもよい。
  3. 当面、部分指標の重なりは許さないが、そのうち重なりも考える。
  4. Σが番号で識別された部分指標を持つ指標のとき、Σi で番号が i である部分指標を意味する。
  5. 等式〈equation〉も書けるが、簡単な例では使わない。

無名指標への名前付けは次の形:

PtMagma := sig {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

同じことを次にようにも書く。

signature PtMagma {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

入れ子の指標にも名前付けができる。

signature PtMagma {
 sig 1 {
   sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

まったく同じだが、気分だけの問題で、部分指標を param で指定する。

signature PtMagma {
 param 1 {
    sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

部分指標を指定された指標をパラメータ付き指標〈parameterized signature〉とも呼ぶ。

パラメータ付き指標には極端な例もある。

signature PtMagma0 {
 param 1 {}
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

signature PtMagma1 {
 param 1 {
  sort U
  operation e:ε → U
  operation m:(U, U) → U
 }
}

次は同じ概念。

  1. パラメータ付き指標
  2. 相対指標〈relative signature〉
  3. 部分指標をただ1つだけ持つ入れ子指標

語「パラメータ」が意味的にふさわしくないときがある。そのときは「相対指標」を使う。例えば、レコードの余域となる相対指標をパラメータ付き指標と呼ぶのは奇妙。

指標Σと、その部分指標 Γ⊆Σ で定義される相対指標を Γ.Σ とも書く。空指標を 0 と書くと、0.Σ や Σ.Σ もある。

相対指標 Γ.Σ は、指標の圏の包含射 Γ→Σ in Sig と同一視できるので、アンビエント圏(モデルのターゲット圏の圏)内の射 Mdl(Σ, C) → Mdl(Γ, C) in AMB を定義する。これは忘却射影関手〈forgetful projection functor〉。ここで、Cは任意のターゲット圏(アンビエント圏の対象)。忘却射影関手は次のように略称する。

  • {忘却}?射影{関手}?

レコードとそのプロファイル

レコードは構文的対象物だが、意味的には関手になる。レコードのプロファイルは、2つの相対指標を矢印で区切った形。構文的に r:Γ.Σ ← Φ.Δ だと、意味的には次のようになる。

\newcommand{\cat}[1]{ \mathcal{#1}}
\xymatrix {
  {Mdl(\Sigma, \cat{C})} \ar[d]^{Proj}
  &{}
\\
  {Mdl(\Gamma, \cat{C})}
  & {Mdl(\Delta, \cat{C})} \ar[l]_{F} \ar[d]^{Proj}
\\
  {}
  & {Mdl(\Phi, \cat{C})}
}\\
\mbox{in }{AMB}

Fがレコードrで定義される関手。レコードが、パラメータを持たない完全定義レコードなら:


\xymatrix {
  {Mdl(\Sigma, \cat{C})} \ar[d]^{=}
  &{}
\\
  {Mdl(\Sigma, \cat{C})}
  & {Mdl(\Delta, \cat{C})} \ar[l]_{F} \ar[d]^{!}
\\
  {}
  & {Mdl(0, \cat{C}) = {\bf I}}
}\\
\mbox{in }{AMB}

さらに域側指標が空指標なら、


\xymatrix {
  {Mdl(\Sigma, \cat{C})} \ar[d]^{=}
  &{}
\\
  {Mdl(\Sigma, \cat{C})}
  & {Mdl(0, \cat{C}) = {\bf I}} \ar[l]_{F} \ar[d]^{=}
\\
  {}
  & {Mdl(0, \cat{C}) = {\bf I}}
}\\
\mbox{in }{AMB}

これは事実上、単一のインスタンス


\xymatrix {
  {Mdl(\Sigma, \cat{C})}
  & {\bf I} \ar[l]_-{F}
}\\
\mbox{in }{AMB}

相対指標を射影関手と解釈する事と、それに伴うレコードの解釈はけっこうミソかも知れない。レコードという言葉はCoqやAgdaに合わせた。特にAgdaだと、この意味論が直接的に使えそう。いや、そうでもないか。


後で書く予定:

レコードのメンバー関数コードの定式化には、構文モナドとクライスリ射、システムのコア指標が必要。コア指標のモデル(エンジンと呼ぶことにする)があれば、クライスリ射はモデルを定義する。

射影関手のセクションと、セクションの一般化であるアドホック・セクション。アドホック・セクションが型クラスのインスタンス(の集まり)に相当する。アドホック・セクションとの対比で、通常のセクションをパラメトリック・セクションと呼ぶ。パラメトリック・セクションは、アドホック・セクションの極めて特殊なもの。

多相型と多相関数は、関手と自然変換で解釈して、関手圏の対象と射と考える。すると、多相型と多相関数で作られる多相モデルは関手圏をターゲット圏とするモデル。アドホック・セクションは、多相モデルを決定する。したがって、アドホックセクションの全体は多相モデルのなかに埋め込める。特に、パラメトリック・セクションの像となっている多相モデルはパラメトリック多相モデルで、パラメトリック多相モデルのメンバー関数はパラメトリック多相関数。ここで、メンバー関数は、指標の演算記号に割り当てられる射のこと。

記法の乱用

"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 use of notational conventions and even sometimes the abuse thereof.
These notational conventions are usually shaped by decades of practice by the
specialists of a given mathematical community. If some conventions may vary
according to the author’s taste, most tend to stabilize into a well-established
common practice. A trained reader can hence easily infer from the context of a
typeset mathematical formula he is reading all the information that is not explicit
in the formula but that is nonetheless necessary to the precise description of the
mathematical objects at stake.

数学のテキストをより簡潔により明瞭に記述する際の重要な手法のひとつは、表記規則の工夫であり、場合によっては記法の乱用をすることです。これらの表記規則は通常、数学の特定分野のコミュニティに属する専門家達の何十年にも及ぶ実践のなかで形成されたものです。一部の規則は著者の好みにより異なりますが、大概の部分は確立された標準へと安定化する傾向があります。したがって、訓練を受けた読者は、彼が読んでいるタイプセットされた数式から、明示的ではないすべての情報を読み取ることができるでしょう。が、当該の数学的対象に関する(暗黙の情報も含む)正確な記述はもちろん必要です。

依存型理論とファイバー付き圏

型カインドの定義は次にある。

これだと、単に「型の集合」だが、排他的型カインドという概念を入れないとまずいな。

排他的型カインドと型ファミリー(型でインデックスされた型の族)をしっかり区別して、シグマ型とパイ型の特性をきちんと定義する。

依存型理論とファイバー付き圏論の類似性から色々と分かる。

グロタンディーク/フビニの定理

グロタンディーク/フビニの定理は、ファイブレーションに関する公式ではなくて、平坦化圏に関する同型性を言っているだけ。射影は関係しない。

一般的な形は: 
\newcommand{\cat}[1]{\mathcal{#1} }%
\newcommand{\hyp}{\mbox{-} }%


{\displaystyle
\int_{a\in \cat{A}}\left(\lambda\,a\in \cat{A}.  \int_{x\in F(a)} G(a, x)  \right)
\cong
\int_{(a, x)\in \int_{\cat{A}} F} G(a, x)
}

簡略に書けば:


{\displaystyle
\int_{\cat{A}}\left(\lambda\,a\in \cat{A}.  \int_{F(a)} G(a, \hyp)  \right)
\cong
\int_{\int_{\cat{A}} F} G
}

加群層の例では:

 
{\displaystyle
\int_{a\in {\bf Man} } \left( \lambda\,a\in {\bf Man}.  \int_{x\in {\bf RngSh}(a)} {\bf ModSh}(a, x)  \right) 
} \\
\cong
{\displaystyle
\int_{(a, x)\in \int_{\bf Man} {\bf RngSh}} {\bf ModSh}(a, x)
}

より普通の記法にして、特に対象に注目すると:

 
{\displaystyle
\int_{M\in {\bf Man} } \left( \lambda\, M\in {\bf Man}.  \int_{R\in {\bf RngSh}[M]} {\bf ModSh}[M, R]  \right) 
} \\
\cong
{\displaystyle
\int_{(M, R)\in {\bf RngSheaf}} {\bf ModSh}[M, R]
}

次の書き方の変換をした。


\quad R\hyp{\bf ModSh} \\
= R\hyp{\bf ModSh}[M] \\
= {\bf ModSh}[M, R]

セクション関手とグロタンディーク構成

次を混同しない。

  1. 層・前層の順像と逆像、随伴ペア
  2. 加群の係数拡大と係数制限、随伴ペア
  3. バンドルの引き戻し ペアになってない

インデックス付き圏とファイバー付き圏の同値によって次のような図式ができる。

\require{AMScd}\newcommand{\hyp}{\mbox{-}}
\begin{CD}
\int_{m\in {\bf Man}} {\bf VectBdl}[m]  @>{\int_{m\in {\bf Man}}\Gamma_{[m]} }>> \int_{r\in {\bf Rng}} (r)\hyp{\bf Mod} \\
@V{\cong}VV                                           @VV{\cong}V \\
{\bf VectBundle}        @>{\Gamma}>>                      {\bf Module}^{CRes} \\
@VVV                                           @VVV \\
{\bf Man}  @>{C^\infty}>> {\bf Rng}
\end{CD}

出てくる記号:

  1. C^\infty : {\bf Man}^{op} \to {\bf Rng} 関数環
  2. \Gamma_{[M]} : {\bf VectBdl}[M] \to C^\infty(M)\hyp{\bf Mod} 特定多様体上のセクション関手
  3. \Gamma : {\bf VectBundle} \to {\bf Module}^{CRes} 一般的な(ビッグな)セクション関手
  4. {\bf VectBdl}[\hyp]: {\bf Man}^{op} \to {\bf CAT} インデックス付き圏、バンドルの引き戻しによる
  5. (\hyp)\hyp{\bf Mod}^{CRes}: {\bf Rng}^{op} \to {\bf CAT} インデックス付き圏、係数制限(CRes = coefficient/scalar restriction)による
  6. C^\infty(\hyp)\hyp{\bf Mod}^{CRes} : {\bf Man}^{op} \to {\bf CAT} インデックス付き圏

心理的空間の上の層への操作

  • 順像=前送り は簡単
  • 逆像=引き戻し は難しい、極限を使ってさらに層化が必要。
  • 逆像には、極限を使った右逆像と、余極限を使った左逆像がある。
  • 右逆像は外からの近似、左逆像は内からの近似。
  • 右逆像は順像の右随伴、左逆像は順像の左随伴。

心理的反対圏

ロカールとフレームの関係で、Locale = Frameop がある。順序的代数構造であるフレームがあれば、ロカールは要らないともいえる。が、ロカールが空間で、フレームはその空間に与えられた構造と考えると、心理的には把握しやすい。

心理的な実在とも言える空間の圏を、心理的反対圏とでも呼ぼう。

シャピラの教科書では、前サイト〈presite〉は心理的反対圏を使って定義される。仮想的・心理的な前サイトの圏があり、それは小圏の圏の反対圏になっている。前サイトXに対して、対応する圏 CX があり、前サイトの射 X → Y には圏のあいだの射 ft = Cf : CYCX がある。

心理的には、前サイトの圏と(小さい)圏の圏は、反変的に1:1対応する。

ホモロジー代数とホモトピー

ド・ラーム復体とホモトピー - 檜山正幸のキマイラ飼育記 (はてなBlog) に書いた+α

  1. ホモトピー圏: 局所化した圏
  2. ホモトピカル圏: 局所化可能な圏の一種、弱同値を持つ圏とほぼ同じ
  3. ホモトピック圏: 鎖複体の圏の鎖ホモトピック合同関係で割った合同付き圏の商圏=ホモトピー商圏

localization in nLab から:

it is variously written C[W−1], W−1C or LWC. In some contexts, it also could be called the homotopy category of C with respect to W.

ホモロジー代数では、ホモトピック圏=鎖ホモトピック合同の商圏/ホモトピー圏=疑同型による局所化圏/ホモトピカル圏=疑同型を持つ鎖複体圏 が全部出てくる。

加群に関する定義

重要な概念\newcommand{\For}{\mbox{For }}%
\newcommand{\hyp}{\mbox{-}}%
\newcommand{\In}{\mbox{ in }}%
\newcommand{\Iff}{\Leftrightarrow}%
\newcommand{\WeDefine}{\mbox{WeDefine } }%
\newcommand{\CAT}{{\bf CAT}}%
\newcommand{\st}{\mbox{ s.t. }}%
\newcommand{\Ch}{\mathscr{C}}%
\newcommand{\cat}[1]{\mathcal{#1}}%
\newcommand{\Imp}{\Rightarrow }%

  1. 階付き加群、G-階付き加群
  2. 階付き微分加群=鎖複体、(G, r)-階付き加群微分加群

加群の平坦性:


\For M \In R\hyp {\bf Mod}\\
\WeDefine IsFlat(M) \\
  : \Iff ( (M\otimes \hyp): R\hyp {\bf Mod} \to R\hyp {\bf Mod} \In \CAT) \: isExact

加群の射影性:


\For P \In R\hyp {\bf Mod}\\
\WeDefine IsProjective(P) \\
 : \Iff \\
\forall g:M \to N \In R\hyp {\bf Mod} \st isEpi .\\
 ([id_P, g]: [P, M] \to [P, N] \In  R\hyp {\bf Mod}) \: isEpi \\
 \Iff \\
([P, \hyp]:R\hyp {\bf Mod} \to R\hyp {\bf Mod}) \: isEpiToEpi

加群の分解:


\For M \In R\hyp {\bf Mod}\\
\For X \In \Ch_\bullet(R\hyp {\bf Mod}) \\
\For \varepsilon : X \to !M \In \Ch_\bullet(R\hyp {\bf Mod}) \\
\WeDefine IsResolutionOf(X, M)\\
 : \Iff \\
 (X \overset{\varepsilon_0 }{\to} M \to 0) \: isExactSeq

加群の入射性:


\For I \In R\hyp {\bf Mod}\\
\WeDefine IsInjective(I) \\
 : \Iff \\
\forall e:L \to M \In R\hyp {\bf Mod} \st isMono .\\
 ([e, id_I]: [M, I] \to [L, I] \In  R\hyp {\bf Mod}) \: isEpi
\Iff \\
([\hyp, I]:R\hyp {\bf Mod} \to R\hyp {\bf Mod}) \: isMonoToEpi

加群の分解(余分解):


\For M \In R\hyp {\bf Mod}\\
\For Y \In \Ch^\bullet(R\hyp {\bf Mod}) \\
\For \eta : !M \to Y \In \Ch^\bullet(R\hyp {\bf Mod}) \\
\WeDefine IsCoResolutionOf(Y, M)\\
 : \Iff \\
 (0 \to M \overset{\eta^0 }{\to} Y ) \: isExactSeq

F-非輪状対象:


\For \cat{A},\cat{B} \In {\bf AbelianCAT}\\
\For F:\cat{A} \to \cat{B}\In \CAT \: isLeftExactAdditive \\
\For A\In \cat{A} \\
\WeDefine IsAcyclic(A, F)\\
 : \Iff \forall p\in {\bf Z}.(p \gt 0 \Imp R^pF(A) = 0)

環が単項イデアル整域:


\For R \In {\bf Rng}\\
\WeDefine IsPID(R)\\
 : \Iff
 \forall I\in Ideal(R). \exists a\in R.( I = (a)_R )

長いホモロジー完全列の構成:


\mbox{For } z''\in H_q(X'') \\
\mbox{Let } [x'']  := z'' \mbox{ s.t. } x'' \in Z_q(X'')\\
\mbox{Let } z'\in Z_{q -1}(X') := \\
\varepsilon\, x'\in Z_{q-1}(X'). (\\
\xymatrix{
{} & x \ar@{|->}[r]^{g_q} \ar@{|->}[d]^{d_q}& x'' \\
x' \ar@{|->}[r]^{f_{q-1}} & y' = y
}\\
)\\
\mbox{Return }[z']

ジャスティフィケーションが別に必要。

マリオス幾何 メモ 3

関係する過去記事。

あと

参考文献は:

メモ:

  1. \mathcal{A} は環付き空間の構造層である環層
  2. 位相空間X上の層または前層の圏を明示してないが、Sh[X] または PSh[X] とする。どちらかを(あるいはどちらも)短く Set[X] とも書く。これはトポス。\mathcal{A} は、Set[X] の環対象。
  3. 群層は層の圏Set[X]内の群対象。
  4. 局所自明群層は、X上で局所的にG自明バンドルのセクション群層と同型。
  5. 群層\mathcal{G}上の主層は、局所的に、群層の作用が、群乗法 \mathcal{G}\times\mathcal{G} \to \mathcal{G} と同型な、群層が作用する集合層。
  6. リー型群層は、群層\mathcal{G}に付加的構造〈extra structure〉が付いたもので、環層\mathcal{A}を係数とするリー代数\mathcal{L}があって、リー代数層としての自己同型内部ホム層aut\_\mathcal{A}\mbox{-}{\bf LieAlg}[X](\mathcal{L}) を群層の圏Grp[X]で考えて、\mathcal{G} からの表現 \rho:\mathcal{G} \to aut\_\mathcal{A}\mbox{-}{\bf LieAlg}[X](\mathcal{L}) \mbox{ in }{\bf Grp}[X] が付いたもの。リー型群層は、(\mathcal{G}, \mathcal{L}, \rho) と書ける。
  7. 主層の台層(集合層)\mathcal{P} \in {\bf Set}[X]局所自明層とは、局所的に、Sファイバーの自明バンドルのセクション層と同型なこと。
  8. 局所的自明群層上の局所自明主層は、局所セクションの0-コチェーンが意味を持つ。局所セクションの0-コチェーンを結ぶ、\mathcal{G}係数の1-コチェーンが定義できる。
  9. リー型群層に対して、モーレー・カルタン微分が定義できる。モーレー・カルタン微分は、群の乗法に対する微分公式(対数微分公式)を満たす。
  10. モーレー・カルタン微分を備えたリー型群層を、リー/モーレー/カルタン群層と呼ぶ。
  11. リー/モーレー/カルタン群層があると、その上の主層に主共変微分を定義できる。
  12. 主共変微分は、主層の切断空間に入る微分演算で、右作用に対する微分公式を満たす。
  13. リー/モーレー/カルタン群層上の主層と主共変微分の組をカルタン接続と呼ぶ。

以上でカルタン接続が定義できた。カルタン接続の圏とコジュール接続の圏の相互関係が、接続の理論の大きな話題。