<The previous article in this series | The table of contents of this series |
description/proof of that for sequence of points on metric space, sequence is Cauchy iff for each \(\epsilon\), there is \(N\) s.t. distance between \((N + 1)\)-th point and each subsequent point is smaller than \(\epsilon\)
Topics
About:
metric space
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that for any sequence of points on any metric space, the sequence is Cauchy if and only if for each \(\epsilon\), there is an \(N\) such that the distance between the \((N + 1)\)-th point and each subsequent point is smaller than \(\epsilon\).
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(T\): \(\in \{\text{ the metric spaces }\}\)
\(s\): \(: \mathbb{N} \setminus \{0\} \to T\)
//
Statements:
\(s \in \{\text{ the Cauchy sequences }\}\)
\(\iff\)
\(\forall \epsilon \in \mathbb{R} \text{ such that } 0 \lt \epsilon (\exists N \in \mathbb{N} \setminus \{0\} (\forall j \in \mathbb{N} \setminus \{0\} \text{ such that } N \lt j (dist (s (N + 1), s (j)) \lt \epsilon)))\)
//
2: Proof
Whole Strategy: Step 1: suppose that there is such an \(N\); Step 2: see that \(s\) satisfies the Cauchy condition; Step 3: suppose that \(s\) satisfies the Cauchy condition; Step 4: see that there is such an \(N\).
Step 1:
Let us suppose that there is such an \(N\).
Step 2:
Let \(\epsilon\) be any.
For \(\epsilon / 2\), there is an \(N\) such that for each \(j\) such that \(N \lt j\), \(dist (s (N + 1), s (j)) \lt \epsilon / 2\).
For each \(l, m\) such that \(N \lt l, m\), \(dist (s (l), s (m)) \le dist (s (l), s (N + 1)) + dist (s (N + 1), s (m)) \lt \epsilon / 2 + \epsilon / 2 = \epsilon\), which means that \(s\) satisfies the Cauchy condition.
Step 3:
Let us suppose that \(s\) satisfies the Cauchy condition.
Let \(\epsilon\) be any.
There is an \(N\) such that for each \(l, m\) such that \(N \lt l, m\), \(dist (s (l), s (m)) \lt \epsilon\).
Taking \(l = N + 1\), \(dist (s (N + 1), s (m)) \lt \epsilon\), for each \(m\) such that \(N \lt m\).
References
<The previous article in this series | The table of contents of this series |
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for Lie group, differential of inversion at identity is inversion of argument
Topics
About:
group
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that for any Lie group, the differential of the inversion at the identity is the inversion of the argument.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(G\): \(\in \{\text{ the Lie groups }\}\)
\(i\): \(: G \to G\), \(= \text{ the inversion }\)
//
Statements:
\(d i_1: T_1M \to T_1M, v \mapsto - v\)
//
2: Proof
Whole Strategy: Step 1: let \(m\) be the multiplication map and let \(\phi: T_{(1, 1)}(G \times G) \to T_1G \times T_1G\) be the 'vectors spaces - linear morphisms' isomorphism, and think of \(m \circ (id, i): G \to G \times G \to G, g \mapsto m (id (g), i (g))\) and see that \(d (m \circ (id, i))_1 = d m_{(1, 1)} \circ \phi^{-1} \circ \phi \circ d (id, i)_1 = 0\); Step 2: see that \(\phi \circ d (id, i)_1 (v) = (v, d i_1 (v))\); Step 3: apply the proposition that for any Lie group and the 'vectors spaces - linear morphisms' isomorphism from the double-product \(C^\infty\) manifold tangent space at the identity onto the direct sum of the constituent tangent spaces at the identities, the composition of the differential of the multiplication at the identity after the inverse of the isomorphism is the addition of the arguments.
Step 1:
Let \(m: G \times G \to G\) be the multiplication map.
There is the 'vectors spaces - linear morphisms' isomorphism, \(\phi: T_{(1, 1)}(G \times G) \to T_1G \oplus T_1G, v \mapsto (d \pi_{1, (1, 1)} (v), d \pi_{2, (1, 1)} (v))\) where \(\pi_j: G \times G \to G\) is the projection into the \(j\)-th component, by the proposition that for any finite-product \(C^\infty\) manifold with boundary, at each point of the manifold with boundary, there is a 'vectors spaces - linear morphisms' isomorphism from the tangent vectors space at the point onto the direct sum of the tangent vectors spaces of the constituents at the corresponding points.
Let us think of \(m \circ (id, i): G \to G \times G \to G, g \mapsto m (id (g), i (g))\) where \(id\) is the identity map.
\(m \circ (id, i)\) is \(C^\infty\) as a composition of \(C^\infty\) maps, by the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
\(d (m \circ (id, i))_1 = d m_{(1, 1)} \circ d (id, i)_1 = d m_{(1, 1)} \circ \phi^{-1} \circ \phi \circ d (id, i)_1 = 0\), because \(m \circ (id, i)\) is constant to \(1\).
Step 2:
For any \(v \in T_1G\), \(v\) can be realized by a \(C^\infty\) curve, \(\gamma: I \to G, t \mapsto \gamma (t)\).
\(\phi \circ d (id, i)_1 (v) = (d \pi_{1, (1, 1)} (d (id, i)_1 (v)), d \pi_{2, (1, 1)} (d (id, i)_1 (v))) = (d (\pi_1 ((id (\gamma (t)), i (\gamma (t))))) / d t \vert_0, d (\pi_2 ((id (\gamma (t)), i (\gamma (t))))) / d t \vert_0) = (d (id (\gamma (t))) / d t \vert_0, d (i (\gamma (t))) / d t \vert_0) = (d \gamma (t) / d t \vert_0, d (i (\gamma (t))) / d t \vert_0) = (v, d i_1 (v))\).
Step 3:
But \(d m_{(1, 1)} \circ \phi^{-1} ((v, d i_1 (v))) = v + d i_1 (v)\), by the proposition that for any Lie group and the 'vectors spaces - linear morphisms' isomorphism from the double-product \(C^\infty\) manifold tangent space at the identity onto the direct sum of the constituent tangent spaces at the identities, the composition of the differential of the multiplication at the identity after the inverse of the isomorphism is the addition of the arguments.
So, \(v + d i_1 (v) = 0\), so, \(d i_1 (v) = - v\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for Lie group and 'vectors spaces - linear morphisms' isomorphism from double-product \(C^\infty\) manifold tangent space onto direct sum of constituent tangent spaces, composition of differential of multiplication at identity after inverse of isomorphism is addition of arguments
Topics
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that for any Lie group and the 'vectors spaces - linear morphisms' isomorphism from the double-product \(C^\infty\) manifold tangent space at the identity onto the direct sum of the constituent tangent spaces at the identities, the composition of the differential of the multiplication at the identity after the inverse of the isomorphism is the addition of the arguments.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(G\): \(\in \{\text{ the Lie groups }\}\)
\(\phi\): \(: T_{(1, 1)}(G \times G) \to T_1G \oplus T_1G\), \(= \text{ the 'vectors spaces - linear morphisms' isomorphism }\)
\(m\): \(: G \times G \to G\), \(= \text{ the multiplication map }\)
\(d m_{(1, 1)}\): \(: T_{(1, 1)}(G \times G) \to T_1G\), \(= \text{ the differential }\)
//
Statements:
\(d m_{(1, 1)} \circ \phi^{-1}: T_1G \oplus T_1G \to T_1G, (v_1, v_2) \mapsto v_1 + v_2\)
//
2: Proof
Whole Strategy: Step 1: see that \(\phi (v) = (d \pi_{1, (1, 1)} (v), d \pi_{2, (1, 1)} (v))\) and \(d m_{(1, 1)} \circ \phi^{-1}\) is linear; Step 2: see that \(d m_{(1, 1)} \circ \phi^{-1} ((v^1, 0)) = v^1\) and \(d m_{(1, 1)} \circ \phi^{-1} ((0, v^2)) = v^2\); Step 3: conclude the proposition.
Step 1:
For each \(v \in T_{(1, 1)}(G \times G)\), \(\phi (v) = (d \pi_{1, (1, 1)} (v), d \pi_{2, (1, 1)} (v))\) where \(\pi_j: G \times G \to G\) is the projection into the \(j\)-th component, by the proposition that for any finite-product \(C^\infty\) manifold with boundary, at each point of the manifold with boundary, there is a 'vectors spaces - linear morphisms' isomorphism from the tangent vectors space at the point onto the direct sum of the tangent vectors spaces of the constituents at the corresponding points.
As \(\phi\) is a 'vectors spaces - linear morphisms' isomorphism, \(d m_{(1, 1)} \circ \phi^{-1}\) is linear.
Step 2:
Let us think of any \((v^1, 0) \in T_1G \oplus T_1G\).
\(v := \phi^{-1} ((v^1, 0))\) can be realized by a \(C^\infty\) curve, \(\gamma: I \to G \times G, t \mapsto (\gamma^1 (t), 1)\), where \(v^1 = d \gamma^1 (t) / d t \vert_0\).
\(d m_{(1, 1)} (v) = d (m \circ \gamma (t)) / d t \vert_0 = d (\gamma^1 (t) 1) / d t \vert_0 = d \gamma_1 (t) / d t \vert_0 = v^1\).
That means that \(d m_{(1, 1)} \circ \phi^{-1} ((v^1, 0)) = v^1\).
Let us think of any \((0, v^2) \in T_1G \oplus T_1G\).
\(v := \phi^{-1} ((0, v_2))\) can be realized by a \(C^\infty\) curve, \(\gamma: I \to G \times G, t \mapsto (1, \gamma^2 (t))\), where \(v^2 = d \gamma^2 (t) / d t \vert_0\).
\(d m_{(1, 1)} (v) = d (m \circ \gamma (t)) / d t \vert_0 = d (1 \gamma^2 (t)) / d t \vert_0 = d \gamma^2 (t) / d t \vert_0 = v^2\).
That means that \(d m_{(1, 1)} \circ \phi^{-1} ((0, v_2)) = v_2\).
Step 3:
As \(d m_{(1, 1)} \circ \phi^{-1}\) is linear, \(d m_{(1, 1)} \circ \phi^{-1} ((v_1, v_2)) = d m_{(1, 1)} \circ \phi^{-1} ((v_1, 0) + (0, v_2)) = d m_{(1, 1)} \circ \phi^{-1} ((v_1, 0)) + d m_{(1, 1)} \circ \phi^{-1} ((0, v_2)) = v_1 + v_2\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of Lie subgroup
Topics
About:
group
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of Lie subgroup.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( G'\): \(\in \{\text{ the Lie groups }\}\)
\(*G\): \(\in \{\text{ the subgroups of } G'\}\) with a topology and an atlas, \(\in \{\text{ the Lie groups }\}\)
//
Conditions:
\(G \in \{\text{ the immersed submanifolds of } G'\}\)
//
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of Lie group
Topics
About:
group
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of Lie group.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(*G\): \(\in \{\text{ the groups }\} \cap \{\text{ the } C^\infty \text{ manifolds } \}\)
//
Conditions:
\(m: G \times G \to G, (g_1, g_2) \mapsto g_1 g_2 \in \{\text{ the } C^\infty \text{ maps }\}\), called "multiplication map"
\(i: G \to G, g \mapsto g^{-1} \in \{\text{ the } C^\infty \text{ maps }\}\), called "inversion map"
//
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of finite-product Hilbert space
Topics
About:
metric space
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of finite-product Hilbert space.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( F\): \(\in \{\mathbb{R}, \mathbb{C}\}\), with the canonical field structure
\( \{V_1, ..., V_n\}\): \(\subseteq \{\text{ the } F \text{ Hilbert spaces }\}\), with any inner products, \(\{\langle \bullet, \bullet \rangle_1, ..., \langle \bullet, \bullet \rangle_n\}\)
\(*V_1 \times ... \times V_n\): \(= \text{ the product vectors space with the product inner product }\) with the metric induced by the norm induced by the inner product, \(\in \{\text{ the } F \text{ Hilbert spaces }\}\)
//
Conditions:
//
2: Note
Let us see that \(V_1 \times ... \times V_n\) is indeed a complete metric space, so, indeed a Hilbert space.
Let \(s: \mathbb{N} \to V_1 \times ... \times V_n\) be any Cauchy sequence.
For each \(\epsilon \in \mathbb{R}\) such that \(0 \lt \epsilon\), there is an \(N \in \mathbb{N}\) such that for each \(m, o \in \mathbb{N}\) such that \(N \lt m, o\), \(\langle s (o) - s (m), s (o) - s (m) \rangle \lt \epsilon^2\).
\(\langle s (o) - s (m), s (o) - s (m) \rangle = \langle (s (o)^1, ..., s (o)^n) - (s (m)^1, ..., s (m)^n), (s (o)^1, ..., s (o)^n) - (s (m)^1, ..., s (m)^n) \rangle = \langle (s (o)^1 - s (m)^1, ..., s (o)^n - s (m)^n), (s (o)^1 - s (m)^1, ..., s (o)^n - s (m)^n) \rangle = \langle s (o)^1 - s (m)^1, s (o)^1 - s (m)^1 \rangle_1 + ... + \langle s (o)^n - s (m)^n, s (o)^n - s (m)^n \rangle_n \lt \epsilon^2\), which means that for each \(j \in \{1, ..., n\}\), \(\langle s (o)^j - s (m)^j, s (o)^j - s (m)^j \rangle_j \lt \epsilon^2\).
That means that \(s^j: \mathbb{N} \to V_j\) is a Cauchy sequence.
As \(V_j\) is complete, \(s^j\) converges to a \(v^j \in V_j\).
Let \(v := (v^1, ..., v^n) \in V_1 \times ... \times V_n\).
\(s\) converges to \(v\), because for each \(\epsilon\), we can take an \(N\) such that for each \(m\) such that \(N \lt m\) and each \(j\), \(\langle v^j - s (m)^j \rangle \lt \epsilon^2 / n\), and then, \(\langle v - s (m), v - s (m) \rangle = \langle (v^1, ..., v^n) - (s (m)^1, ..., s (m)^n), (v^1, ..., v^n) - (s (m)^1, ..., s (m)^n) \rangle = \langle v^1 - s (m)^1, v^1 - s (m)^1 \rangle_1 + ... \langle v^n - s (m)^n, v^n - s (m)^n \rangle_n \lt \epsilon^2 / n + ... + \epsilon^2 / n = \epsilon^2\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for finite-product vectors space with finite-product inner product, topology induced by product inner product is product topology of topologies induced by inner products
The table of contents of this article
Main Body
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of finite-product inner product
Topics
About:
vectors space
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of finite-product inner product.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( F\): \(\in \{ \mathbb{R}, \mathbb{C} \}\), with the canonical field structure
\( \{V_1, ..., V_n\}\): \(\subseteq \{\text{ the } F \text{ vectors spaces }\}\), with any inner products, \(\{\langle \bullet, \bullet \rangle_1, ..., \langle \bullet, \bullet \rangle_n\}\)
\( V_1 \times ... \times V_n\): \(= \text{ the product vectors space }\)
\(*\langle \bullet, \bullet \rangle\): \(: (V_1 \times ... \times V_n) \times (V_1 \times ... \times V_n) \to F\), \(\in \{\text{ the inner products for } V_1 \times ... \times V_n\}\)
//
Conditions:
\(\forall (v_1, ..., v_n), (v'_1, ..., v'_n) \in V_1 \times ... \times V_n (\langle (v_1, ..., v_n), (v'_1, ..., v'_n) \rangle = \langle v_1, v'_1 \rangle_1 + ... + \langle v_n, v'_n \rangle_n)\)
//
2: Note
Let us see that \(\langle \bullet, \bullet \rangle\) is indeed an inner product.
Let \(v_1 = (v_{1, 1}, ..., v_{1, n}), v_2 = (v_{2, 1}, ..., v_{2, n}), v_3 = (v_{3, 1}, ..., v_{3, n}) \in V_1 \times ... \times V_n\) be any; let \(r_1, r_2 \in F\) be any.
1) \((0 \le \langle v_1, v_1 \rangle)\) \(\land\) \((0 = \langle v_1, v_1 \rangle \iff v_1 = 0)\): \(0 \le \langle v_{1, 1}, v_{1, 1} \rangle_1 + ... + \langle v_{1, n}, v_{1, n} \rangle_n = \langle (v_{1, 1}, ..., v_{1, n}), (v_{1, 1}, ..., v_{1, n}) \rangle = \langle v_1, v_1 \rangle\); when \(0 = \langle v_1, v_1 \rangle\), each \(\langle v_{1, j}, v_{1, j} \rangle_j = 0\), so, each \(v_{1, j} = 0\), so, \(v_1 = (v_{1, 1}, ..., v_{1, n}) = 0\); when \(v_1 = (v_{1, 1}, ..., v_{1, n}) = 0\), each \(v_{1, j} = 0\), so, each \(\langle v_{1, j}, v_{1, j} \rangle_j = 0\), so, \(0 = \langle v_1, v_1 \rangle\).
2) \(\langle v_1, v_2 \rangle = \overline{\langle v_2, v_1 \rangle}\), where the over-line denotes the complex conjugate: \(\langle v_1, v_2 \rangle = \langle v_{1, 1}, v_{2, 1} \rangle_1 + ... + \langle v_{1, n}, v_{2, n} \rangle_n = \overline{\langle v_{2, 1}, v_{1, 1} \rangle_1} + ... + \overline{\langle v_{2, n}, v_{1, n} \rangle_n} = \overline{\langle v_{2, 1}, v_{1, 1} \rangle_1 + ... + \langle v_{2, n}, v_{1, n} \rangle_n} = \overline{\langle v_2, v_1 \rangle}\).
3) \(\langle r_1 v_1 + r_2 v_2, v_3 \rangle = r_1 \langle v_1, v_3 \rangle + r_2 \langle v_2, v_3 \rangle\): \(\langle r_1 v_1 + r_2 v_2, v_3 \rangle = \langle r_1 (v_{1, 1}, ..., v_{1, n}) + r_2 (v_{2, 1}, ..., v_{2, n}), (v_{3, 1}, ..., v_{3, n}) \rangle = \langle (r_1 v_{1, 1} + r_2 v_{2, 1}, ..., r_1 v_{1, n} + r_2 v_{2, n}), (v_{3, 1}, ..., v_{3, n}) \rangle = \langle r_1 v_{1, 1} + r_2 v_{2, 1}, v_{3, 1} \rangle_1 + ... + \langle r_1 v_{1, n} + r_2 v_{2, n}, v_{3, n} \rangle_n = r_1 \langle v_{1, 1}, v_{3, 1} \rangle_1 + r_2 \langle v_{2, 1}, v_{3, 1} \rangle_1 + ... + r_1 \langle v_{1, n}, v_{3, n} \rangle_n + r_2 \langle v_{2, n}, v_{3, n} \rangle_n = r_1 (\langle v_{1, 1}, v_{3, 1} \rangle_1 + ... + \langle v_{1, n}, v_{3, n} \rangle_n) + r_2 (\langle v_{2, 1}, v_{3, 1} \rangle_1 + ... + \langle v_{2, n}, v_{3, n} \rangle_n) = r_1 \langle v_1, v_3 \rangle + r_2 \langle v_2, v_3 \rangle\).
The product needs to be finite, because otherwise, the inner product may not be into \(F\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of group right action that corresponds to group left action
Topics
About:
group
About:
set
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of group right action that corresponds to group left action.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( G\): \(\in \{ \text{ the groups } \}\)
\( S\): \(\in \{ \text{ the sets } \}\)
\( f\): \(: G \times S \to S\), \(\in \{\text{ the group left actions }\}\)
\(*f'\): \(: S \times G \to S, (s, g) \mapsto f (g^{-1}, s)\), \(\in \{\text{ the group right actions }\}\)
//
Conditions:
//
2: Note
Let us see that \(f'\) is indeed a group right action.
For each \(g_1, g_2 \in G\) and each \(s \in S\), \(f' (f' (s, g_1), g_2) = f' (f (g_1^{-1}, s), g_2) = f (g_2^{-1}, f (g_1^{-1}, s)) = f (g_2^{-1} g_1^{-1}, s) = f ((g_1 g_2)^{-1}, s) = f' (s, g_1 g_2)\).
For each \(s \in S\), \(f' (s, 1) = f (1^{-1}, s) = f (1, s) = s\).
Note that \(f\) itself cannot be regarded to be any group right action; we have constructed the group right action from \(f\): 'group left action' is not about just denoting \(G \times S\) instead of \(S \times G\): \(f'': S \times G \to S, (s, g) \mapsto f (g, s)\) is not any group right action, because \(f'' (f'' (s, g_1), g_2) = f'' (f (g_1, s), g_2) = f (g_2, f (g_1, s)) = f (g_2 g_1, s) = f'' (s, g_2 g_1)\), which does not equal \(f'' (s, g_1 g_2)\) in general.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of group left action that corresponds to group right action
Topics
About:
group
About:
set
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of group left action that corresponds to group right action.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( G\): \(\in \{ \text{ the groups } \}\)
\( S\): \(\in \{ \text{ the sets } \}\)
\( f\): \(: S \times G \to S\), \(\in \{\text{ the group right actions }\}\)
\(*f'\): \(: G \times S \to S, (g, s) \mapsto f (s, g^{-1})\), \(\in \{\text{ the group left actions }\}\)
//
Conditions:
//
2: Note
Let us see that \(f'\) is indeed a group left action.
For each \(g_1, g_2 \in G\) and each \(s \in S\), \(f' (g_2, f' (g_1, s)) = f' (g_2, f (s, {g_1}^{-1})) = f (f (s, {g_1}^{-1}), g_2^{-1}) = f (s, {g_1}^{-1} g_2^{-1}) = f (s, (g_2 g_1)^{-1}) = f' (g_2 g_1, s)\).
For each \(s \in S\), \(f' (1, s) = f (s, 1) = s\).
Note that \(f\) itself cannot be regarded to be any group left action; we have constructed the group left action from \(f\): 'group right action' is not about just denoting \(S \times G\) instead of \(G \times S\): \(f'': G \times S \to S, (g, s) \mapsto f (s, g)\) is not any group left action, because \(f'' (g_2, f'' (g_1, s)) = f'' (g_2, f (s, g_1)) = f (f (s, g_1), g_2) = f (s, g_1 g_2) = f'' (g_1 g_2, s)\), which does not equal \(f'' (g_2 g_1, s)\) in general.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
definition of group right action
Topics
About:
group
About:
set
The table of contents of this article
Starting Context
Target Context
-
The reader will have a definition of group right action.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( G\): \(\in \{ \text{ the groups } \}\)
\( S\): \(\in \{ \text{ the sets } \}\)
\(*f\): \(: S \times G \to S\)
//
Conditions:
\(\forall g_1, g_2 \in G, \forall s \in S (f (f (s, g_1), g_2) = f (s, g_1 g_2))\)
\(\land\)
\(\forall s \in S (f (s, 1) = s)\)
//
\(f (s, g)\) is usually denoted as \(s g\).
2: Note
The notation, \(s g\), is permissible because \(s g_1 g_2\) is not ambiguous because of the conditions for group right action.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for surjective local diffeomorphism between \(C^\infty\) manifolds with boundary and section along open subset of codomain, section is \(C^\infty\)
Topics
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that for any surjective local diffeomorphism between any \(C^\infty\) manifolds with boundary and any section along any open subset of the codomain, the section is \(C^\infty\).
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(M_1\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M_2\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(f\): \(: M_1 \to M_2\), \(\in \{\text{ the surjections }\} \land \{\text{ the local diffeomorphisms }\}\)
\(U_2\): \(\in \{\text{ the open subsets of } M_2\}\)
\(s\): \(: U_2 \to M_1\), \(\in \{\text{ the sections of } f \text{ along } U_2\}\)
//
Statements:
\(s \in \{\text{ the } C^\infty \text{ maps }\}\)
//
2: Note
So, \(s\) inevitably becomes \(C^\infty\) by virtue of \(f\) being a local diffeomorphism.
As Proof shows, this proposition is possible because \(s\) is guaranteed to be continuous by definition.
3: Proof
Whole Strategy: Step 1: take any \(u \in U_2\), an open neighborhood of \(s (u)\), \(U'_{s (u)} \subseteq M_1\), and an open neighborhood of \(u\), \(U'_u \subseteq M_2\), such that \(U'_u \subseteq U_2\) and \(f \vert_{U'_{s (u)}}: U'_{s (u)} \to U'_u\) is a diffeomorphism; Step 2: take an open neighborhood of \(u\), \(U_u \subseteq U_2\), such that \(U_u \subseteq U'_u\) and \(s (U_u) \subseteq U'_{s (u)}\); Step 3: see that \(s \vert_{U_u}: U_u \to U'_{s (u)}\) is the restriction of \({f \vert_{U'_{s (u)}}}^{-1}\).
Step 1:
Let \(u \in U_2\) be any.
\(f (s (u)) = u\).
Let us take an open neighborhood of \(s (u)\), \(U'_{s (u)} \subseteq M_1\), and an open neighborhood of \(u\), \(U'_u \subseteq M_2\), such that \(U'_u \subseteq U_2\) and \(f \vert_{U'_{s (u)}}: U'_{s (u)} \to U'_u\) is a diffeomorphism, which is possible by the proposition that for any local diffeomorphism between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, any open neighborhood of any domain point, and any open neighborhood of the point image, a diffeomorphism can be chosen to be contained in the neighborhoods.
Step 2:
Let us take an open neighborhood of \(u\), \(U_u \subseteq U_2\), such that \(U_u \subseteq U'_u\) and \(s (U_u) \subseteq U'_{s (u)}\), which is possible because \(s\) is continuous by definition: if \(U_u\) is not contained in \(U'_u\), \(U_u \cap U'_u\) can be taken to be \(U_u\) instead.
Step 3:
Let us think of \(s \vert_{U_u}: U_u \to U'_{s (u)}\).
\({f \vert_{U'_{s (u)}}}^{-1}: U'_u \to U'_{s (u)}\) is \(C^\infty\).
\(s \vert_{U_u}\) is the domain restriction of \({f \vert_{U'_{s (u)}}}^{-1}\), because for each \(u' \in U_u\), \(f \circ s \vert_{U_u} (u') = u'\), but as \(s \vert_{U_u} (u') \in U'_{s (u)}\), \(f \circ s \vert_{U_u} (u') = f \vert_{U'_{s (u)}} \circ s \vert_{U_u} (u')\), so, \({f \vert_{U'_{s (u)}}}^{-1} \circ f \vert_{U'_{s (u)}} \circ s \vert_{U_u} (u') = {f \vert_{U'_{s (u)}}}^{-1} (u')\), but the left hand side is \(s \vert_{U_u} (u')\).
So, \(s \vert_{U_u}\) is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction on any domain that contains the point is \(C^k\) at the point.
Also the codomain extension, \(s \vert_{U_u}: U_u \to M_1\), is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point.
So, \(s: U_2 \to M_1\) is \(C\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, the map is \(C^k\) at any point if the restriction on any subspace open neighborhood of the point domain is \(C^k\) at the point, where \(k\) includes \(\infty\).
References
<The previous article in this series | The table of contents of this series | The next article in this series>
<The previous article in this series | The table of contents of this series | The next article in this series>
description/proof of that for local diffeomorphism between arbitrary subsets of \(C^\infty\) manifolds with boundary, open neighborhood of domain point, and open neighborhood of point image, diffeomorphism can be chosen to be contained in neighborhoods
Topics
About:
\(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
-
The reader will have a description and a proof of the proposition that for any local diffeomorphism between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, any open neighborhood of any domain point, and any open neighborhood of the point image, a diffeomorphism can be chosen to be contained in the neighborhoods.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(M_1\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M_2\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(S_1\): \(\subseteq M_1\)
\(S_2\): \(\subseteq M_2\)
\(f\): \(: S_1 \to S_2\), \(\in \{\text{ the local diffeomorphisms }\}\)
\(s\): \(\in S_1\)
\(U'_s\): \(\in \{\text{ the open neighborhoods of } s \text{ on } S_1\}\)
\(U'_{f (s)}\): \(\in \{\text{ the open neighborhoods of } f (s) \text{ on } S_2\}\)
//
Statements:
\(\exists U_s \in \{\text{ the open neighborhoods of } s \text{ on } S_1\}, \exists U_{f (s)} \in \{\text{ the open neighborhoods of } f (s) \text{ on } S_2\} (U_s \subseteq U'_s \land U_{f (s)} \subseteq U'_{f (s)} \land f \vert_{U_s}: U_s \to U_{f (s)} \in \{\text{ the diffeomorphisms }\})\)
//
2: Note
This proposition tends to be accepted as obvious, but we will prove it for sure, for once.
Typically, \(S_1 = M_1\) and \(S_2 = M_2\), but we do not exclude the other cases.
3: Proof
Whole Strategy: Step 1: take an open neighborhood of \(s\), \(U''_s \subseteq M_1\), and an open neighborhood of \(f (s)\), \(U''_{f (s)} \subseteq M_2\), such that \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism; Step 2: take an open neighborhood of \(s\), \(U'''_s \subseteq S_1\), such that \(f (U'''_s) \subseteq U'_{f (s)}\); Step 3: take \(U_s := U'_s \cap U''_s \cap U'''_s\) and \(U_{f (s)} := f (U_s)\), and see that \(U_s \subseteq S_1\) is an open neighborhood of \(s\), \(U_{f (s)} \subseteq S_2\) is an open neighborhood of \(f (s)\), and \(U_s \subseteq U'_s\), \(U_{f (s)} \subseteq U'_{f (s)}\), and \(f \vert_{U_s}: U_s \to U_{f (s)}\) is a diffeomorphism.
Step 1:
Let us take an open neighborhood of \(s\), \(U''_s \subseteq M_1\), and an open neighborhood of \(f (s)\), \(U''_{f (s)} \subseteq M_2\), such that \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism, which is possible because \(f\) is a local diffeomorphism.
Step 2:
Let us take an open neighborhood of \(s\), \(U'''_s \subseteq S_1\), such that \(f (U'''_s) \subseteq U'_{f (s)}\), which is possible because \(f\) is continuous, by the proposition that any map between arbitrary subsets of any \(C^\infty\) manifolds with boundary locally diffeomorphic at any point is \(C^\infty\) at the point: being \(C^\infty\) implies being continuous as is mentions in Note for the definition of map between arbitrary subsets of \(C^\infty\) manifolds with boundary \(C^k\) at point, where \(k\) excludes \(0\) and includes \(\infty\).
Step 3:
Let us take \(U_s := U'_s \cap U''_s \cap U'''_s\) and \(U_{f (s)} := f (U_s)\).
\(U_s \subseteq S_1\) is an open neighborhood of \(s\), because \(s \in U_s\), and \(U_s\) is an open subset of \(S_1\), because \(U_s = U'_s \cap U''_s \cap U'''_s \cap S_1 = U'_s \cap (U''_s \cap S_1) \cap U'''_s\), but \(U''_s \cap S_1\) is open on \(S_1\) by the definition of subspace topology and \(U'_s\) and \(U'''_s\) are open on \(S_1\).
\(U_{f (s)} \subseteq S_2\) is an open neighborhood of \(f (s)\), because \(f (s) \in U_{f (s)}\), because as \(s \in U_s\), \(f (s) \in f (U_s) = U_{f (s)}\), \(U_{f (s)}\) is a subset of \(S_2\), because as \(U_s \subseteq U'''_s\), \(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)} \subseteq S_2\), and it is open on \(S_2\), because \(U_s := U'_s \cap U''_s \cap U'''_s\) is open on \(U''_s \cap S_1\) because \(= U''_s \cap S_1 \cap (U'_s \cap U'''_s) = (U''_s \cap S_1) \cap U''''_s \cap S_1\) where \(U''''_s \subseteq M_1\) is an open neighborhood of \(s\) on \(M_1\), \(= (U''_s \cap S_1) \cap U''''_s\), so, \(f (U_s)\) is open on \(U''_{f (s)} \cap S_2\) because \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism, but as \(U''_{f (s)} \cap S_2\) is open on \(S_2\), \(f (U_s)\) is open on \(S_2\), by the proposition that for any topological space and any topological subspace that is open on the base space, any subset of the subspace is open on the subspace if and only if it is open on the base space.
\(U_s \subseteq U'_s\).
\(U_{f (s)} \subseteq U'_{f (s)}\), because \(U_s \subseteq U'''_s\), and \(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)}\).
\(f \vert_{U_s}: U_s \to U_{f (s)}\) is a diffeomorphism, because it is a bijection as the restriction of the bijective \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\), and it is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction on any domain that contains the point is \(C^k\) at the point and the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point, and its inverse is \(C^\infty\), likewise.
References
<The previous article in this series | The table of contents of this series | The next article in this series>
