Smooth immersions

In this file, we define immersions and prove some of their basic properties.

Main definitions

• Immersion I I' f n: a C^n map f : M → M' is an immersion iff its mfderiv is injective at each point
• InjImmersion: an immersion which is also injective

Main results

Implementation notes

The initial design of immersions only assumed injectivity of the differential. This is not sufficient to ensure immersions are C^n: While mathlib's mfderiv has junk value zero when f is not differentiable and the zero map is only injective if M has dimension zero (in which case f is always C^n), this argument only shows immersions are MDifferentiable, not C^n.

NOTE. This is not the correct definition in the infinite-dimensional context, but in finite dimensions, the general definition is equivalent to the one in this file.

Tags

manifold, immersion

structure Immersion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [instE : NormedAddCommGroup E] [instE' : NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (n : WithTop ℕ∞) : Prop

A C^n immersion f : M → M is a C^n map whose differential is injective at every point.

• contMDiff : ContMDiff I I' n f
• diff_injective (p : M) : Function.Injective ⇑(mfderiv I I' f p)

structure InjImmersion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [instE : NormedAddCommGroup E] [instE' : NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (n : WithTop ℕ∞) extends Immersion I I' f n : Prop

An injective C^n immersion

• contMDiff : ContMDiff I I' n f
• diff_injective (p : M) : Function.Injective ⇑(mfderiv I I' f p)
• injective : Function.Injective f