Composing immersions with local diffeomorphisms

Mathlib defines Manifold.IsImmersion by a normal form in charts and lists the composition of immersions as a TODO in Mathlib/Geometry/Manifold/Immersion.lean. The composition with a diffeomorphism on either side is in TauCeti.Geometry.Manifold.Immersion.Basic. This file treats the local version: composing with a C^n local diffeomorphism, on either side, preserves the immersion normal form at a point, with the same complement.

As for diffeomorphisms, nothing has to be recombined. A partial diffeomorphism Φ of the source carries a chart ψ of the maximal atlas to the chart Φ ≫ ψ, and f ∘ Φ read in it is f read in ψ. On the target, a partial diffeomorphism Θ near f x pulls a chart χ back to Θ⁻¹ ≫ χ, and Θ ∘ f read in it is f read in χ, once the source chart is shrunk so that f maps it into the source of Θ.

Since the inclusion of an open subset is a local diffeomorphism (TauCeti.isLocalDiffeomorph_subtype_val), being an immersion at a point can be tested after restricting the source, or corestricting the target, to an open subset.

Together with a topological embedding condition, this gives smooth embeddings: precomposing a smooth embedding with a local diffeomorphism which is a topological embedding, or postcomposing it with a map that is a local diffeomorphism along its image and a topological embedding on a set containing the image, gives a smooth embedding. Charts of the maximal atlas and their inverses are the basic examples of the latter (OpenPartialHomeomorph.isLocalDiffeomorphAt_of_mem_maximalAtlas and OpenPartialHomeomorph.isLocalDiffeomorphAt_symm_of_mem_maximalAtlas).

Main results

• TauCeti.isImmersionAtOfComplement_comp_isLocalDiffeomorphAt, TauCeti.isImmersionAtOfComplement_isLocalDiffeomorphAt_comp: the pointwise normal form with a fixed complement survives composing with a local diffeomorphism on the source or on the target.
• TauCeti.isImmersionAtOfComplement_comp_isLocalDiffeomorphAt_iff, TauCeti.isImmersionAt_comp_isLocalDiffeomorphAt_iff: on the source, precomposing with a local diffeomorphism also reflects the pointwise normal form, since a local inverse is again a local diffeomorphism.
• TauCeti.isImmersion_comp_isLocalDiffeomorph, TauCeti.isImmersion_isLocalDiffeomorphAt_comp: the corresponding statements for immersions.
• TauCeti.isSmoothEmbedding_comp_isLocalDiffeomorph, TauCeti.isSmoothEmbedding_isLocalDiffeomorphAt_comp: the corresponding statements for smooth embeddings.
• TauCeti.isImmersionAt_comp_subtypeVal_iff, TauCeti.isImmersionAt_codRestrict_opens_iff: immersions at a point, restricted to an open subset of the source or corestricted to an open subset of the target.
• TauCeti.isImmersion_comp_subtypeVal_iff, TauCeti.isImmersion_iff_of_isOpenCover: restriction to open source subsets and locality on open covers for finite-dimensional targets.
• Manifold.IsImmersion.codRestrict: an immersion with image in an open subset is an immersion into that open submanifold.
• TauCeti.isImmersion_subtypeVal_comp_iff, TauCeti.isSmoothEmbedding_subtypeVal_comp_iff, Manifold.IsSmoothEmbedding.comp_subtypeVal: immersions and smooth embeddings into an open submanifold, and smooth embeddings restricted to an open subset of the source.
• Manifold.IsImmersion.isLocalDiffeomorph: an immersion of a boundaryless manifold into a manifold modelled on a space of the same finite dimension is a local diffeomorphism.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, for immersions and their behaviour under composition.

Precomposing with a local diffeomorphism

theorem TauCeti.isImmersionAtOfComplement_comp_isLocalDiffeomorphAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) (h : Manifold.IsImmersionAtOfComplement F I J n f (g x)) : Manifold.IsImmersionAtOfComplement F I J n (f ∘ g) x

Precomposing with a local diffeomorphism of the source preserves the immersion normal form at a point, with the same complement: the domain chart is pulled back along a partial diffeomorphism representing the local diffeomorphism.

theorem TauCeti.isImmersionAt_comp_isLocalDiffeomorphAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) (h : Manifold.IsImmersionAt I J n f (g x)) : Manifold.IsImmersionAt I J n (f ∘ g) x

Precomposing with a local diffeomorphism of the source preserves being an immersion at a point.

theorem TauCeti.isImmersionOfComplement_comp_isLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} (hg : IsLocalDiffeomorph I I n g) (h : Manifold.IsImmersionOfComplement F I J n f) : Manifold.IsImmersionOfComplement F I J n (f ∘ g)

Precomposing an immersion with a fixed complement by a local diffeomorphism gives an immersion with the same complement.

theorem TauCeti.isImmersion_comp_isLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} (hg : IsLocalDiffeomorph I I n g) (h : Manifold.IsImmersion I J n f) : Manifold.IsImmersion I J n (f ∘ g)

Precomposing an immersion with a local diffeomorphism gives an immersion.

theorem TauCeti.isSmoothEmbedding_comp_isLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} (hg : IsLocalDiffeomorph I I n g) (hge : Topology.IsEmbedding g) (h : Manifold.IsSmoothEmbedding I J n f) : Manifold.IsSmoothEmbedding I J n (f ∘ g)

Precomposing a smooth embedding with a local diffeomorphism which is a topological embedding gives a smooth embedding.

theorem TauCeti.isImmersionAtOfComplement_comp_isLocalDiffeomorphAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) : Manifold.IsImmersionAtOfComplement F I J n (f ∘ g) x ↔ Manifold.IsImmersionAtOfComplement F I J n f (g x)

Precomposing with a local diffeomorphism of the source neither creates nor destroys the immersion normal form at a point: f ∘ g is an immersion at x, with complement F, exactly when f is one at g x.

theorem TauCeti.isImmersionAt_comp_isLocalDiffeomorphAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) : Manifold.IsImmersionAt I J n (f ∘ g) x ↔ Manifold.IsImmersionAt I J n f (g x)

Precomposing with a local diffeomorphism of the source neither creates nor destroys immersions at a point: f ∘ g is an immersion at x exactly when f is one at g x.

Postcomposing with a local diffeomorphism

theorem TauCeti.isImmersionAtOfComplement_isLocalDiffeomorphAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} {x : M} (hk : IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsImmersionAtOfComplement F I J n f x) : Manifold.IsImmersionAtOfComplement F I J n (k ∘ f) x

Postcomposing with a local diffeomorphism of the target preserves the immersion normal form at a point, with the same complement: the codomain chart is pulled back along a partial diffeomorphism representing the local diffeomorphism, after shrinking the domain chart so that the immersion maps it into the source of that partial diffeomorphism.

theorem TauCeti.isImmersionAt_isLocalDiffeomorphAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} {x : M} (hk : IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsImmersionAt I J n f x) : Manifold.IsImmersionAt I J n (k ∘ f) x

Postcomposing with a local diffeomorphism of the target preserves being an immersion at a point.

theorem TauCeti.isImmersionOfComplement_isLocalDiffeomorphAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} (hk : ∀ (x : M), IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsImmersionOfComplement F I J n f) : Manifold.IsImmersionOfComplement F I J n (k ∘ f)

Postcomposing an immersion with a fixed complement by a map which is a local diffeomorphism at every point of its image gives an immersion with the same complement.

theorem TauCeti.isImmersion_isLocalDiffeomorphAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} (hk : ∀ (x : M), IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsImmersion I J n f) : Manifold.IsImmersion I J n (k ∘ f)

Postcomposing an immersion with a map which is a local diffeomorphism at every point of its image gives an immersion.

theorem TauCeti.isSmoothEmbedding_isLocalDiffeomorphAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} {s : Set N} (hk : ∀ (x : M), IsLocalDiffeomorphAt J J n k (f x)) (hfs : Set.range f ⊆ s) (hks : Topology.IsEmbedding (s.domRestrict k)) (h : Manifold.IsSmoothEmbedding I J n f) : Manifold.IsSmoothEmbedding I J n (k ∘ f)

Postcomposing a smooth embedding with a map which is a local diffeomorphism at every point of its image, and a topological embedding on a set containing the image, gives a smooth embedding.

Open subsets

theorem TauCeti.isImmersionAt_comp_subtypeVal_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] {U : TopologicalSpace.Opens M} {x : ↥U} : Manifold.IsImmersionAt I J n (f ∘ Subtype.val) x ↔ Manifold.IsImmersionAt I J n f ↑x

A map is an immersion at a point of an open subset of its source exactly when its restriction to that subset is.

theorem TauCeti.isImmersion_comp_subtypeVal_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E'] [IsManifold I n M] {U : TopologicalSpace.Opens M} : Manifold.IsImmersion I J n (f ∘ Subtype.val) ↔ ∀ x ∈ U, Manifold.IsImmersionAt I J n f x

For a finite-dimensional target model, restriction to an open source subset is an immersion exactly when the original map is an immersion at every point of that subset.

theorem TauCeti.isImmersion_iff_of_isOpenCover {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E'] [IsManifold I n M] {ι : Type u_11} {U : ι → TopologicalSpace.Opens M} (hU : TopologicalSpace.IsOpenCover U) : Manifold.IsImmersion I J n f ↔ ∀ (i : ι), Manifold.IsImmersion I J n (f ∘ Subtype.val)

For a finite-dimensional target model, being an immersion can be checked on an arbitrary open cover of the source.

theorem TauCeti.isImmersionAt_codRestrict_opens_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n N] {U : TopologicalSpace.Opens N} (hf : ∀ (y : M), f y ∈ U) {x : M} : Manifold.IsImmersionAt I J n (fun (y : M) => ⟨f y, ⋯⟩) x ↔ Manifold.IsImmersionAt I J n f x

A map into an open subset of a manifold is an immersion at a point exactly when its composition with the inclusion of the subset is.

Codomain restriction and the inverse function theorem

theorem Manifold.IsImmersion.codRestrict {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n N] (hf : IsImmersion I J n f) (U : TopologicalSpace.Opens N) (h : ∀ (x : M), f x ∈ U) : IsImmersion I J n fun (x : M) => ⟨f x, ⋯⟩

An immersion with image in an open subset U stays an immersion into the open submanifold U.

theorem TauCeti.isImmersion_subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold J n N] {U : TopologicalSpace.Opens N} {g : M → ↥U} : Manifold.IsImmersion I J n (Subtype.val ∘ g) ↔ Manifold.IsImmersion I J n g

A map into an open submanifold U is an immersion exactly when its composition with the inclusion of U is.

theorem TauCeti.isSmoothEmbedding_subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold J n N] {U : TopologicalSpace.Opens N} {g : M → ↥U} : Manifold.IsSmoothEmbedding I J n (Subtype.val ∘ g) ↔ Manifold.IsSmoothEmbedding I J n g

A map into an open submanifold U is a smooth embedding exactly when its composition with the inclusion of U is.

theorem Manifold.IsSmoothEmbedding.comp_subtypeVal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] (h : IsSmoothEmbedding I J n f) (U : TopologicalSpace.Opens M) : IsSmoothEmbedding I J n (f ∘ Subtype.val)

Restricting a smooth embedding to an open subset of its source gives a smooth embedding.

theorem Manifold.IsImmersion.isLocalDiffeomorph {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {n : WithTop ℕ∞} {𝕂 : Type u_11} [RCLike 𝕂] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [FiniteDimensional 𝕂 F] {K : ModelWithCorners 𝕂 F H} {F' : Type u_13} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] [FiniteDimensional 𝕂 F'] {K' : ModelWithCorners 𝕂 F' G} {X : Type u_14} [TopologicalSpace X] [ChartedSpace H X] {Y : Type u_15} [TopologicalSpace Y] [ChartedSpace G Y] [IsManifold K n X] [IsManifold K' n Y] [BoundarylessManifold K X] {g : X → Y} (hg : IsImmersion K K' n g) (hd : Module.finrank 𝕂 F = Module.finrank 𝕂 F') (hn : 1 ≤ n) : IsLocalDiffeomorph K K' n g

An immersion of a boundaryless manifold into a manifold modelled on a space of the same finite dimension is a local diffeomorphism.