Immersions

TheoremComposition of immersions at a point with fixed complements#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be charted spaces modelled through models with corners on normed spaces over \(\mathbb{K}\), where the models of \(N\) and \(N'\) are boundaryless. Let \(F_1\) and \(F_2\) be normed spaces over \(\mathbb{K}\). If \(f : M \to N\) is a \(C^n\) immersion at a point \(x \in M\) with complement \(F_1\) and \(g : N \to N'\) is a \(C^n\) immersion at \(f(x)\) with complement \(F_2\), then \(g \circ f\) is a \(C^n\) immersion at \(x\) with complement \(F_1 \times F_2\).

Here a map is a \(C^n\) immersion at a point with complement \(F\) when there are charts of the maximal \(C^n\) atlases around the point and its image, the first mapped by the map into the second, in which the map reads \(u \mapsto \varphi(u, 0)\) for a continuous linear isomorphism \(\varphi\) from the product of the source model space with \(F\) onto the target model space.

theorem _root_.Manifold.IsImmersionAtOfComplement.comp {F₁ F₂ : Type*}
    [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
    [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
    [J.Boundaryless] [J'.Boundaryless]
    {f : M → N} {g : N → N'} {x : M}
    (hg : IsImmersionAtOfComplement F₂ J J' n g (f x))
    (hf : IsImmersionAtOfComplement F₁ I J n f x) :
    IsImmersionAtOfComplement (F₁ × F₂) I J' n (g ∘ f) x

Used by 2

Used byComposition of immersions at a point over boundaryless models · Composition of immersions with fixed complements

TheoremComposition of immersions at a point over boundaryless models#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be charted spaces modelled through models with corners on normed spaces over \(\mathbb{K}\), where the models of \(N\) and \(N'\) are boundaryless. If \(f : M \to N\) is a \(C^n\) immersion at a point \(x \in M\) and \(g : N \to N'\) is a \(C^n\) immersion at \(f(x)\), then \(g \circ f\) is a \(C^n\) immersion at \(x\).

Here a map is a \(C^n\) immersion at a point when, for some normed space \(F\) over \(\mathbb{K}\), there are charts of the maximal \(C^n\) atlases around the point and its image, the first mapped by the map into the second, in which the map reads \(u \mapsto \varphi(u, 0)\) for a continuous linear isomorphism \(\varphi\) from the product of the source model space with \(F\) onto the target model space.

theorem _root_.Manifold.IsImmersionAt.comp [J.Boundaryless] [J'.Boundaryless]
    {f : M → N} {g : N → N'} {x : M}
    (hg : IsImmersionAt J J' n g (f x)) (hf : IsImmersionAt I J n f x) :
    IsImmersionAt I J' n (g ∘ f) x

Uses 1 · Used by 1

Proof usesComposition of immersions at a point with fixed complements

Used byComposition of immersions at a point

TheoremComposition of immersions with fixed complements#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be charted spaces modelled through models with corners on normed spaces over \(\mathbb{K}\), where the models of \(N\) and \(N'\) are boundaryless. Let \(F_1\) and \(F_2\) be normed spaces over \(\mathbb{K}\). If \(f : M \to N\) is a \(C^n\) immersion with complement \(F_1\) and \(g : N \to N'\) is a \(C^n\) immersion with complement \(F_2\), then \(g \circ f\) is a \(C^n\) immersion with complement \(F_1 \times F_2\).

Here a map is a \(C^n\) immersion with complement \(F\) when for every point there are charts of the maximal \(C^n\) atlases around the point and its image, the first mapped by the map into the second, in which the map reads \(u \mapsto \varphi(u, 0)\) for a continuous linear isomorphism \(\varphi\) from the product of the source model space with \(F\) onto the target model space.

theorem _root_.Manifold.IsImmersionOfComplement.comp {F₁ F₂ : Type*}
    [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
    [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
    [J.Boundaryless] [J'.Boundaryless]
    {f : M → N} {g : N → N'}
    (hg : IsImmersionOfComplement F₂ J J' n g)
    (hf : IsImmersionOfComplement F₁ I J n f) :
    IsImmersionOfComplement (F₁ × F₂) I J' n (g ∘ f)

Uses 1 · Used by 1

Proof usesComposition of immersions at a point with fixed complements

Used byComposition of immersions over boundaryless models

TheoremComposition of immersions over boundaryless models#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be charted spaces modelled through models with corners on normed spaces over \(\mathbb{K}\), where the models of \(N\) and \(N'\) are boundaryless. If \(f : M \to N\) and \(g : N \to N'\) are \(C^n\) immersions, then \(g \circ f\) is a \(C^n\) immersion.

Here a map is a \(C^n\) immersion when there is a normed space \(F\) over \(\mathbb{K}\) such that for every point there are charts of the maximal \(C^n\) atlases around the point and its image, the first mapped by the map into the second, in which the map reads \(u \mapsto \varphi(u, 0)\) for a continuous linear isomorphism \(\varphi\) from the product of the source model space with \(F\) onto the target model space.

theorem _root_.Manifold.IsImmersion.comp [J.Boundaryless] [J'.Boundaryless]
    {f : M → N} {g : N → N'}
    (hg : IsImmersion J J' n g) (hf : IsImmersion I J n f) :
    IsImmersion I J' n (g ∘ f)

Uses 1 · Used by 1

Proof usesComposition of immersions with fixed complements

Used byComposition of immersions

TheoremComposition of immersions at a point#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be \(C^n\) manifolds without boundary modeled on Banach spaces over \(\mathbb{K}\). If \(f : M \to N\) is a \(C^n\) immersion at a point \(x \in M\) and \(g : N \to N'\) is a \(C^n\) immersion at \(f(x)\), then \(g \circ f\) is a \(C^n\) immersion at \(x\).

Here a map is a \(C^n\) immersion at a point when, in suitable charts around the point and its image, it reads \(u \mapsto \varphi(u, 0)\) for a continuous linear isomorphism \(\varphi : E \times F \to E'\), where \(E\) and \(E'\) are the model spaces of the source and target and \(F\) is some normed space over \(\mathbb{K}\).

Proof: Restrict the first immersion's codomain chart to the second immersion's domain chart, then conjugate that chart transition through the second linear normal form. The normal forms compose with the product of their complements.

theorem immersionAt_comp
    [CompleteSpace E] [CompleteSpace E''] [CompleteSpace E''']
    [I.Boundaryless] [J.Boundaryless] [J'.Boundaryless]
    [IsManifold I n M] [IsManifold J n N] [IsManifold J' n N']
    {f : M → N} {g : N → N'} {x : M}
    (hf : IsImmersionAt I J n f x) (hg : IsImmersionAt J J' n g (f x)) :
    IsImmersionAt I J' n (g ∘ f) x

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.

Uses 1

Proof usesComposition of immersions at a point over boundaryless models

TheoremComposition of immersions#✓fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\), \(N\), \(N'\) be \(C^n\) manifolds without boundary modeled on Banach spaces over \(\mathbb{K}\). If \(f : M \to N\) and \(g : N \to N'\) are \(C^n\) immersions, then \(g \circ f\) is a \(C^n\) immersion.

Here a map is a \(C^n\) immersion when there is a normed space \(F\) over \(\mathbb{K}\) such that around every point, in suitable charts around the point and its image, the map reads \(u \mapsto \varphi(u, 0)\) for some continuous linear isomorphism \(\varphi : E \times F \to E'\), where \(E\) and \(E'\) are the model spaces of the source and target.

Proof: Apply the pointwise composition construction using the product of the two global complements, then package the resulting fixed-complement immersion.

theorem immersion_comp
    [CompleteSpace E] [CompleteSpace E''] [CompleteSpace E''']
    [I.Boundaryless] [J.Boundaryless] [J'.Boundaryless]
    [IsManifold I n M] [IsManifold J n N] [IsManifold J' n N']
    {f : M → N} {g : N → N'}
    (hf : IsImmersion I J n f) (hg : IsImmersion J J' n g) :
    IsImmersion I J' n (g ∘ f)

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.

Uses 1

Proof usesComposition of immersions over boundaryless models

TheoremInjective differential with complemented range gives an immersion#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(n \ge 1\) be a smoothness degree (possibly \(\infty\) or \(\omega\)), and let \(M\) and \(N\) be \(C^n\) manifolds without boundary over \(\mathbb{K}\), modelled on Banach spaces \(E\) and \(E'\). Let \(f \colon M \to N\) be \(C^n\) at every point of some neighbourhood of a point \(x \in M\), and suppose that its differential \(df_x \colon E \to E'\) is injective and that there is a continuous linear projection of \(E'\) onto the range of \(df_x\). Then \(f\) is a \(C^n\) immersion at \(x\).

Manifold.IsImmersionAt.of_injective_mfderiv_of_closedComplemented_range · 15 lines

theorem Manifold.IsImmersionAt.of_injective_mfderiv_of_closedComplemented_range
    {𝕜 E E' H G M N : Type*} [NontriviallyNormedField 𝕜]
    [CompleteSpace 𝕜] [IsRCLikeNormedField 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E']
    [TopologicalSpace H] [TopologicalSpace G]
    {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G}
    [I.Boundaryless] [J.Boundaryless]
    [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N]
    {n : ℕ∞ω} [IsManifold I n M] [IsManifold J n N]
    {f : M → N} {x : M} (hn : 1 ≤ n)
    (hfn : ∀ᶠ y in 𝓝 x, ContMDiffAt I J n f y)
    (hderiv : Function.Injective (mfderiv I J f x : E →L[𝕜] E'))
    (hcompl : (mfderiv I J f x : E →L[𝕜] E').range.ClosedComplemented) :
    IsImmersionAt I J n f x

Used by 1

Used byInjective differential gives an immersion

TheoremInjective differential gives an immersion#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(n \ge 1\) be a smoothness degree (possibly \(\infty\) or \(\omega\)), and let \(M\) and \(N\) be \(C^n\) manifolds without boundary over \(\mathbb{K}\), modelled on finite-dimensional normed \(\mathbb{K}\)-vector spaces. If a map \(f \colon M \to N\) is \(C^n\) at every point of some neighbourhood of a point \(x \in M\) and its differential \(df_x\) at \(x\) is injective, then \(f\) is a \(C^n\) immersion at \(x\).

Proof: Choose a complement to the differential's range, apply the inverse function theorem to the resulting product map in extended charts, and use its local inverse as a target chart.

theorem immersionAt_of_injective_mfderiv
    [CompleteSpace 𝕜] [IsRCLikeNormedField 𝕜]
    [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'']
    [I.Boundaryless] [J.Boundaryless]
    [IsManifold I n M] [IsManifold J n N]
    {f : M → N} {x : M}
    (hn : 1 ≤ n) (hfn : ∀ᶠ y in 𝓝 x, ContMDiffAt I J n f y)
    (hderiv : Function.Injective (mfderiv I J f x)) :
    IsImmersionAt I J n f x

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.

Uses 1

Proof usesInjective differential with complemented range gives an immersion

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.