Cancelling local diffeomorphisms from compositions #
A continuous map into a manifold is C^n if its composite with a C^n local diffeomorphism is
C^n. This file provides pointwise-within, on-set, and global versions of this cancellation
principle.
Dually, a map out of a manifold is C^m at the image of a point at which p is a C^n local
diffeomorphism, for m ≤ n, exactly when its precomposite with p is C^m at that point. For a
surjective local diffeomorphism, such as the orbit projection of a free properly discontinuous
action, this characterises the C^m maps out of its target. The same holds for maps out of a
product A × B whose second factor is the target of p, precomposed with Prod.map id p; this
characterises the C^m maps A × B → N, such as flows on a quotient manifold.
Precomposing a C^n local diffeomorphism out of a normed space E with a continuous linear
automorphism of E gives again a C^n local diffeomorphism
(IsLocalDiffeomorph.comp_continuousLinearEquiv); for open embeddings this is Mathlib's
Homeomorph.isOpenEmbedding_comp_iff. For a linear isometry R, both facts are also stated for
e ∘ R itself (Topology.IsOpenEmbedding.comp_linearIsometryEquiv,
IsLocalDiffeomorph.comp_linearIsometryEquiv): the coercion of R to a continuous linear
equivalence is not reducibly equal to R, so instances built from the general statements would not
apply to e ∘ R.
Main results #
ContMDiffWithinAt.of_comp_isLocalDiffeomorph: pointwise-within cancellation.ContMDiffOn.of_comp_isLocalDiffeomorph: on-set cancellation.ContMDiff.of_comp_isLocalDiffeomorph: global cancellation.IsLocalDiffeomorphAt.contMDiffAt_comp_iff: pointwise cancellation on the source side.IsLocalDiffeomorphAt.mdifferentiableAt_comp_iff: the same for differentiability.IsLocalDiffeomorph.contMDiff_comp_iff: global cancellation on the source side, for a surjective local diffeomorphism.IsLocalDiffeomorphAt.contMDiffAt_comp_prodMap_iff,IsLocalDiffeomorph.contMDiff_comp_prodMap_iff: the same cancellation for maps out of a product, along the second factor.
A continuous map is C^n within a set at a point when its composite with a map that is a
C^n local diffeomorphism at the image point is C^n there.
A continuous map on a set is C^n there when its composite with a C^n local diffeomorphism
is C^n on that set.
A continuous map is C^n when its composite with a C^n local diffeomorphism is C^n.
If p is a C^n local diffeomorphism at x and m ≤ n, a map g is C^m at p x
exactly when g ∘ p is C^m at x.
If p is a C^n local diffeomorphism at x with n ≠ 0, a map g is differentiable at
p x exactly when g ∘ p is differentiable at x.
If p is a surjective C^n local diffeomorphism and m ≤ n, a map g out of its target is
C^m exactly when g ∘ p is C^m.
If p is a C^n local diffeomorphism at x and m ≤ n, a map g out of a product is C^m
at (a, p x) exactly when g ∘ Prod.map id p is C^m at (a, x).
If p is a surjective C^n local diffeomorphism and m ≤ n, a map g out of a product with
second factor the target of p is C^m exactly when g ∘ Prod.map id p is C^m.
A C^n local diffeomorphism out of a normed space E remains one when precomposed with a
continuous linear automorphism of E.
A map out of a normed space E which is an open embedding remains one when precomposed with
a linear isometry R of E, stated for e ∘ R itself.
The special case of IsLocalDiffeomorph.comp_continuousLinearEquiv for a linear isometry R,
stated for e ∘ R itself rather than for its continuous linear equivalence.