Composing bundled smooth embeddings with local diffeomorphisms #
TauCeti.Geometry.Manifold.Immersion.LocalDiffeomorph shows that the predicate
Manifold.IsSmoothEmbedding survives precomposition with a local diffeomorphism which is a
topological embedding, and postcomposition with a map which is a local diffeomorphism along a set
containing the image and a topological embedding on that set. This file packages these as
operations on the bundled type TauCeti.SmoothEmbedding, in the way
TauCeti.SmoothEmbedding.compDiffeomorph and TauCeti.SmoothEmbedding.transDiffeomorph package
composition with diffeomorphisms.
The basic example of the second operation is a chart: a smooth embedding whose image lies in the source of a chart of the maximal atlas, read in that chart, is a smooth embedding into the model space.
Main definitions #
TauCeti.SmoothEmbedding.compLocalDiffeomorph: precompose with a local diffeomorphism which is a topological embedding.TauCeti.SmoothEmbedding.transLocalDiffeomorph: postcompose with a map which is a local diffeomorphism along a set containing the image, and a topological embedding on that set.TauCeti.SmoothEmbedding.transChart: read a smooth embedding in a chart of the maximal atlas whose source contains its image.TauCeti.SmoothEmbedding.codRestrict: a smooth embedding whose image lies in an open subset, as a smooth embedding into that open submanifold.
Main results #
TauCeti.SmoothEmbedding.isLocalDiffeomorph: a smooth embedding of a boundaryless manifold into a manifold modelled on a space of the same finite dimension is a local diffeomorphism.
def
TauCeti.SmoothEmbedding.compLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold I n M']
(f : SmoothEmbedding I J n M N)
(g : M' → M)
(hg : IsLocalDiffeomorph I I n g)
(hge : Topology.IsEmbedding g)
:
SmoothEmbedding I J n M' N
Precompose a smooth embedding with a local diffeomorphism which is a topological embedding.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_compLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold I n M']
(f : SmoothEmbedding I J n M N)
(g : M' → M)
(hg : IsLocalDiffeomorph I I n g)
(hge : Topology.IsEmbedding g)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.compLocalDiffeomorph_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M']
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold I n M']
(f : SmoothEmbedding I J n M N)
(g : M' → M)
(hg : IsLocalDiffeomorph I I n g)
(hge : Topology.IsEmbedding g)
(x : M')
:
def
TauCeti.SmoothEmbedding.transLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace G P]
{n : WithTop ℕ∞}
[IsManifold J n P]
(f : SmoothEmbedding I J n M N)
(k : N → P)
{s : Set N}
(hk : ∀ y ∈ s, IsLocalDiffeomorphAt J J n k y)
(hks : Topology.IsEmbedding (s.domRestrict k))
(hfs : Set.range ⇑f ⊆ s)
:
SmoothEmbedding I J n M P
Postcompose a smooth embedding with a map which is a local diffeomorphism at every point of a set containing the image, and a topological embedding on that set.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_transLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace G P]
{n : WithTop ℕ∞}
[IsManifold J n P]
(f : SmoothEmbedding I J n M N)
(k : N → P)
{s : Set N}
(hk : ∀ y ∈ s, IsLocalDiffeomorphAt J J n k y)
(hks : Topology.IsEmbedding (s.domRestrict k))
(hfs : Set.range ⇑f ⊆ s)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.transLocalDiffeomorph_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace G P]
{n : WithTop ℕ∞}
[IsManifold J n P]
(f : SmoothEmbedding I J n M N)
(k : N → P)
{s : Set N}
(hk : ∀ y ∈ s, IsLocalDiffeomorphAt J J n k y)
(hks : Topology.IsEmbedding (s.domRestrict k))
(hfs : Set.range ⇑f ⊆ s)
(x : M)
:
def
TauCeti.SmoothEmbedding.transChart
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n G]
(f : SmoothEmbedding I J n M N)
{φ : OpenPartialHomeomorph N G}
(hφ : φ ∈ IsManifold.maximalAtlas J n N)
(hf : Set.range ⇑f ⊆ φ.source)
:
SmoothEmbedding I J n M G
A smooth embedding whose image lies in the source of a chart of the maximal atlas, read in that chart: a smooth embedding into the model space.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_transChart
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n G]
(f : SmoothEmbedding I J n M N)
{φ : OpenPartialHomeomorph N G}
(hφ : φ ∈ IsManifold.maximalAtlas J n N)
(hf : Set.range ⇑f ⊆ φ.source)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.transChart_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n G]
(f : SmoothEmbedding I J n M N)
{φ : OpenPartialHomeomorph N G}
(hφ : φ ∈ IsManifold.maximalAtlas J n N)
(hf : Set.range ⇑f ⊆ φ.source)
(x : M)
:
theorem
Manifold.IsSmoothEmbedding.codRestrict
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n N]
{f : M → N}
(hf : IsSmoothEmbedding I J n f)
(U : TopologicalSpace.Opens N)
(h : ∀ (x : M), f x ∈ U)
:
IsSmoothEmbedding I J n fun (x : M) => ⟨f x, ⋯⟩
A smooth embedding with image in an open subset U stays a smooth embedding into the open
submanifold U.
noncomputable def
TauCeti.SmoothEmbedding.codRestrict
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
(U : TopologicalSpace.Opens N)
(h : ∀ (x : M), f x ∈ U)
:
SmoothEmbedding I J n M ↥U
A smooth embedding whose image lies in the open subset U, as a smooth embedding into the
open submanifold U.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.val_codRestrict_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
(U : TopologicalSpace.Opens N)
(h : ∀ (x : M), f x ∈ U)
(x : M)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.val_comp_codRestrict
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold J n N]
(f : SmoothEmbedding I J n M N)
(U : TopologicalSpace.Opens N)
(h : ∀ (x : M), f x ∈ U)
:
theorem
TauCeti.SmoothEmbedding.isLocalDiffeomorph
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{n : WithTop ℕ∞}
{𝕂 : Type u_10}
[RCLike 𝕂]
{F : Type u_11}
[NormedAddCommGroup F]
[NormedSpace 𝕂 F]
[FiniteDimensional 𝕂 F]
{K : ModelWithCorners 𝕂 F H}
{F' : Type u_12}
[NormedAddCommGroup F']
[NormedSpace 𝕂 F']
[FiniteDimensional 𝕂 F']
{K' : ModelWithCorners 𝕂 F' G}
{X : Type u_13}
[TopologicalSpace X]
[ChartedSpace H X]
{Y : Type u_14}
[TopologicalSpace Y]
[ChartedSpace G Y]
[IsManifold K n X]
[IsManifold K' n Y]
[BoundarylessManifold K X]
(f : SmoothEmbedding K K' n X Y)
(hd : Module.finrank 𝕂 F = Module.finrank 𝕂 F')
(hn : 1 ≤ n)
:
IsLocalDiffeomorph K K' n ⇑f
A smooth embedding of a boundaryless manifold into a manifold modelled on a space of the same finite dimension is a local diffeomorphism.