Immersions in the sense of differentials

Given a map f : M → N between manifolds, we say f is an immersion in the sense of differentials at x if and only if the mfderiv of f at x splits, i.e. admits a continuous left inverse. (If N is finite-dimensional, this is equivalent to injectivity of the mfderiv.) Under (relatively mild) conditions, this is equivalent to being an immersion at x. This is not true in full generality; there are counterexamples involving manifolds with boundary. This equivalence will be shown in a future PR.

IsDiffImmersionAt always behaves nicely under composition: future PRs will use the above equivalence to prove that immersions compose (in nice situations).

Main definitions and results

• IsDiffImmersionAt: f is an immersion at x in the sense of differentials iff mfderiv I J f x has a continuous left inverse
• IsLocalDiffeomorphAt.isDiffImmersionAt: if f is a local diffeomorphism at x, then f is an immersion at x in the sense of differentials.
• IsDiffImmersionAt.comp: if f is an immersion at x, and g is an immersion at f x (both in the sense of differentials), then g ∘ f is an immersion (of differentials) at x
• IsDiffImmersionAt.of_comp: if g ∘ f is an immersion at x (of differentials), then (assuming f and g are differentiable at x resp. f x), f is also an immersion at x
• IsDiffImmersionAt.prodMap: if f is an immersion at x and g is an immersion at y, then f × g is an immersion at (x, y) (all in the sense of differentials)
• IsDiffImmersionAt.of_injective_of_finiteDimensional: if f : M → N has injective mfderiv at x and N is finite-dimensional, then f is an immersion at x

def IsDiffImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (x : M) : Prop

We say a map f : M → M is an immersion at x in the sense of differentials if mfderiv I I' f x splits, i.e. has a continuous left inverse.

In nice situations (but not always), this is equivalent to IsImmersionAt. Please use IsImmersionAt in general.

Equations

• IsDiffImmersionAt I I' f x = (mfderiv% f x).HasLeftInverse

theorem isDiffImmersionAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} : IsDiffImmersionAt I I' f x ↔ (mfderiv% f x).HasLeftInverse

theorem IsDiffImmersionAt.mfderiv_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) : Function.Injective ⇑(mfderiv% f x)

theorem IsDiffImmersionAt.mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) : MDiffAt f x

theorem IsDiffImmersionAt.continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) : ContinuousAt f x

theorem IsDiffImmersionAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f g : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) (hfg : g =ᶠ[nhds x] f) : IsDiffImmersionAt I I' g x

theorem IsDiffImmersionAt.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {G' : Type u_9} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M'} {x : M} {y : N} (hf : IsDiffImmersionAt I I' f x) {g : N → N'} (hg : IsDiffImmersionAt J J' g y) : IsDiffImmersionAt (I.prod J) (I'.prod J') (Prod.map f g) (x, y)

If f is an immersion at x and g is an immersion at y, then f × g is an immersion at (x, y) (all in the sense of differentials).

theorem IsDiffImmersionAt.of_mfderiv_isInvertible {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} (hf : (mfderiv% f x).IsInvertible) : IsDiffImmersionAt I I' f x

theorem IsLocalDiffeomorphAt.isDiffImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} {f : M → M'} {x : M} (hf : IsLocalDiffeomorphAt I I' n f x) (hn : n ≠ 0) : IsDiffImmersionAt I I' f x

If f is a local diffeomorphism at x, then f is an immersion at x (in the sense of differentials).

theorem ContinuousLinearEquiv.isDiffImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) {x : E} : IsDiffImmersionAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) (⇑f) x

A continuous linear equivalence is an immersion at every point (in the sense of differentials).

theorem IsDiffImmersionAt.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {f : M → M'} {x : M} {g : M' → N} (hg : IsDiffImmersionAt I' J g (f x)) (hf : IsDiffImmersionAt I I' f x) : IsDiffImmersionAt I J (g ∘ f) x

If f is an immersion at x, and g is an immersion at f x (both in the sense of differentials), then g ∘ f is an immersion at x.

theorem IsDiffImmersionAt.of_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {f : M → M'} {x : M} {g : M' → N} (hf : MDiffAt f x) (hg : MDiffAt g (f x)) (hfg : IsDiffImmersionAt I J (g ∘ f) x) : IsDiffImmersionAt I I' f x

If g ∘ f is an immersion at x (of differentials), then (assuming f and g are differentiable at x resp. f x), f is also an immersion at x.

theorem IsDiffImmersionAt.comp_isInvertible_mfderiv_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) {f₀ : N → M} {y : N} (hxy : f₀ y = x) (hf₀ : (mfderiv% f₀ y).IsInvertible) : IsDiffImmersionAt J I' (f ∘ f₀) y

theorem IsDiffImmersionAt.comp_isLocalDiffeomorphAt_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) {f₀ : N → M} {y : N} (hxy : f₀ y = x) (hf₀ : IsLocalDiffeomorphAt J I n f₀ y) (hn : n ≠ 0) : IsDiffImmersionAt J I' (f ∘ f₀) y

theorem IsDiffImmersionAt.comp_isLocalDiffeomorphAt_left_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → M'} {x : M} {f₀ : N → M} {y : N} (hxy : f₀ y = x) (hf₀ : IsLocalDiffeomorphAt J I n f₀ y) (hn : n ≠ 0) : IsDiffImmersionAt I I' f x ↔ IsDiffImmersionAt J I' (f ∘ f₀) y

theorem IsDiffImmersionAt.comp_isInvertible_mfderiv_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) {g : M' → N} (hg : (mfderiv% g (f x)).IsInvertible) : IsDiffImmersionAt I J (g ∘ f) x

theorem IsDiffImmersionAt.comp_isLocalDiffeomorphAt_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → M'} {x : M} (hf : IsDiffImmersionAt I I' f x) {g : M' → N} (hg : IsLocalDiffeomorphAt I' J n g (f x)) (hn : n ≠ 0) : IsDiffImmersionAt I J (g ∘ f) x

theorem IsDiffImmersionAt.comp_isLocalDiffeomorphAt_right_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {G : Type u_8} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → M'} {x : M} (hf : ContinuousAt f x) {g : M' → N} (hg : IsLocalDiffeomorphAt I' J n g (f x)) (hn : n ≠ 0) : IsDiffImmersionAt I I' f x ↔ IsDiffImmersionAt I J (g ∘ f) x

theorem IsDiffImmersionAt.of_injective_of_finiteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E'] (hf' : Function.Injective ⇑(mfderiv% f x)) : IsDiffImmersionAt I I' f x

If mfderiv I J f x is injective and N is finite-dimensional, then f is an immersion (in the sense of differentials) at x.