Smooth submersions

In this file, we define C^n submersions between C^n manifolds. As in the case of immersions, the correct definition in the infinite-dimensional setting differs from the classical finite-dimensional one (which is usually phrased in terms of surjectivity of the mfderiv). Future work will prove that our definition implies the latter, and that both are equivalent for finite-dimensional manifolds.

Our definition is formulated in terms of local normal forms; i.e., a map f is a submersion at x if there exist charts near x and f x in which f looks like the standard projection (u, v) ↦ u. The results in this file follow from abstract results about such local properties.

Main definitions

• IsSubmersionAtOfComplement F I J n f x means a map f : M → N between C^n manifolds M and N is a submersion 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, v) ↦ u, w.r.t. some equivalence E ≃L[𝕜] (E'' × F). Differentiability of f is not assumed as it follows from this definition.
• IsSubmersionAt I J n f x means that f is a C^n submersion 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.
• IsSubmersionOfComplement F I J n f means f : M → N is a submersion at every point x : M, w.r.t. the chosen complement F.
• IsSubmersion I J n f means f : M → N is a submersion at every point x : M, w.r.t. some global choice of complement.

Main results

• IsSubmersionAt.congr_of_eventuallyEq: being a submersion is a local property. If f and g agree near x and f is a submersion at x, then so is g.
• IsSubmersionAtOfComplement.congr_F, IsSubmersionOfComplement.congr_F: being a submersion at x w.r.t. F is stable under replacing the complement F by an isomorphic copy.
• isOpen_isSubmersionAtOfComplement and isOpen_isSubmersionAt: the set of points where IsSubmersionAt(OfComplement) holds is open.
• IsSubmersionAt.prodMap and IsSubmersion.prodMap: the product of two submersions (at a point) is a submersion (at the product point).

Implementation notes

The implementation strategy is identical to the one for immersions. See the implementation notes in Mathlib/Geometry/Manifold/Immersion for details on:

• IsSubmersionAt(OfComplement),
• universe level issues for complements,
• small and smallEquiv constructions.

TODO

• The converse to IsSubmersionAtOfComplement.congr_F also holds: any two complements are isomorphic, as they are isomorphic to the kernel of the differential mfderiv I J f x.
• IsSubmersionAt.contMDiffAt: if f is a submersion at x, it is C^n at x.
• IsSubmersion.contMDiff: if f is a submersion, it is C^n.
• If f is a submersion at x, its differential mfderiv I J f x admits a continuous right inverse, in particular is surjective.
• If f : M → N is a map between Banach manifolds, mfderiv I J f x having a continuous right inverse implies f is a submersion at x. (This requires the inverse function theorem.)
• IsSubmersionAt.comp: if f : M → N and g: N → N' are maps between Banach manifolds such that f is a submersion at x : M and g is a submersion at f x, then g ∘ f is a submersion at x.
• IsSubmersion.comp: the composition of submersions is a submersion
• If f : M → N is a map between finite-dimensional manifolds, mfderiv I J f x being surjective implies f is a submersion at x.
• IsLocalDiffeomorphAt.isSubmersionAt and IsLocalDiffeomorph.isSubmersion: a local diffeomorphism (at x) is a submersion (at x)
• Diffeomorph.isSubmersion: in particular, a diffeomorphism is a submersion

References

• [Alexander Schmeding, An introduction to infinite-dimensional differential geometry] [Sch23]
• Note that Margelef-Roig and Dominguez have a slightly different definition of submersions.

Please do not work on this file without prior discussion with Michael Rothgang. This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.

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

The local property of being a submersion at a point: f : M → N is a submersion 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 projection (u, v) ↦ u. This definition has a fixed parameter F, which is a choice of complement of E'' in the model normed space E of M: being a submersion 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_submmersionAtProp {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [TopologicalSpace N] : IsLocalSourceTargetProperty (SubmersionAtProp F I J M N)

Being a submersion at x is a local property.

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

f : M → N is a C^n submersion 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, v) ↦ u. 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, choosing 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 IsSubmersionAt instead.

Equations

• Manifold.IsSubmersionAtOfComplement F I J n f x = Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.SubmersionAtProp F I J M N)

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

f : M → N is a C^n submersion 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, v) ↦ u. 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 a submersion at x includes a choice of linear isomorphism between E and E'' × F, which is where the choice of F enters. If you need stronger control over the complement F, use IsSubmersionAtOfComplement instead.

Equations

• Manifold.IsSubmersionAt I J n f x = ∃ (F : Type ?u.7) (x_1 : NormedAddCommGroup F) (x_2 : NormedSpace 𝕜 F), Manifold.IsSubmersionAtOfComplement F I J n f x

theorem Manifold.IsSubmersionAtOfComplement.mk_of_charts {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (equiv : E ≃L[𝕜] E'' × F) (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) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x

theorem Manifold.IsSubmersionAtOfComplement.mk_of_continuousAt {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : E ≃L[𝕜] E'' × F) (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) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x

f : M → N is a C^n submersion 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,v) ↦ u. This version does not assume that f maps φ.source to ψ.source, but that f is continuous at x.

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

A choice of chart on the domain M of a submersion f at x: w.r.t. this chart and the data h.codChart and h.equiv, f will look like a projection (u,v) ↦ u 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 = Manifold.LiftSourceTargetPropertyAt.domChart h

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

A choice of chart on the codomain N of a submersion f at x: w.r.t. this chart and the data h.domChart and h.equiv, f will look like a projection (u, v) ↦ u 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 = Manifold.LiftSourceTargetPropertyAt.codChart h

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

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

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

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

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

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

A linear equivalence E ≃L[𝕜] E'' × F which belongs to the data of a submersion 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.IsSubmersionAtOfComplement.writtenInCharts {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) : Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (Prod.fst ∘ ⇑h.equiv) (h.domChart.extend I).target

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

theorem Manifold.IsSubmersionAtOfComplement.image_target_subset_target {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) : Prod.fst ∘ ⇑h.equiv '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

If f is a submersion 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.

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

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

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

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

If f is a submersion at x and g = f on some neighbourhood of x, then g is a submersion at x.

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

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

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

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

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

Equations

• hf.smallComplement = Shrink.{?u.8, ?u.5} F

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Given a submersion 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.IsSubmersionAtOfComplement.trans_F {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAtOfComplement F I J n f x) (e : F ≃L[𝕜] F') : IsSubmersionAtOfComplement F' I J n f x

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

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

theorem isOpen_isSubmersionAtOfComplement {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} : IsOpen {x : M | Manifold.IsSubmersionAtOfComplement F I J n f x}

theorem Manifold.IsSubmersionAtOfComplement.prodMap {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup E'''] [NormedSpace 𝕜 E'''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {g : M' → N'} {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] (hf : IsSubmersionAtOfComplement F I J n f x) (hg : IsSubmersionAtOfComplement F' I' J' n g x') : IsSubmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x')

If f: M → N and g: M' × N' are submersions at x and x', respectively, then f × g: M × N → M' × N' is a submersion at (x, x').

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

If f is a submersion at x w.r.t. some complement F, it is a submersion at x.

Note that the proof contains a small formalisation-related subtlety: F can live in any universe, while being a submersion 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.IsSubmersionAt.mk_of_charts {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (equiv : E ≃L[𝕜] E'' × F) (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) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target) : IsSubmersionAt I J n f x

theorem Manifold.IsSubmersionAt.mk_of_continuousAt {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : E ≃L[𝕜] E'' × F) (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) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target) : IsSubmersionAt I J n f x

f : M → N is a C^n submersion 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, v) ↦ u. This version does not assume that f maps φ.source to ψ.source, but that f is continuous at x.

def Manifold.IsSubmersionAt.complement {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt 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 h

@[implicit_reducible]

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

Equations

• h.instNormedAddCommGroupComplement = Classical.choose ⋯

@[implicit_reducible]

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

Equations

• h.instNormedSpaceComplement = Classical.choose ⋯

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

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

A choice of chart on the domain M of a submersion f at x: w.r.t. this chart and the data h.codChart and h.equiv, f will look like a projection (u, v) ↦ u 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

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

A choice of chart on the co-domain N of a submersion f at x: w.r.t. this chart and the data h.domChart and h.equiv, f will look like a projection (u, v) ↦ u 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.IsSubmersionAt.mem_domChart_source {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt I J n f x) : x ∈ h.domChart.source

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

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

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

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

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

A linear equivalence E ≃L[𝕜] (E'' × F) which belongs to the data of a submersion 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.IsSubmersionAt.writtenInCharts {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt I J n f x) : Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (Prod.fst ∘ ⇑h.equiv) (h.domChart.extend I).target

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

theorem Manifold.IsSubmersionAt.image_target_subset_target {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsSubmersionAt I J n f x) : Prod.fst ∘ ⇑h.equiv '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

If f is a submersion 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.

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

If f is a submersion 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 image_target_subset_target for a version stated using images.

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

If f is a submersion at x and g = f on some neighbourhood of x, then g is a submersion at x.

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

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

theorem isOpen_isSubmersionAt {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} : IsOpen {x : M | Manifold.IsSubmersionAt I J n f x}

theorem Manifold.IsSubmersionAt.prodMap {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {H : Type u_7} {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup E'''] [NormedSpace 𝕜 E'''] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {g : M' → N'} {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] (hf : IsSubmersionAt I J n f x) (hg : IsSubmersionAt I' J' n g x') : IsSubmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x')

If f: M → N and g: M' × N' are submersions at x and x', respectively, then f × g: M × N → M' × N' is a submersion at (x, x').

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

f : M → N is a C^n submersion 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, v) ↦ u.

In other words, f is a submersion at each x ∈ M.

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

Equations

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

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

f : M → N is a C^n submersion 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, v) ↦ u.

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

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

Equations

• Manifold.IsSubmersion I J n f = ∃ (F : Type ?u.7) (x : NormedAddCommGroup F) (x_1 : NormedSpace 𝕜 F), Manifold.IsSubmersionOfComplement F I J n f

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

If f is a submersion, it is a submersion at each point.

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

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

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

theorem Manifold.IsSubmersionOfComplement.prodMap {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup E'''] [NormedSpace 𝕜 E'''] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] (h : IsSubmersionOfComplement F I J n f) (h' : IsSubmersionOfComplement F' I' J' n g) : IsSubmersionOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g)

If f: M → N and g: M' × N' are submersions at x and x' (w.r.t. F and F'), respectively, then f × g: M × N → M' × N' is a submersion at (x, x') w.r.t. F × F'.

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

If f is a submersion w.r.t. some complement F, it is a submersion.

Note that the proof contains a small formalisation-related subtlety: F can live in any universe, while being a submersion 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.IsSubmersionOfComplement.id {𝕜 : Type u_1} {H : Type u_7} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] : IsSubmersionOfComplement PUnit.{u_15 + 1} I I n id

The identity map is a submersion with complement PUnit.

def Manifold.IsSubmersion.complement {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (h : IsSubmersion 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

@[implicit_reducible]

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

Equations

• h.instNormedAddCommGroupComplement = Classical.choose ⋯

@[implicit_reducible]

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

Equations

• h.instNormedSpaceComplement = Classical.choose ⋯

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

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

If f is a submersion, it is a submersion at each point.

theorem Manifold.IsSubmersion.prodMap {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {H : Type u_7} {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup E'''] [NormedSpace 𝕜 E'''] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] (hf : IsSubmersion I J n f) (hg : IsSubmersion I' J' n g) : IsSubmersion (I.prod I') (J.prod J') n (Prod.map f g)

If f: M → N and g: M' × N' are submersions at x and x', respectively, then f × g: M × N → M' × N' is a submersion at (x, x').

theorem Manifold.IsSubmersion.id {𝕜 : Type u_1} {H : Type u_7} {E : Type u} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] : IsSubmersion I I n id

The identity map is an submersion.