A description/proof of that for diffeomorphism from
Topics
About:
The table of contents of this article
Starting Context
-
The reader knows a definition of
manifold with boundary. - The reader knows a definition of neighborhood of point.
-
The reader knows a definition of map between arbitrary subsets of
manifolds with boundary at point, where excludes and includes . -
The reader knows a definition of diffeomorphism between arbitrary subsets of
manifolds with boundary. -
The reader knows a definition of differential of
map between manifolds with boundary at point. - The reader knows a definition of %category name% isomorphism.
-
The reader admits the proposition that any
manifold with boundary is locally compact. - The reader admits the proposition that for any locally compact Hausdorff topological space, in any neighborhood around any point, there is an open neighborhood of the point whose (the open neighborhood's) closure is compact and contained in the former neighborhood.
-
The reader admits the proposition that for any map between any arbitrary subsets of any
manifolds with boundary at any point, where includes , the restriction on any domain that contains the point is at the point. -
The reader admits the proposition that for any maps between any arbitrary subsets of any
manifolds with boundary at corresponding points, where includes , the composition is at the point. -
The reader admits the proposition that for any
function from any closed subset of any manifold with boundary and any open neighborhood of the closed subset, there is a extension over the manifold with boundary that is supported in the open neighborhood. -
The reader admits the proposition that any tangent vector at any point on any
manifold with boundary is realized by a curve. - The reader admits the proposition that any bijective linear morphism is a 'vectors spaces - linear morphisms' isomorphism.
Target Context
-
The reader will have a description and a proof of the proposition that for any diffeomorphism from any
manifold with boundary onto any neighborhood of any point image on any manifold with boundary, the differential of the diffeomorphism or any its codomain extension at the point is a 'vectors spaces - linear morphisms' isomorphism.
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: Note
For any diffeomorphism between any
The domain has to be the whole
2: Description
For any
In fact, for any subset,
3: Proof
Let us prove that
Let
There is a
As
There is a
As
So, yes, there is a
Let us prove that
As any tangent vector on
When
When
When
So,
For
So,