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).
• IsSubmersionAt.contMDiffAt: if f is a submersion at x, it is C^n at x.
• IsSubmersion.contMDiff: if f is a submersion, it is automatically C^n in the sense of ContMDiff.

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.
• 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] [schmeding2023]
• Note that Margelef-Roig and Dominguez have a slightly different definition of submersions.

Please talk to Michael Rothgang before working on this file, to avoid duplicate work. The above TODOs are the topic of Samantha Naranjo's master's thesis; it's nicer 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 submersion 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

theorem Manifold.IsSubmersionAtOfComplement.mapsto_domChart_source_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) : Set.MapsTo f h.domChart.source 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 × M' → N × 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.IsSubmersionAtOfComplement.contMDiffOn {𝕜 : 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) : ContMDiffOn I J n f h.domChart.source

If f is a C^n submersion at x, then f is C^n on its domain chart's source, in particular on an open neighbourhood of x.

Prefer using IsSubmersionAtOfComplement.contMDiffAt instead.

theorem Manifold.IsSubmersionAtOfComplement.contMDiffAt {𝕜 : 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) : ContMDiffAt I J n f x

A C^n submersion at x is C^n at x.

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 × M' → N × N' is a submersion at (x, x').

theorem Manifold.IsSubmersionAt.contMDiffOn {𝕜 : 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) : ContMDiffOn I J n f h.domChart.source

If f is a submersion at x, then f is C^n on its domain chart's source, in particular on an open neighbourhood of x.`

Prefer using IsSubmersionAt.contMDiffAt instead

theorem Manifold.IsSubmersionAt.contMDiffAt {𝕜 : 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) : ContMDiffAt I J n f x

A C^n submersion at x is C^n at 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 × M' → N × 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.

theorem Manifold.IsSubmersionOfComplement.contMDiff {𝕜 : 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) : ContMDiff I J n f

A C^n submersion is C^n

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 × M' → N × 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.

theorem Manifold.IsSubmersion.contMDiff {𝕜 : 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) : ContMDiff I J n f

A C^n submersion is C^n