Smooth immersions

In this file, we define C^n immersions between C^n manifolds. The correct definition in the infinite-dimensional setting differs from the standard finite-dimensional definition (concerning the mfderiv being injective): future pull requests will prove that our definition implies the latter, and that both are equivalent for finite-dimensional manifolds.

This definition can be conveniently formulated in terms of local properties: f is an immersion at x iff there exist suitable charts near x and f x such that f has a nice form w.r.t. these charts. Most results below can be deduced from more abstract results about such local properties. This shortens the overall argument, as the definition of submersions has the same general form.

Main definitions

• IsImmersionAtOfComplement F I J n f x means a map f : M → N between C^n manifolds M and N is an immersion at x : M: there are charts φ and ψ of M and N around x and f x, respectively, such that in these charts, f looks like u ↦ (u, 0), w.r.t. some equivalence E' ≃L[𝕜] E × F. We do not demand that f be differentiable (this follows from this definition).
• IsImmersionAt I J n f x means that f is a C^n immersion at x : M for some choice of a complement F of the model normed space E of M in the model normed space E' of N. In most cases, prefer this definition over IsImmersionAtOfComplement.
• IsImmersionOfComplement F I J n f means f : M → N is an immersion at every point x : M, w.r.t. the chosen complement F.
• IsImmersion I J n f means f : M → N is an immersion at every point x : M, w.r.t. some global choice of complement.

Main results

• IsImmersionAt.congr_of_eventuallyEq: being an immersion is a local property. If f and g agree near x and f is an immersion at x, so is g
• IsImmersionAtOfComplement.congr_F, IsImmersionOfComplement.congr_F: being an immersion (at x) w.r.t. F is stable under replacing the complement F by an isomorphic copy

Implementation notes

• In most applications, there is no need to control the chosen complement in the definition of immersions, so IsImmersion(At) is perfectly fine to use. Such control will be helpful, however, when considering the local characterisation of submanifolds: locally, a submanifold is described either as the image of an immersion, or the preimage of a submersion --- w.r.t. the same complement. Having access to a definition version with complements allows stating this equivalence cleanly.
• To avoid a free universe variable in IsImmersion(At), we ask for a complement in the same universe as the model normed space for N. We provide convenience constructors which do not have this restriction (recovering usability). The underlying observation is that the equivalence in the definition of immersions allows shrinking the universe of the complement: this is implemented in IsImmersion(At)OfComplement.small and IsImmersion(At)OfComplement.smallEquiv.

TODO

• The converse to IsImmersionAtOfComplement.congr_F also holds: any two complements are isomorphic, as they are isomorphic to the cokernel of the differential mfderiv I J f x.
• The set where IsImmersionAt(OfComplement) holds is open.
• IsImmersionAt.contMDiffAt: if f is an immersion at x, it is C^n at x.
• IsImmersion.contMDiff: if f is an immersion, it is C^n.
• IsImmersionAt.prodMap: the product of two immersions is an immersion.
• If f is an immersion at x, its differential splits, hence is injective.
• If f : M → N is a map between Banach manifolds, mfderiv I J f x splitting implies f is an immersion at x. (This requires the inverse function theorem.)
• IsImmersionAt.comp: if f : M → N and g: N → N' are maps between Banach manifolds such that f is an immersion at x : M and g is an immersion at f x, then g ∘ f is an immersion at x.
• IsImmersion.comp: the composition of immersions (between Banach manifolds) is an immersion
• If f : M → N is a map between finite-dimensional manifolds, mfderiv I J f x being injective implies f is an immersion at x.

References

• Juan Margalef-Roig and Enrique Outerelo Dominguez, Differential topology

def Manifold.ImmersionAtProp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) (M : Type u_11) [TopologicalSpace M] (N : Type u_13) [TopologicalSpace N] : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop

The local property of being an immersion at a point: f : M → N is an immersion at x if there exist charts φ and ψ of M and N around x and f x, respectively, such that in these charts, f looks like the inclusion u ↦ (u, 0).

This definition has a fixed parameter F, which is a choice of complement of E in the model normed space E' of N: being an immersion at x includes a choice of linear isomorphism between E × F and E'.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.isLocalSourceTargetProperty_immersionAtProp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] {N : Type u_13} [TopologicalSpace N] : IsLocalSourceTargetProperty (ImmersionAtProp F I J M N)

Being an immersion at x is a local property.

@[irreducible]

def Manifold.IsImmersionAtOfComplement {𝕜 : Type u_15} [NontriviallyNormedField 𝕜] {E : Type u_16} {E'' : Type u_17} (F : Type u_18) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_19} [TopologicalSpace H] {G : Type u_20} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_21} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_22} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop

f : M → N is a C^n immersion at x if there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0). Additionally, we demand that f map φ.source into ψ.source.

NB. We don't know the particular atlasses used for M and N, so asking for φ and ψ to be in the atlas would be too optimistic: lying in the maximalAtlas is sufficient.

This definition has a fixed parameter F, which is a choice of complement of E in E': being an immersion at x includes a choice of linear isomorphism between E × F and E'. While the particular choice of complement is often not important, chosing a complement is useful in some settings, such as proving that embedded submanifolds are locally given either by an immersion or a submersion. Unless you have a particular reason, prefer to use IsImmersionAt instead.

Equations

• Manifold.IsImmersionAtOfComplement F I J n f x = Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.ImmersionAtProp F I J M N)

theorem Manifold.IsImmersionAtOfComplement_def {𝕜 : Type u_15} [NontriviallyNormedField 𝕜] {E : Type u_16} {E'' : Type u_17} (F : Type u_18) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_19} [TopologicalSpace H] {G : Type u_20} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_21} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_22} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) : IsImmersionAtOfComplement F I J n f x = LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp F I J M N)

theorem Manifold.IsImmersionAt_def {𝕜 : Type u_15} [NontriviallyNormedField 𝕜] {E : Type u_16} {E'' : Type u_17} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_18} [TopologicalSpace H] {G : Type u_19} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_20} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_21} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) : IsImmersionAt I J n f x = ∃ (F : Type u_17) (x_1 : NormedAddCommGroup F) (x_2 : NormedSpace 𝕜 F), IsImmersionAtOfComplement F I J n f x

@[irreducible]

def Manifold.IsImmersionAt {𝕜 : Type u_15} [NontriviallyNormedField 𝕜] {E : Type u_16} {E'' : Type u_17} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_18} [TopologicalSpace H] {G : Type u_19} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_20} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_21} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop

f : M → N is a C^n immersion at x if there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0). Additionally, we demand that f map φ.source into ψ.source.

NB. We don't know the particular atlasses used for M and N, so asking for φ and ψ to be in the atlas would be too optimistic: lying in the maximalAtlas is sufficient.

Implicit in this definition is an abstract choice F of a complement of E in E': being an immersion at x includes a choice of linear isomorphism between E × F and E', which is where the choice of F enters. If you need stronger control over the complement F, use IsImmersionAtOfComplement instead.

Equations

• Manifold.IsImmersionAt I J n f x = ∃ (F : Type ?u.29) (x_1 : NormedAddCommGroup F) (x_2 : NormedSpace 𝕜 F), Manifold.IsImmersionAtOfComplement F I J n f x

theorem Manifold.IsImmersionAtOfComplement.mk_of_charts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G) (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source) (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hsource : domChart.source ⊆ f ⁻¹' codChart.source) (hwrittenInExtend : Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun (x : E) => (x, 0)) (domChart.extend I).target) : IsImmersionAtOfComplement F I J n f x

theorem Manifold.IsImmersionAtOfComplement.mk_of_continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G) (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source) (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hwrittenInExtend : Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun (x : E) => (x, 0)) (domChart.extend I).target) : IsImmersionAtOfComplement F I J n f x

f : M → N is a C^n immersion at x if there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0). This version does not assume that f maps φ.source to ψ.source, but that f is continuous at x.

def Manifold.IsImmersionAtOfComplement.domChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph M H

A choice of chart on the domain M of an immersion f at x: w.r.t. this chart and the data h.codChart and h.equiv, f will look like an inclusion u ↦ (u, 0) in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.codChart and h.codChart.

Equations

• h.domChart = ⋯.domChart

def Manifold.IsImmersionAtOfComplement.codChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph N G

A choice of chart on the co-domain N of an immersion f at x: w.r.t. this chart and the data h.domChart and h.equiv, f will look like an inclusion u ↦ (u, 0) in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.equiv and h.domChart.

Equations

• h.codChart = ⋯.codChart

theorem Manifold.IsImmersionAtOfComplement.mem_domChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : x ∈ h.domChart.source

theorem Manifold.IsImmersionAtOfComplement.mem_codChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : f x ∈ h.codChart.source

theorem Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : h.domChart ∈ IsManifold.maximalAtlas I n M

theorem Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : h.codChart ∈ IsManifold.maximalAtlas J n N

theorem Manifold.IsImmersionAtOfComplement.source_subset_preimage_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : h.domChart.source ⊆ f ⁻¹' h.codChart.source

def Manifold.IsImmersionAtOfComplement.equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : (E × F) ≃L[𝕜] E''

A linear equivalence E × F ≃L[𝕜] E'' which belongs to the data of an immersion f at x: the particular equivalence is arbitrary, but this choice matches the witnesses given by h.domChart and h.codChart.

Equations

• h.equiv = Classical.choose ⋯

theorem Manifold.IsImmersionAtOfComplement.writtenInCharts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (⇑h.equiv ∘ fun (x : E) => (x, 0)) (h.domChart.extend I).target

theorem Manifold.IsImmersionAtOfComplement.property {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp F I J M N)

theorem Manifold.IsImmersionAtOfComplement.map_target_subset_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : (⇑h.equiv ∘ fun (x : E) => (x, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

If f is an immersion at x, it maps its domain chart's target (h.domChart.extend I).target to its codomain chart's target (h.domChart.extend J).target.

Roig and Domingues' [roigdomingues1992] definition of immersions only asks for this inclusion between the targets of the local charts: using mathlib's formalisation conventions, that condition is slightly weaker than source_subset_preimage_source: the latter implies that h.codChart.extend J ∘ f maps h.domChart.source to (h.codChart.extend J).target = (h.codChart.extend I) '' h.codChart.source, but that does not imply f maps h.domChart.source to h.codChartSource; a priori f could map some point f ∘ h.domChart.extend I x ∉ h.codChart.source into the target. Note that this difference only occurs because of our design using junk values; this is not a mathematically meaningful difference.`

At the same time, this condition is fairly weak: it is implied, for instance, by f being continuous at x (see mk_of_continuousAt), which is easy to ascertain in practice.

See target_subset_preimage_target for a version stated using preimages instead of images.

theorem Manifold.IsImmersionAtOfComplement.target_subset_preimage_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : (h.domChart.extend I).target ⊆ (⇑h.equiv ∘ fun (x : E) => (x, 0)) ⁻¹' (h.codChart.extend J).target

If f is an immersion at x, its domain chart's target (h.domChart.extend I).target is mapped to it codomain chart's target (h.domChart.extend J).target: see map_target_subset_target for a version stated using images.

theorem Manifold.IsImmersionAtOfComplement.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) (hfg : f =ᶠ[nhds x] g) : IsImmersionAtOfComplement F I J n g x

If f is an immersion at x and g = f on some neighbourhood of x, then g is an immersion at x.

theorem Manifold.IsImmersionAtOfComplement.congr_iff_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} (hfg : f =ᶠ[nhds x] g) : IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F I J n g x

If f = g on some neighbourhood of x, then f is an immersion at x if and only if g is an immersion at x.

theorem Manifold.IsImmersionAtOfComplement.small {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) : Small.{u, u_5} F

def Manifold.IsImmersionAtOfComplement.smallComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) : Type u

Given an immersion f at x, this is a choice of complement which lives in the same universe as the model space for the co-domain of f: this is useful to avoid universe restrictions.

Equations

• hf.smallComplement = Shrink.{?u.144, ?u.141} F

instance Manifold.IsImmersionAtOfComplement.instNormedAddCommGroupSmallComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement

Equations

• hf.instNormedAddCommGroupSmallComplement = id inferInstance

instance Manifold.IsImmersionAtOfComplement.instNormedSpaceSmallComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement

Equations

• hf.instNormedSpaceSmallComplement = id inferInstance

def Manifold.IsImmersionAtOfComplement.smallEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsImmersionAtOfComplement F I J n f x) : F ≃L[𝕜] hf.smallComplement

Given an immersion f at x w.r.t. a complement F, this construction provides a continuous linear equivalence from F to the small complement of F: mathematically, this is just the identity map; however, this is technically useful as it enables us to always work with hf.smallComplement.

Equations

• hf.smallEquiv = (Equiv.continuousLinearEquiv 𝕜 (equivShrink F).symm).symm

theorem Manifold.IsImmersionAtOfComplement.trans_F {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) (e : F ≃L[𝕜] F') : IsImmersionAtOfComplement F' I J n f x

theorem Manifold.IsImmersionAtOfComplement.congr_F {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (e : F ≃L[𝕜] F') : IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F' I J n f x

Being an immersion at x w.r.t. F is stable under replacing F by an isomorphic copy.

theorem Manifold.IsImmersionAtOfComplement.isImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAtOfComplement F I J n f x) : IsImmersionAt I J n f x

If f is an immersion at x w.r.t. some complement F, it is an immersion at x.

Note that the proof contains a small formalisation-related subtlety: F can live in any universe, while being an immersion at x requires the existence of a complement in the same universe as the model normed space of N. This is solved by smallComplement and smallEquiv.

theorem Manifold.IsImmersionAt.mk_of_charts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G) (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source) (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hsource : domChart.source ⊆ f ⁻¹' codChart.source) (hwrittenInExtend : Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun (x : E) => (x, 0)) (domChart.extend I).target) : IsImmersionAt I J n f x

theorem Manifold.IsImmersionAt.mk_of_continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G) (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source) (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hwrittenInExtend : Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun (x : E) => (x, 0)) (domChart.extend I).target) : IsImmersionAt I J n f x

f : M → N is a C^n immersion at x if there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0). This version does not assume that f maps φ.source to ψ.source, but that f is continuous at x.

def Manifold.IsImmersionAt.complement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : Type u

A choice of complement of the model normed space E of M in the model normed space E' of N

Equations

• h.complement = Classical.choose ⋯

noncomputable instance Manifold.IsImmersionAt.instNormedAddCommGroupComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement

Equations

• h.instNormedAddCommGroupComplement = Classical.choose ⋯

noncomputable instance Manifold.IsImmersionAt.instNormedSpaceComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement

Equations

• h.instNormedSpaceComplement = Classical.choose ⋯

theorem Manifold.IsImmersionAt.isImmersionAtOfComplement_complement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : IsImmersionAtOfComplement h.complement I J n f x

def Manifold.IsImmersionAt.domChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : OpenPartialHomeomorph M H

A choice of chart on the domain M of an immersion f at x: w.r.t. this chart and the data h.codChart and h.equiv, f will look like an inclusion u ↦ (u, 0) in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.codChart and h.codChart.

Equations

• h.domChart = ⋯.domChart

def Manifold.IsImmersionAt.codChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : OpenPartialHomeomorph N G

A choice of chart on the co-domain N of an immersion f at x: w.r.t. this chart and the data h.domChart and h.equiv, f will look like an inclusion u ↦ (u, 0) in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.equiv and h.domChart.

Equations

• h.codChart = ⋯.codChart

theorem Manifold.IsImmersionAt.mem_domChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : x ∈ h.domChart.source

theorem Manifold.IsImmersionAt.mem_codChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : f x ∈ h.codChart.source

theorem Manifold.IsImmersionAt.domChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : h.domChart ∈ IsManifold.maximalAtlas I n M

theorem Manifold.IsImmersionAt.codChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : h.codChart ∈ IsManifold.maximalAtlas J n N

theorem Manifold.IsImmersionAt.source_subset_preimage_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : h.domChart.source ⊆ f ⁻¹' h.codChart.source

def Manifold.IsImmersionAt.equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : (E × h.complement) ≃L[𝕜] E''

A linear equivalence E × F ≃L[𝕜] E'' which belongs to the data of an immersion f at x: the particular equivalence is arbitrary, but this choice matches the witnesses given by h.domChart and h.codChart.

Equations

• h.equiv = ⋯.equiv

theorem Manifold.IsImmersionAt.writtenInCharts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (⇑h.equiv ∘ fun (x_1 : E) => (x_1, 0)) (h.domChart.extend I).target

theorem Manifold.IsImmersionAt.property {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp h.complement I J M N)

theorem Manifold.IsImmersionAt.map_target_subset_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : (⇑h.equiv ∘ fun (x_1 : E) => (x_1, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

If f is an immersion at x, it maps its domain chart's target to its codomain chart's target: (h.domChart.extend I).target to (h.domChart.extend J).target.

Roig and Domingues' [roigdomingues1992] definition of immersions only asks for this inclusion between the targets of the local charts: using mathlib's formalisation conventions, that condition is slightly weaker than source_subset_preimage_source: the latter implies that h.codChart.extend J ∘ f maps h.domChart.source to (h.codChart.extend J).target = (h.codChart.extend I) '' h.codChart.source, but that does not imply f maps h.domChart.source to h.codChartSource; a priori f could map some point f ∘ h.domChart.extend I x ∉ h.codChart.source into the target. Note that this difference only occurs because of our design using junk values; this is not a mathematically meaningful difference.`

At the same time, this condition is fairly weak: it is implied, for instance, by f being continuous at x (see mk_of_continuousAt), which is easy to ascertain in practice.

See target_subset_preimage_target for a version stated using preimages instead of images.

theorem Manifold.IsImmersionAt.target_subset_preimage_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) : (h.domChart.extend I).target ⊆ (⇑h.equiv ∘ fun (x_1 : E) => (x_1, 0)) ⁻¹' (h.codChart.extend J).target

If f is an immersion at x, its domain chart's target (h.domChart.extend I).target is mapped to it codomain chart's target (h.domChart.extend J).target: see map_target_subset_target for a version stated using images.

theorem Manifold.IsImmersionAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} (hf : IsImmersionAt I J n f x) (hfg : f =ᶠ[nhds x] g) : IsImmersionAt I J n g x

If f is an immersion at x and g = f on some neighbourhood of x, then g is an immersion at x.

theorem Manifold.IsImmersionAt.congr_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} (hfg : f =ᶠ[nhds x] g) : IsImmersionAt I J n f x ↔ IsImmersionAt I J n g x

If f = g on some neighbourhood of x, then f is an immersion at x if and only if g is an immersion at x.

def Manifold.IsImmersionOfComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) : Prop

f : M → N is a C^n immersion if around each point x ∈ M, there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0).

In other words, f is an immersion at each x ∈ M.

This definition has a fixed parameter F, which is a choice of complement of E in E': being an immersion at x includes a choice of linear isomorphism between E × F and E'.

Equations

• Manifold.IsImmersionOfComplement F I J n f = ∀ (x : M), Manifold.IsImmersionAtOfComplement F I J n f x

def Manifold.IsImmersion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) : Prop

f : M → N is a C^n immersion if around each point x ∈ M, there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0).

Implicit in this definition is an abstract choice F of a complement of E in E': being an immersion includes a choice of linear isomorphism between E × F and E', which is where the choice of F enters. If you need stronger control over the complement F, use IsImmersionOfComplement instead.

Note that our global choice of complement is a bit stronger than asking f to be an immersion at each x ∈ M w.r.t. to potentially varying complements: see isImmersionAt for details.

Equations

• Manifold.IsImmersion I J n f = ∃ (F : Type ?u.30) (x : NormedAddCommGroup F) (x_1 : NormedSpace 𝕜 F), Manifold.IsImmersionOfComplement F I J n f

theorem Manifold.IsImmersionOfComplement.isImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersionOfComplement F I J n f) (x : M) : IsImmersionAtOfComplement F I J n f x

If f is an immersion, it is an immersion at each point.

theorem Manifold.IsImmersionOfComplement.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} (h : IsImmersionOfComplement F I J n f) (heq : f = g) : IsImmersionOfComplement F I J n g

If f = g and f is an immersion, so is g.

theorem Manifold.IsImmersionOfComplement.trans_F {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersionOfComplement F I J n f) (e : F ≃L[𝕜] F') : IsImmersionOfComplement F' I J n f

theorem Manifold.IsImmersionOfComplement.congr_F {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (e : F ≃L[𝕜] F') : IsImmersionOfComplement F I J n f ↔ IsImmersionOfComplement F' I J n f

Being an immersion w.r.t. F is stable under replacing F by an isomorphic copy.

theorem Manifold.IsImmersionOfComplement.isImmersion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersionOfComplement F I J n f) : IsImmersion I J n f

If f is an immersion w.r.t. some complement F, it is an immersion.

Note that the proof contains a small formalisation-related subtlety: F can live in any universe, while being an immersion requires the existence of a complement in the same universe as the model normed space of N. This is solved by smallComplement and smallEquiv.

def Manifold.IsImmersion.complement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersion I J n f) : Type u

A choice of complement of the model normed space E of M in the model normed space E' of N

Equations

• h.complement = Classical.choose h

noncomputable instance Manifold.IsImmersion.instNormedAddCommGroupComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersion I J n f) : NormedAddCommGroup h.complement

Equations

• h.instNormedAddCommGroupComplement = Classical.choose ⋯

noncomputable instance Manifold.IsImmersion.instNormedSpaceComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersion I J n f) : NormedSpace 𝕜 h.complement

Equations

• h.instNormedSpaceComplement = Classical.choose ⋯

theorem Manifold.IsImmersion.isImmersionOfComplement_complement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersion I J n f) : IsImmersionOfComplement h.complement I J n f

theorem Manifold.IsImmersion.isImmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsImmersion I J n f) (x : M) : IsImmersionAt I J n f x

If f is an immersion, it is an immersion at each point.

Note that the converse statement is false in general: if f is an immersion at each x, but with the choice of complement possibly depending on x, there need not be a global choice of complement for which f is an immersion at each point. The complement of f at x is isomorphic to the cokernel of mfderiv I J f x, but the mfderiv of f at (even nearby) points x and x' are not directly related. They have the same rank (the dimension of E, as will follow from injectivity), but if E'' is infinite-dimensional this is not conclusive. If E'' is infinite-dimensional, this dimension can indeed change between different connected of M.

theorem Manifold.IsImmersion.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} (h : IsImmersion I J n f) (heq : f = g) : IsImmersion I J n g

If f = g and f is an immersion, so is g.