Submersions

TheoremChanging the target chart of a submersion at a point#βœ“fully proved

Let \(\mathbb{K}\) be a nontrivially normed field, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(M\) and \(N\) be charted spaces modelled, through models with corners, on normed spaces \(E\) and \(E''\) over \(\mathbb{K}\), both models without boundary. Let \(f : M \to N\) be a \(C^n\) submersion at \(x \in M\) with complement \(F\), and let \(e : E \to E'' \times F\) be the continuous linear equivalence chosen for it. Then for every chart \(\psi\) of \(N\) in the \(C^n\) maximal atlas with \(f(x)\) in its domain there is a chart \(\varphi\) of \(M\) in the \(C^n\) maximal atlas with \(x\) in its domain, such that \(f\) maps the domain of \(\varphi\) into the domain of \(\psi\) and \(\hat\psi \circ f \circ \hat\varphi^{-1} = \mathrm{pr}_1 \circ e\) on the image of \(\hat\varphi\), where \(\hat\varphi\) and \(\hat\psi\) denote the charts followed by the models with corners.

Here \(f\) is a \(C^n\) submersion at \(x\) with complement \(F\) (a normed space over \(\mathbb{K}\)) when there are charts of \(M\) around \(x\) and of \(N\) around \(f(x)\) in the \(C^n\) maximal atlases, the first mapped by \(f\) into the second, in which \(f\) reads \(\mathrm{pr}_1 \circ e\) on the image of the first, for some continuous linear equivalence \(e : E \to E'' \times F\); a witness of this fixes one such \(e\).

theorem _root_.Manifold.IsSubmersionAtOfComplement.exists_domChart_of_codChart
    [I.Boundaryless] [J.Boundaryless]
    {F : Type u} [NormedAddCommGroup F] [NormedSpace π•œ F]
    {f : M β†’ N} {x : M} (hf : IsSubmersionAtOfComplement F I J n f x)
    (codChart : OpenPartialHomeomorph N G) (hfx : f x ∈ codChart.source)
    (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) :
    βˆƒ domChart : OpenPartialHomeomorph M H,
      x ∈ domChart.source ∧
      domChart ∈ IsManifold.maximalAtlas I n M ∧
      domChart.source βŠ† f ⁻¹' codChart.source ∧
      Set.EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm)
        (Prod.fst ∘ hf.equiv) (domChart.extend I).target
Used by 1
Used byComposition of submersions at a point with chosen complements

TheoremComposition of submersions at a point with chosen 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 \(E\), \(E''\), \(E'''\) over \(\mathbb{K}\), where the models of \(M\) and \(N\) have no boundary. Let \(F_1\) and \(F_2\) be normed spaces over \(\mathbb{K}\). If \(f : M \to N\) is a \(C^n\) submersion at \(x \in M\) with complement \(F_1\) and \(g : N \to N'\) is a \(C^n\) submersion at \(f(x)\) with complement \(F_2\), then \(g \circ f\) is a \(C^n\) submersion at \(x\) with complement \(F_2 \times F_1\).

Here \(f\) is a \(C^n\) submersion at \(x\) with complement \(F\) when there are charts \(\varphi\) of \(M\) around \(x\) and \(\psi\) of \(N\) around \(f(x)\) in the \(C^n\) maximal atlases, with \(f\) mapping the domain of \(\varphi\) into the domain of \(\psi\), and a continuous linear equivalence \(e : E \to E'' \times F\) such that \(\hat\psi \circ f \circ \hat\varphi^{-1} = \mathrm{pr}_1 \circ e\) on the image of \(\hat\varphi\), where \(\hat\varphi\) and \(\hat\psi\) denote the charts followed by the models with corners.

theorem _root_.Manifold.IsSubmersionAtOfComplement.comp
    [I.Boundaryless] [J.Boundaryless]
    {F₁ Fβ‚‚ : Type u}
    [NormedAddCommGroup F₁] [NormedSpace π•œ F₁]
    [NormedAddCommGroup Fβ‚‚] [NormedSpace π•œ Fβ‚‚]
    {f : M β†’ N} {g : N β†’ N'} {x : M}
    (hg : IsSubmersionAtOfComplement Fβ‚‚ J J' n g (f x))
    (hf : IsSubmersionAtOfComplement F₁ I J n f x) :
    IsSubmersionAtOfComplement (Fβ‚‚ Γ— F₁) I J' n (g ∘ f) x
Uses 1 Β· Used by 2
Proof usesChanging the target chart of a submersion at a point
Used bySubmersions at a point are closed under composition Β· Composition of submersions with chosen complements

TheoremSubmersions at a point are closed under composition#βœ“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 \(E\), \(E''\), \(E'''\) over \(\mathbb{K}\), where the models of \(M\) and \(N\) have no boundary. If \(f : M \to N\) is a \(C^n\) submersion at \(x \in M\) and \(g : N \to N'\) is a \(C^n\) submersion at \(f(x)\), then \(g \circ f\) is a \(C^n\) submersion at \(x\).

Here \(f\) is a \(C^n\) submersion at \(x\) when, for some normed space \(F\) over \(\mathbb{K}\), there are charts \(\varphi\) of \(M\) around \(x\) and \(\psi\) of \(N\) around \(f(x)\) in the \(C^n\) maximal atlases, with \(f\) mapping the domain of \(\varphi\) into the domain of \(\psi\), and a continuous linear equivalence \(e : E \to E'' \times F\) such that \(\hat\psi \circ f \circ \hat\varphi^{-1} = \mathrm{pr}_1 \circ e\) on the image of \(\hat\varphi\), where \(\hat\varphi\) and \(\hat\psi\) denote the charts followed by the models with corners.

theorem _root_.Manifold.IsSubmersionAt.comp
    [I.Boundaryless] [J.Boundaryless]
    {f : M β†’ N} {g : N β†’ N'} {x : M}
    (hg : IsSubmersionAt J J' n g (f x)) (hf : IsSubmersionAt I J n f x) :
    IsSubmersionAt I J' n (g ∘ f) x
Uses 1 Β· Used by 1
Proof usesComposition of submersions at a point with chosen complements
Used byComposition of submersions at a point

TheoremComposition of submersions with chosen 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 \(E\), \(E''\), \(E'''\) over \(\mathbb{K}\), where the models of \(M\) and \(N\) have no boundary. Let \(F_1\) and \(F_2\) be normed spaces over \(\mathbb{K}\). If \(f : M \to N\) is a \(C^n\) submersion with complement \(F_1\) and \(g : N \to N'\) is a \(C^n\) submersion with complement \(F_2\), then \(g \circ f\) is a \(C^n\) submersion with complement \(F_2 \times F_1\).

Here \(f\) is a \(C^n\) submersion with complement \(F\) when at every \(x \in M\) there are charts \(\varphi\) of \(M\) around \(x\) and \(\psi\) of \(N\) around \(f(x)\) in the \(C^n\) maximal atlases, with \(f\) mapping the domain of \(\varphi\) into the domain of \(\psi\), and a continuous linear equivalence \(e : E \to E'' \times F\) such that \(\hat\psi \circ f \circ \hat\varphi^{-1} = \mathrm{pr}_1 \circ e\) on the image of \(\hat\varphi\), where \(\hat\varphi\) and \(\hat\psi\) denote the charts followed by the models with corners.

theorem _root_.Manifold.IsSubmersionOfComplement.comp
    [I.Boundaryless] [J.Boundaryless]
    {F₁ Fβ‚‚ : Type u}
    [NormedAddCommGroup F₁] [NormedSpace π•œ F₁]
    [NormedAddCommGroup Fβ‚‚] [NormedSpace π•œ Fβ‚‚]
    {f : M β†’ N} {g : N β†’ N'}
    (hg : IsSubmersionOfComplement Fβ‚‚ J J' n g)
    (hf : IsSubmersionOfComplement F₁ I J n f) :
    IsSubmersionOfComplement (Fβ‚‚ Γ— F₁) I J' n (g ∘ f)
Uses 1 Β· Used by 1
Proof usesComposition of submersions at a point with chosen complements
Used bySubmersions are closed under composition

TheoremSubmersions are closed under composition#βœ“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 \(E\), \(E''\), \(E'''\) over \(\mathbb{K}\), where the models of \(M\) and \(N\) have no boundary. If \(f : M \to N\) and \(g : N \to N'\) are \(C^n\) submersions, then so is \(g \circ f\).

Here \(f\) is a \(C^n\) submersion when there is one normed space \(F\) over \(\mathbb{K}\) such that at every \(x \in M\) there are charts \(\varphi\) of \(M\) around \(x\) and \(\psi\) of \(N\) around \(f(x)\) in the \(C^n\) maximal atlases, with \(f\) mapping the domain of \(\varphi\) into the domain of \(\psi\), and a continuous linear equivalence \(e : E \to E'' \times F\) such that \(\hat\psi \circ f \circ \hat\varphi^{-1} = \mathrm{pr}_1 \circ e\) on the image of \(\hat\varphi\), where \(\hat\varphi\) and \(\hat\psi\) denote the charts followed by the models with corners.

theorem _root_.Manifold.IsSubmersion.comp
    [I.Boundaryless] [J.Boundaryless]
    {f : M β†’ N} {g : N β†’ N'}
    (hg : IsSubmersion J J' n g) (hf : IsSubmersion I J n f) :
    IsSubmersion I J' n (g ∘ f)
Uses 1 Β· Used by 1
Proof usesComposition of submersions with chosen complements
Used byComposition of submersions

TheoremComposition of submersions 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 over \(\mathbb{K}\) modelled on Banach spaces. If \(f : M \to N\) is a \(C^n\) submersion at \(x \in M\) and \(g : N \to N'\) is a \(C^n\) submersion at \(f(x)\), then \(g \circ f\) is a \(C^n\) submersion at \(x\). Here \(f\) is a \(C^n\) submersion at \(x\) when there are charts of the \(C^n\) maximal atlases around \(x\) and \(f(x)\), the first mapped by \(f\) into the second, in which \(f\) reads \((u, v) \mapsto u\) after a continuous linear identification of the model space of \(M\) with the product of the model space of \(N\) and some normed space.

Proof: Replace the first submersion's target chart by the second submersion's source chart, then compose the two projection normal forms and use the product of their complements.

theorem submersionAt_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 : IsSubmersionAt I J n f x) (hg : IsSubmersionAt J J' n g (f x)) :
    IsSubmersionAt I J' n (g ∘ f) x
Sources
  • J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.
Uses 1
Proof usesSubmersions at a point are closed under composition

TheoremComposition of submersions#βœ“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 over \(\mathbb{K}\) modelled on Banach spaces. If \(f : M \to N\) and \(g : N \to N'\) are \(C^n\) submersions, then so is \(g \circ f\). Here \(f\) is a \(C^n\) submersion when there is one normed space \(F\) such that at every \(x \in M\) there are charts of the \(C^n\) maximal atlases around \(x\) and \(f(x)\), the first mapped by \(f\) into the second, in which \(f\) reads \((u, v) \mapsto u\) after a continuous linear identification of the model space of \(M\) with the product of the model space of \(N\) and \(F\).

Proof: Apply the complement-level pointwise composition theorem using the two fixed global complements, then package their product as the complement of the composite.

theorem submersion_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 : IsSubmersion I J n f) (hg : IsSubmersion J J' n g) :
    IsSubmersion I J' n (g ∘ f)
Sources
  • J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.
Uses 1
Proof usesSubmersions are closed under composition

TheoremSurjective differential into a finite-dimensional manifold gives a submersion#βœ“fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(n \in \mathbb{N} \cup \{\infty, \omega\}\) with \(n \ge 1\), let \(M\) be a \(C^n\) manifold without boundary over \(\mathbb{K}\) modelled on a Banach space, and let \(N\) be a \(C^n\) manifold, possibly with boundary or corners, over \(\mathbb{K}\) modelled on a finite-dimensional space. If \(f : M \to N\) is \(C^n\) at every point of some neighbourhood of \(x \in M\) and the manifold derivative of \(f\) at \(x\) is surjective, then \(f\) is a \(C^n\) submersion at \(x\): there are charts of the \(C^n\) maximal atlases around \(x\) and \(f(x)\), the first mapped by \(f\) into the second, in which \(f\) reads \((u, v) \mapsto u\) after a continuous linear identification of the model space of \(M\) with the product of the model space of \(N\) and some normed space.

theorem of_surjective_mfderiv
    {π•œ : Type*} [NontriviallyNormedField π•œ] [IsRCLikeNormedField π•œ]
    {E : Type u} {E'' H G M N : Type*}
    [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E]
    [NormedAddCommGroup E''] [NormedSpace π•œ E''] [FiniteDimensional π•œ E'']
    [TopologicalSpace H] [TopologicalSpace G]
    {I : ModelWithCorners π•œ E H} {J : ModelWithCorners π•œ E'' G}
    [TopologicalSpace M] [ChartedSpace H M]
    [TopologicalSpace N] [ChartedSpace G N]
    {n : β„•βˆžΟ‰} [I.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.Surjective (mfderiv I J f x)) :
    IsSubmersionAt I J n f x
Used by 1
Used bySurjective differential gives a submersion between finite-dimensional manifolds

TheoremSurjective differential gives a submersion between finite-dimensional manifolds#βœ“fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(n \in \mathbb{N} \cup \{\infty, \omega\}\) with \(n \ge 1\), and let \(M\) and \(N\) be \(C^n\) manifolds without boundary over \(\mathbb{K}\) modelled on finite-dimensional spaces. If \(f : M \to N\) is \(C^n\) at every point of some neighbourhood of \(x \in M\) and the manifold derivative of \(f\) at \(x\) is surjective, then \(f\) is a \(C^n\) submersion at \(x\): there are charts of the \(C^n\) maximal atlases around \(x\) and \(f(x)\), the first mapped by \(f\) into the second, in which \(f\) reads \((u, v) \mapsto u\) after a linear identification of the model space of \(M\) with the product of the model space of \(N\) and some normed space.

Proof: Split the surjective derivative, augment the map by its kernel coordinate, and apply the inverse function theorem to obtain charts in which the map is the first projection.

theorem submersionAt_of_surjective_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.Surjective (mfderiv I J f x)) :
    IsSubmersionAt I J n f x
Sources
  • J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4.
Uses 1
Proof usesSurjective differential into a finite-dimensional manifold gives a submersion
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.