Submersions: pointwise characterization, derivative and local sections

A map is a submersion with a fixed complement F exactly when it is a submersion with complement F at every point (Manifold.isSubmersionOfComplement_iff). Mathlib states only the forward direction, Manifold.IsSubmersionOfComplement.isSubmersionAt, and does not expose the definition, so the converse is needed to build global submersions from pointwise local normal forms, for instance with Manifold.IsSubmersionAtOfComplement.mk_of_continuousAt. The first projection of a product of manifolds is a submersion, with the second model space as complement (Manifold.isSubmersionOfComplement_fst).

This file also differentiates the normal form of a C^n submersion f : M → N, n ≠ 0: around every point x there are charts φ of M and ψ of N and a continuous linear equivalence L : E ≃L[𝕜] E'' × F in which f reads as u ↦ (L u).1. On the whole source of φ, the derivative of f read through the derivative of ψ is (L (dφ v)).1 (Manifold.IsSubmersionAtOfComplement.mfderiv_extend_comp_mfderiv), so mfderiv f y is surjective, it has a continuous right inverse since the projection u ↦ (L u).1 has one (Manifold.IsSubmersionAt.hasRightInverse_mfderiv; Mathlib lists this as a TODO), and its kernel is the preimage under dφ of the fixed subspace L⁻¹ (0 × F) of the model space.

When the model of the source has no boundary, a submersion at x has a C^n local section through x over an open neighbourhood of f x, read off from the normal-form charts (Manifold.IsSubmersionAt.exists_contMDiffOn_section).

Main results

• Manifold.isSubmersionOfComplement_iff: a submersion with complement F is one at every point.
• Manifold.IsSubmersionAtOfComplement.mfderiv_extend_comp_mfderiv: the derivative of a submersion in its normal-form charts.
• Manifold.IsSubmersionAtOfComplement.surjective_mfderiv, Manifold.IsSubmersionAt.surjective_mfderiv and Manifold.IsSubmersion.surjective_mfderiv: the derivative of a submersion is surjective. Mathlib lists this as a TODO.
• Manifold.IsSubmersionAtOfComplement.hasRightInverse_mfderiv, Manifold.IsSubmersionAt.hasRightInverse_mfderiv and Manifold.IsSubmersion.hasRightInverse_mfderiv: the derivative of a submersion has a continuous right inverse.
• Manifold.IsSubmersionAtOfComplement.mfderiv_eq_zero_iff: the kernel of the derivative on the source of the normal-form chart.
• Manifold.IsSubmersionAtOfComplement.exists_contMDiffOn_section, Manifold.IsSubmersionAt.exists_contMDiffOn_section: local sections of a submersion.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Theorem 4.12 (local form of a submersion) and Theorem 4.26 (local sections of submersions).

theorem Manifold.isSubmersionOfComplement_iff {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {f : M → N} : IsSubmersionOfComplement F I J n f ↔ ∀ (x : M), IsSubmersionAtOfComplement F I J n f x

A map is a submersion with complement F exactly when it is a submersion with complement F at every point.

theorem Manifold.isSubmersionOfComplement_fst {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] : IsSubmersionOfComplement E' (I.prod J) I n Prod.fst

The first projection of a product of manifolds is a submersion, with the second model space as complement. No nonemptiness assumption on either factor is needed.

theorem Manifold.isSubmersion_fst {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] : IsSubmersion (I.prod J) I n Prod.fst

The first projection of a product of manifolds is a submersion.

noncomputable def Manifold.IsSubmersionAtOfComplement.projection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) : E →L[𝕜] E''

The linear projection u ↦ (L u).1 that a submersion reads as in its normal-form charts, where L is the linear equivalence h.equiv : E ≃L[𝕜] E'' × F.

@[simp]

theorem Manifold.IsSubmersionAtOfComplement.projection_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (u : E) : h.projection u = (h.equiv u).1

The normal-form projection of a submersion is the first component of h.equiv.

theorem Manifold.IsSubmersionAtOfComplement.codChart_extend_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) {y : M} (hy : y ∈ h.domChart.source) : ↑(h.codChart.extend J) (f y) = h.projection (↑(h.domChart.extend I) y)

On the source of its domain chart φ, a submersion reads as y ↦ (L (φ y)).1 through its codomain chart ψ, where φ and ψ are taken extended.

theorem Manifold.IsSubmersionAtOfComplement.mfderiv_extend_comp_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) {y : M} (hy : y ∈ h.domChart.source) : mfderiv% ↑(h.codChart.extend J) (f y) ∘SL mfderiv% f y = h.projection ∘SL mfderiv% ↑(h.domChart.extend I) y

The derivative of a submersion in its normal-form charts. On the source of the domain chart φ, the derivative of f followed by the derivative of the codomain chart ψ is the derivative of φ followed by the projection u ↦ (L u).1.

theorem Manifold.IsSubmersionAtOfComplement.surjective_mfderiv_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) {y : M} (hy : y ∈ h.domChart.source) : Function.Surjective ⇑(mfderiv% f y)

The derivative of a submersion at any point of the source of its domain chart is surjective.

theorem Manifold.IsSubmersionAtOfComplement.surjective_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) : Function.Surjective ⇑(mfderiv% f x)

The derivative of a submersion is surjective.

theorem Manifold.IsSubmersionAtOfComplement.hasRightInverse_mfderiv_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) {y : M} (hy : y ∈ h.domChart.source) : (mfderiv% f y).HasRightInverse

At any point of the source of the domain chart φ, the derivative of a submersion has a continuous right inverse: read through the invertible derivatives of the charts it is the projection u ↦ (L u).1, which has one.

theorem Manifold.IsSubmersionAtOfComplement.hasRightInverse_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) : (mfderiv% f x).HasRightInverse

The derivative of a submersion has a continuous right inverse.

theorem Manifold.IsSubmersionAtOfComplement.mfderiv_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (hn : n ≠ 0) {y : M} (hy : y ∈ h.domChart.source) (v : TangentSpace I y) : (mfderiv% f y) v = 0 ↔ (h.equiv ((mfderiv% ↑(h.domChart.extend I) y) v)).1 = 0

On the source of the domain chart φ of a submersion, a tangent vector v lies in the kernel of the derivative of f exactly when its image dφ v in the model space lies in L⁻¹ (0 × F).

theorem Manifold.IsSubmersionAt.surjective_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt I J n f x) (hn : n ≠ 0) : Function.Surjective ⇑(mfderiv% f x)

The derivative of a submersion is surjective.

theorem Manifold.IsSubmersion.surjective_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsSubmersion I J n f) (hn : n ≠ 0) (x : M) : Function.Surjective ⇑(mfderiv% f x)

The derivative of a submersion is surjective at every point.

theorem Manifold.IsSubmersionAt.hasRightInverse_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt I J n f x) (hn : n ≠ 0) : (mfderiv% f x).HasRightInverse

The derivative of a submersion has a continuous right inverse.

theorem Manifold.IsSubmersion.hasRightInverse_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsSubmersion I J n f) (hn : n ≠ 0) (x : M) : (mfderiv% f x).HasRightInverse

The derivative of a submersion has a continuous right inverse at every point.

theorem Manifold.IsSubmersionAtOfComplement.exists_contMDiffOn_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} [I.Boundaryless] (h : IsSubmersionAtOfComplement F I J n f x) : ∃ (U : Set N), IsOpen U ∧ f x ∈ U ∧ ∃ (s : N → M), s (f x) = x ∧ ContMDiffOn J I n s U ∧ ∀ y ∈ U, f (s y) = y

Local sections of a submersion. If f is a C^n submersion at x and the model of M has no boundary, then over an open neighbourhood U of f x there is a C^n section of f through x: a map s with s (f x) = x, f (s y) = y for y ∈ U, and C^n on U. In the normal-form charts φ and ψ it is y ↦ φ⁻¹ (L⁻¹ (ψ y, c)), where c is the second component of L (φ x).

theorem Manifold.IsSubmersionAt.exists_contMDiffOn_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E'' : Type u_2} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} [I.Boundaryless] (h : IsSubmersionAt I J n f x) : ∃ (U : Set N), IsOpen U ∧ f x ∈ U ∧ ∃ (s : N → M), s (f x) = x ∧ ContMDiffOn J I n s U ∧ ∀ y ∈ U, f (s y) = y

Local sections of a submersion. If f is a C^n submersion at x and the model of M has no boundary, then over an open neighbourhood U of f x there is a C^n section s of f with s (f x) = x.