\(C^\infty\) 1-フォームを\(C^\infty\)カーブに沿った\(C^\infty\)ベクトルたちフィールド（場）へ作用させたものはカーブのドメイン（定義域）上方の\(C^\infty\)ファンクション（関数）であることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、の定義を知っている。
- 読者は、\(C^\infty\)カーブに沿った\(C^\infty\)ベクトルたちフィールド（場）の定義を知っている。
- 読者は、\(C^\infty\)マニフォールド（多様体）上方の\(q\)-フォームの定義を知っている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、上方の任意の\((0, q)\)-テンソルたちフィールド（場）は\(C^\infty\)である、もしも、任意の\(C^\infty\)ベクトルたちフィールド（場）たちへのオペレーション結果が\(C^\infty\)である場合、そしてその場合に限って、という命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、およびその上の任意の\(C^\infty\)カーブに対して、任意の\(C^\infty\)1-フォームを当該カーブに沿った任意の\(C^\infty\)ベクトルたちフィールド（場）へ作用させたものは当該カーブのドメイン（定義域）上方の\(C^\infty\)ファンクション（関数）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M\): \(\in \{\text{ 全ての } d \text{ -ディメンショナル（次元） } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(I\): \(= (s_1, s_2) \subseteq \mathbb{R}\)、当該ユークリディアン\(C^\infty\)マニフォールド（多様体）のオープン（開）サブマニフォールド（部分多様体）として
\(\lambda\): \(: I \to M\), \(\in \{\text{ 全ての } C^\infty \text{ カーブたち }\}\)
\(V\): \(:I \to \lambda (I) \to TM\), \(\in \{\lambda \text{ に沿った全ての } C^\infty \text{ ベクトルたちフィールド（場）たち }\}\)
\(t\): \(: M \to T^0_1 (TM)\), \(\in \{\text{ 全ての } C^\infty 1 \text{ -フォームたち }\}\)
//
ステートメント（言明）たち:
\(t (V): I \to \mathbb{R} \in \{\text{ 全ての } C^\infty \text{ マップ（写像）たち }\}\)
//
2: 証明
各\(s \in I\)に対して、あるチャート\((U_{\lambda (s)} \subseteq M, \phi_{\lambda (s)})\)およびインデュースト（誘導された）チャート\((\pi^{-1} (U_{\lambda (s)}) \subseteq TM, \widetilde{\phi_{\lambda (s)}})\)を取ろう。
\(\lambda\)はコンティニュアス（連続）であるので、\(s\)の以下を満たすあるオープンネイバーフッド（開近傍）\(U_s \subseteq I\)、つまり、\(\lambda (U_s) \subseteq U_{\lambda (s)}\)、がある。
\(U_s\)上方にて、\(V (\lambda (s)) = V^j (\lambda (s)) \partial / \partial x^j\)、ここで、\(V^j (\lambda (s))\)たちは\(C^\infty\)である、(s\)のファンクション（関数）たちとして、なぜなら、\(V\)は\(C^\infty\)である。
\(t (V (\lambda (s))) = t (V^j (\lambda (s)) \partial / \partial x^j) = V^j (\lambda (s)) t (\partial / \partial x^j)\)、しかし、\(\partial / \partial x^j\)は\(U_{\lambda (s)}\)上方の\(C^\infty\)ベクトルたちフィールド（場）であるから、\(t (\partial / \partial x^j)\)は\(U_{\lambda (s)}\)上方の\(C^\infty\)ファンクション（関数）である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、上方の任意の\((0, q)\)-テンソルたちフィールド（場）は\(C^\infty\)である、もしも、任意の\(C^\infty\)ベクトルたちフィールド（場）たちへのオペレーション結果が\(C^\infty\)である場合、そしてその場合に限って、という命題によって、そして、\(V^j (\lambda (s)) t (\partial / \partial x^j) = V^j (\lambda (s)) (t (\partial / \partial x^j)) (\lambda (s))\)、そして、\((t (\partial / \partial x^j)) (\lambda (s))\)は\(s\)の\(C^\infty\)ファンクション（関数）である、なぜなら、\(\lambda\)は\(C^\infty\)である、したがって、\(t (V (\lambda (s)))\)は\(s\)の\(C^\infty\)ファンクション（関数）である。
