Immersion normal forms from split differentials

A map from a real or complex normed space to a Banach space with a continuous left inverse to its derivative has the local normal form of an immersion. The map need only be C^n on an open neighbourhood, with 1 ≤ n. This turns a differential splitting into actual slice charts, as needed to extend data from the image of an embedded map.

The construction adds a closed complement to the source and applies the inverse function theorem to the resulting map. It uses Mathlib's ContinuousLinearMap.HasLeftInverse.complement and ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl, and Tau Ceti's smooth inverse function theorem on an open neighbourhood.

The same criterion holds for maps between manifolds without boundary. A normal form of a map read in the preferred extended charts is carried back to the manifolds by composing its charts with the preferred charts (Manifold.IsImmersionAtOfComplement.of_writtenInExtChartAt); on a boundaryless model the manifold derivative is the derivative of the map read in these charts. So, for a finite-dimensional target model, a smooth map with injective differential everywhere is an immersion (ContMDiff.isImmersion_of_injective_mfderiv). A parameter-preserving map (p, x) ↦ (p, G (p, x)) is then an immersion at every point where its slice x ↦ G (p, x) is one in the sense of differentials, as for the space-time track of a moving embedded submanifold. Likewise, postcomposing an immersion with a diffeomorphism onto a manifold with a different finite-dimensional model gives an immersion (Diffeomorph.isImmersion_comp), for example after exchanging the factors of a product. In particular, a C^n map with a left inverse near a point, differentiable at the image of that point, is an immersion there (ContMDiffOn.isImmersionAt_of_comp_eventuallyEq_id), and a C^n map with a global left inverse differentiable along its image is an immersion (ContMDiff.isImmersion_of_leftInverse). Pairing an immersion with any C^n map into a finite-dimensional manifold gives an immersion (Manifold.IsImmersion.prodMk).

Reference: M. Hirsch, Differential Topology, Chapter 1, §3 (the local immersion theorem), and Chapter 8, §1 (its use in isotopy extension).

theorem ContDiffOn.isImmersionAt_of_hasLeftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {n : WithTop ℕ∞} {f : E → F} {s : Set E} {x : E} (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) (hdf : (fderiv 𝕜 f x).HasLeftInverse) : Manifold.IsImmersionAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n f x

A C^n map on an open set has an immersion normal form at any point where its derivative admits a continuous linear left inverse. Both spaces may be infinite dimensional.

theorem ContDiffOn.isImmersionAt_iff_hasLeftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {n : WithTop ℕ∞} {f : E → F} {s : Set E} {x : E} (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) : Manifold.IsImmersionAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n f x ↔ (fderiv 𝕜 f x).HasLeftInverse

For a C^n map on an open subset of a normed space with values in a Banach space, the immersion normal form is equivalent to the derivative having a continuous linear left inverse.

theorem ContDiffOn.isImmersionAt_iff_injective_fderiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} {s : Set E} {x : E} [FiniteDimensional 𝕜 F] (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) : Manifold.IsImmersionAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n f x ↔ Function.Injective ⇑(fderiv 𝕜 f x)

For a finite-dimensional target, a C^n map on an open set has the immersion normal form exactly when its derivative is injective.

theorem Manifold.IsImmersionAtOfComplement.of_writtenInExtChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] (hf : ContinuousAt f x) (h : IsImmersionAtOfComplement F (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n (writtenInExtChartAt I J x f) (↑(extChartAt I x) x)) : IsImmersionAtOfComplement F I J n f x

An immersion normal form of a map between boundaryless manifolds, read in the preferred extended charts, is an immersion normal form of the map itself, with the same complement.

theorem ContMDiffOn.isImmersionAt_of_hasLeftInverse_mfderiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) (hdf : (mfderiv% f x).HasLeftInverse) : Manifold.IsImmersionAt I J n f x

A C^n map on an open subset of a boundaryless manifold, with values in a boundaryless manifold, is an immersion at any point where its manifold derivative admits a continuous linear left inverse.

theorem ContMDiffOn.isImmersionAt_iff_hasLeftInverse_mfderiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) : Manifold.IsImmersionAt I J n f x ↔ (mfderiv% f x).HasLeftInverse

For a C^n map on an open subset of a boundaryless manifold, with values in a boundaryless manifold, the immersion normal form is equivalent to the manifold derivative having a continuous linear left inverse.

theorem ContMDiffOn.isImmersionAt_iff_injective_mfderiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} [FiniteDimensional 𝕜 E'] (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) : Manifold.IsImmersionAt I J n f x ↔ Function.Injective ⇑(mfderiv% f x)

For a finite-dimensional target model, a C^n map on an open subset of a boundaryless manifold, with values in a boundaryless manifold, has the immersion normal form exactly when its manifold derivative is injective.

theorem ContMDiff.isImmersion_of_injective_mfderiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} [FiniteDimensional 𝕜 E'] (hf : ContMDiff I J n f) (hn : 1 ≤ n) (hdf : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) : Manifold.IsImmersion I J n f

A C^n map between boundaryless manifolds, with a finite-dimensional target model, is an immersion when its manifold derivative is injective at every point.

theorem ContMDiffOn.isImmersionAt_of_comp_eventuallyEq_id {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M} {x : M} {g : N → M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s) (hn : 1 ≤ n) (hg : MDiffAt g (f x)) (hgf : g ∘ f =ᶠ[nhds x] id) : Manifold.IsImmersionAt I J n f x

A C^n map on an open subset of a boundaryless manifold, with values in a boundaryless manifold, is an immersion at any point x near which it has a left inverse g differentiable at f x: the manifold derivative of g at f x is then a continuous linear left inverse of that of f at x.

theorem ContMDiff.isImmersion_of_leftInverse {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} [FiniteDimensional 𝕜 E'] {g : N → M} (hf : ContMDiff I J n f) (hn : 1 ≤ n) (hg : ∀ (x : M), MDiffAt g (f x)) (hgf : Function.LeftInverse g f) : Manifold.IsImmersion I J n f

A C^n map between boundaryless manifolds, with 1 ≤ n, which has a left inverse differentiable along its image is an immersion.

theorem ContMDiff.isImmersionAt_fst_prod {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {EP : Type u_8} {HP : Type u_9} {P : Type u_10} [NormedAddCommGroup EP] [NormedSpace 𝕜 EP] [CompleteSpace EP] [TopologicalSpace HP] {IP : ModelWithCorners 𝕜 EP HP} [TopologicalSpace P] [ChartedSpace HP P] [IP.Boundaryless] [IsManifold IP n P] {G✝ : P × M → N} (hG : ContMDiff (IP.prod I) J n G✝) (hn : 1 ≤ n) {q : P × M} (hq : IsDiffImmersionAt I J (fun (x : M) => G✝ (q.1, x)) q.2) : Manifold.IsImmersionAt (IP.prod I) (IP.prod J) n (fun (q : P × M) => (q.1, G✝ q)) q

A C^n parameter-preserving map (p, x) ↦ (p, G (p, x)) between boundaryless manifolds is an immersion at every point where its slice at the fixed parameter is an immersion in the sense of differentials.

theorem Diffeomorph.isImmersion_comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [IsManifold I n M] {f : M → N} {EP : Type u_8} {HP : Type u_9} {P : Type u_10} [NormedAddCommGroup EP] [NormedSpace 𝕜 EP] [TopologicalSpace HP] {IP : ModelWithCorners 𝕜 EP HP} [TopologicalSpace P] [ChartedSpace HP P] [IP.Boundaryless] [IsManifold IP n P] [FiniteDimensional 𝕜 EP] (Φ : Diffeomorph J IP N P n) (hn : 1 ≤ n) (hf : Manifold.IsImmersion I J n f) : Manifold.IsImmersion I IP n (⇑Φ ∘ f)

Postcomposing an immersion from a boundaryless manifold with a diffeomorphism of the target onto a boundaryless manifold gives an immersion, also when the new target has a different model, provided that model is finite dimensional.

theorem Manifold.IsImmersion.prodMk {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] {f : M → N} {EP : Type u_8} {HP : Type u_9} {P : Type u_10} [NormedAddCommGroup EP] [NormedSpace 𝕜 EP] [TopologicalSpace HP] {IP : ModelWithCorners 𝕜 EP HP} [TopologicalSpace P] [ChartedSpace HP P] [IP.Boundaryless] [IsManifold IP n P] [FiniteDimensional 𝕜 E'] [FiniteDimensional 𝕜 EP] {g : M → P} (hf : IsImmersion I J n f) (hg : ContMDiff I IP n g) (hn : 1 ≤ n) : IsImmersion I (J.prod IP) n fun (x : M) => (f x, g x)

Pairing an immersion from a boundaryless manifold with a C^n map, both with values in boundaryless manifolds with finite-dimensional models, gives an immersion x ↦ (f x, g x).