Extending diffeomorphisms by the identity #
A diffeomorphism of an open part of a manifold extends by the identity when its moving points
are contained in a closed subset of the ambient manifold lying inside that open part.
IsLocalDiffeomorph.exists_diffeomorph_extend gives this extension along an open embedding which
is a local diffeomorphism. The source and ambient manifold may have different models.
For a compact set in the source, its image is closed in a Hausdorff ambient manifold, giving
IsLocalDiffeomorph.exists_diffeomorph_extend_of_isCompact. In particular,
Diffeomorph.exists_extend_of_isCompact extends a compactly supported diffeomorphism of any open
submanifold. These results transplant diffeomorphisms constructed in coordinates to the ambient
manifold while keeping control of where points move.
When the open part is the source of an extended chart, the extension has an explicit formula,
TauCeti.chartExtend: a map f of the model space which fixes every point outside a compact
subset K of the interior of the chart target, and maps K into itself, is read through the chart
on the chart source and extended by the identity elsewhere. The formula makes the dependence on
f visible: a family of such maps depending C^n-smoothly on a parameter gives a family of
self-maps of the manifold depending C^n-smoothly on the parameter
(TauCeti.contMDiff_chartExtend). A diffeomorphism of the model space supported in K extends to
the diffeomorphism Diffeomorph.chartExtend of the manifold.
The underlying homeomorphism is supplied by
Topology.IsOpenEmbedding.exists_homeomorph_extend. Smoothness follows locally: on the open
image, cancel the coordinate local diffeomorphism; away from the closed set, the extension is
locally the identity. This applies to the inverse as well, without any loss of regularity.
References #
- R. Palais, Extending diffeomorphisms, Proc. Amer. Math. Soc. 11 (1960), 274â277, for the use of coordinate extensions in ambient extension arguments.
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8.
A diffeomorphism of N extends along a smooth open embedding Ī : N â M by the identity
if its moving points lie over a closed set C â range Ī. The extension intertwines the original
diffeomorphism with Ī and fixes every point outside C.
A diffeomorphism fixing the complement of a compact set K extends along a smooth open
embedding into a Hausdorff manifold, fixing the complement of the compact image Ī '' K.
A diffeomorphism of an open submanifold, equal to the identity off a compact set K in
that submanifold, extends to an ambient diffeomorphism equal to the identity off K's image.
In particular, the ambient diffeomorphism fixes every point outside the open submanifold.
Extension through a chart #
The extension by the identity of a map f of the model space through the extended chart at
x: a point z of the chart source goes to (extChartAt I x).symm (f (extChartAt I x z)), and
every other point is fixed.
Instances For
On the chart source, the extension of f is f read through the chart.
Off the chart source, the extension of f is the identity.
On the chart, the extension of f reads as f.
The extension of a map fixing every point outside K fixes every point outside the preimage
of K under the chart.
The extension of the identity is the identity.
Extension through a chart is compatible with composition, for maps fixing every point outside
a subset K of the chart target and mapping K into itself.
Smooth dependence of the extension through a chart on parameters. Let ÎĻ q, for q in a
manifold P, be maps of the model space depending jointly C^n-smoothly on q and the point,
each fixing every point outside a compact subset K of the interior of the chart target and
mapping K into itself. Then their extensions through the chart at x depend jointly
C^n-smoothly on q and the point of M.
The extension of a diffeomorphism of the model space through a chart. A C^n
diffeomorphism Ī of the model space fixing every point outside a compact subset K of the
interior of the target of the extended chart at x extends to a C^n diffeomorphism of M: it
reads as Ī through the chart (Diffeomorph.chartExtend_extChartAt_symm) and fixes every point
outside the preimage of K under the chart (Diffeomorph.chartExtend_eq_self). Its inverse is
the extension of Ī.symm (Diffeomorph.chartExtend_symm).
Instances For
The extension of Ī through the chart is TauCeti.chartExtend of Ī.
The inverse of the extension of Ī through the chart is the extension of Ī.symm.
The extension of Ī through the chart reads as Ī on the chart.
The extension of Ī through the chart fixes every point outside the preimage of K.
Smooth families of extensions through a chart. The extensions through the chart at x of
a family Ī q, q â P, of diffeomorphisms of the model space depending jointly C^n-smoothly on
q and the point, each fixing every point outside K, depend jointly C^n-smoothly on q and
the point of M.