Local diffeomorphisms between manifolds #
In this file, we define C^n local diffeomorphisms between manifolds.
A C^n map f : M → N is a local diffeomorphism at x iff there are neighbourhoods s
and t of x and f x, respectively such that f restricts to a diffeomorphism
between s and t. f is called a local diffeomorphism on s iff it is a local diffeomorphism
at every x ∈ s, and a local diffeomorphism iff it is a local diffeomorphism on univ.
Main definitions #
IsLocalDiffeomorphAt I J n f x:fis aC^nlocal diffeomorphism atxIsLocalDiffeomorphOn I J n f s:fis aC^nlocal diffeomorphism onsIsLocalDiffeomorph I J n f:fis aC^nlocal diffeomorphism
Main results #
- Each of
Diffeomorph,IsLocalDiffeomorph,IsLocalDiffeomorphOnandIsLocalDiffeomorphAtimplies the next. IsLocalDiffeomorph.isLocalHomeomorph: a local diffeomorphisms is a local homeomorphism, similarly for local diffeomorphism onsIsLocalDiffeomorph.isOpen_range: the image of a local diffeomorphism is openIslocalDiffeomorph.diffeomorph_of_bijective: a bijective local diffeomorphism is a diffeomorphism
TODO #
- an injective local diffeomorphism is a diffeomorphism to its image
- each differential of a
C^ndiffeomorphism (n ≥ 1) is a linear equivalence. - if
fis a local diffeomorphism atx, the differentialmfderiv I J n f xis a continuous linear isomorphism. - conversely, if
fisC^natxandmfderiv I J n f xis a linear isomorphism,fis a local diffeomorphism atx. - if
fis a local diffeomorphism, each differentialmfderiv I J n f xis a continuous linear isomorphism. - Conversely, if
fisC^nand each differential is a linear isomorphism,fis a local diffeomorphism.
Implementation notes #
This notion of diffeomorphism is needed although there is already a notion of local structomorphism
because structomorphisms do not allow the model spaces H and H' of the two manifolds to be
different, i.e. for a structomorphism one has to impose H = H' which is often not the case in
practice.
Tags #
local diffeomorphism, manifold
structure
PartialDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_7)
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
extends
PartialEquiv
:
Type (max u_6 u_7)
A partial diffeomorphism on s is a function f : M → N such that f restricts to a
diffeomorphism s → t between open subsets of M and N, respectively.
This is an auxiliary definition and should not be used outside of this file.
- toFun : M → N
- invFun : N → M
- source : Set M
- target : Set N
- open_source : IsOpen self.source
- open_target : IsOpen self.target
- contMDiffOn_toFun : ContMDiffOn I J n (↑self.toPartialEquiv) self.source
- contMDiffOn_invFun : ContMDiffOn J I n self.invFun self.target
Instances For
theorem
PartialDiffeomorph.open_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(self : PartialDiffeomorph I J M N n)
:
IsOpen self.source
theorem
PartialDiffeomorph.open_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(self : PartialDiffeomorph I J M N n)
:
IsOpen self.target
theorem
PartialDiffeomorph.contMDiffOn_toFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(self : PartialDiffeomorph I J M N n)
:
ContMDiffOn I J n (↑self.toPartialEquiv) self.source
theorem
PartialDiffeomorph.contMDiffOn_invFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(self : PartialDiffeomorph I J M N n)
:
ContMDiffOn J I n self.invFun self.target
instance
instCoeFunPartialDiffeomorphForall
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_7)
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
:
CoeFun (PartialDiffeomorph I J M N n) fun (x : PartialDiffeomorph I J M N n) => M → N
Coercion of a PartialDiffeomorph to function.
Note that a PartialDiffeomorph is not DFunLike (like PartialHomeomorph),
as toFun doesn't determine invFun outside of target.
Equations
- instCoeFunPartialDiffeomorphForall I J M N n = { coe := fun (Φ : PartialDiffeomorph I J M N n) => ↑Φ.toPartialEquiv }
def
Diffeomorph.toPartialDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
PartialDiffeomorph I J M N n
A diffeomorphism is a partial diffeomorphism.
Equations
- h.toPartialDiffeomorph = { toPartialEquiv := h.toHomeomorph.toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }
Instances For
def
PartialDiffeomorph.toPartialHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
A partial diffeomorphism is also a local homeomorphism.
Equations
- Φ.toPartialHomeomorph = { toPartialEquiv := Φ.toPartialEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
Instances For
def
PartialDiffeomorph.symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
PartialDiffeomorph J I N M n
The inverse of a local diffeomorphism.
Equations
- Φ.symm = { toPartialEquiv := Φ.symm, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }
Instances For
theorem
PartialDiffeomorph.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
ContMDiffOn I J n (↑Φ.toPartialEquiv) Φ.source
theorem
PartialDiffeomorph.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
(hn : 1 ≤ n)
:
MDifferentiableOn I J (↑Φ.toPartialEquiv) Φ.source
theorem
PartialDiffeomorph.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
(hn : 1 ≤ n)
{x : M}
(hx : x ∈ Φ.source)
:
MDifferentiableAt I J (↑Φ.toPartialEquiv) x
def
IsLocalDiffeomorphAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
(f : M → N)
(x : M)
:
f : M → N is called a C^n local diffeomorphism at x iff there exist
open sets U ∋ x and V ∋ f x and a diffeomorphism Φ : U → V such that f = Φ on U.
Equations
- IsLocalDiffeomorphAt I J n f x = ∃ (Φ : PartialDiffeomorph I J M N n), x ∈ Φ.source ∧ Set.EqOn f (↑Φ.toPartialEquiv) Φ.source
Instances For
def
IsLocalDiffeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
(f : M → N)
(s : Set M)
:
f : M → N is called a C^n local diffeomorphism on s iff it is a local diffeomorphism
at each x : s.
Equations
- IsLocalDiffeomorphOn I J n f s = ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
Instances For
def
IsLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
(f : M → N)
:
f : M → N is a C^n local diffeomorphism iff it is a local diffeomorphism
at each x ∈ M.
Equations
- IsLocalDiffeomorph I J n f = ∀ (x : M), IsLocalDiffeomorphAt I J n f x
Instances For
theorem
isLocalDiffeomorphOn_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(s : Set M)
:
IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
theorem
isLocalDiffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
:
IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x
theorem
isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
:
IsLocalDiffeomorph I J n f ↔ IsLocalDiffeomorphOn I J n f Set.univ
theorem
IsLocalDiffeomorph.isLocalDiffeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(s : Set M)
:
IsLocalDiffeomorphOn I J n f s
Basic properties of local diffeomorphisms #
theorem
IsLocalDiffeomorphAt.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
ContMDiffAt I J n f x
A C^n local diffeomorphism at x is C^n differentiable at x.
theorem
IsLocalDiffeomorphAt.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hn : 1 ≤ n)
:
MDifferentiableAt I J f x
A local diffeomorphism at x is differentiable at x.
theorem
IsLocalDiffeomorphOn.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
:
ContMDiffOn I J n f s
A C^n local diffeomorphism on s is C^n on s.
theorem
IsLocalDiffeomorphOn.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
(hn : 1 ≤ n)
:
MDifferentiableOn I J f s
A local diffeomorphism on s is differentiable on s.
theorem
IsLocalDiffeomorph.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
ContMDiff I J n f
A C^n local diffeomorphism is C^n.
theorem
IsLocalDiffeomorph.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hn : 1 ≤ n)
:
MDifferentiable I J f
A C^n local diffeomorphism is differentiable.
theorem
Diffeomorph.isLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(Φ : Diffeomorph I J M N n)
:
IsLocalDiffeomorph I J n ⇑Φ
A C^n diffeomorphism is a local diffeomorphism.
theorem
IsLocalDiffeomorphOn.isLocalHomeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
:
A local diffeomorphism on s is a local homeomorphism on s.
theorem
IsLocalDiffeomorph.isLocalHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism is a local homeomorphism.
theorem
IsLocalDiffeomorph.isOpenMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism is an open map.
theorem
IsLocalDiffeomorph.isOpen_range
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism has open range.
def
IsLocalDiffeomorph.image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
The image of a local diffeomorphism is open.
Instances For
theorem
IsLocalDiffeomorph.image_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
noncomputable def
IslocalDiffeomorph.diffeomorph_of_bijective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hf' : Function.Bijective f)
:
Diffeomorph I J M N n
A bijective local diffeomorphism is a diffeomorphism.
Equations
- One or more equations did not get rendered due to their size.