Composing submersions with local diffeomorphisms

Mathlib defines Manifold.IsSubmersionAt by a normal form in charts: around x there are charts of the source and target in which the map reads as the projection (u, v) ↦ u. This file proves that composing with a C^n local diffeomorphism, on either side, preserves this normal form at a point, with the same complement. It is the submersion counterpart of TauCeti.Geometry.Manifold.Immersion.LocalDiffeomorph.

Nothing has to be recombined. A partial diffeomorphism Φ of the source carries a chart ψ of the maximal atlas to the chart Φ ≫ ψ, and f ∘ Φ read in it is f read in ψ. On the target, a partial diffeomorphism Θ near f x pulls a chart χ back to Θ⁻¹ ≫ χ, and Θ ∘ f read in it is f read in χ, once the source chart is shrunk so that f maps it into the source of Θ.

Precomposition with a local diffeomorphism g also reflects the normal form: f is a submersion at g x as soon as f ∘ g is a submersion at x, because near g x the map f agrees with f ∘ g composed with a local inverse of g, again a local diffeomorphism. This is how a map out of a quotient manifold, such as the orbit space of a free properly discontinuous action, is shown to be a submersion: the orbit projection is a local diffeomorphism, so it suffices to check the lift of the map to the covering manifold.

Main results

• IsLocalDiffeomorphAt.isSubmersionAtOfComplement_comp, IsLocalDiffeomorphAt.comp_isSubmersionAtOfComplement: the pointwise normal form with a fixed complement survives composing with a local diffeomorphism on the source or on the target.
• IsLocalDiffeomorphAt.isSubmersionAtOfComplement_comp_iff: precomposing with a local diffeomorphism at x neither creates nor destroys the normal form at x.
• IsLocalDiffeomorphAt.isSubmersionAt_comp_iff, IsLocalDiffeomorphAt.comp_isSubmersionAt: the same statements for IsSubmersionAt.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 4, for submersions and their behaviour under composition.

Precomposing with a local diffeomorphism

theorem IsLocalDiffeomorphAt.isSubmersionAtOfComplement_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) (h : Manifold.IsSubmersionAtOfComplement F I J n f (g x)) : Manifold.IsSubmersionAtOfComplement F I J n (f ∘ g) x

Precomposing with a local diffeomorphism of the source preserves the submersion normal form at a point, with the same complement: the domain chart is pulled back along a partial diffeomorphism representing the local diffeomorphism.

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

Submersions out of a local diffeomorphism. If g is a local diffeomorphism at x, then f ∘ g is a submersion at x with complement F exactly when f is a submersion at g x with complement F. Near g x, the map f is f ∘ g composed with a local inverse of g.

theorem IsLocalDiffeomorphAt.isSubmersionAt_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [IsManifold I n M] [IsManifold I n M'] {g : M' → M} {x : M'} (hg : IsLocalDiffeomorphAt I I n g x) : Manifold.IsSubmersionAt I J n (f ∘ g) x ↔ Manifold.IsSubmersionAt I J n f (g x)

Precomposing with a local diffeomorphism at x neither creates nor destroys being a submersion at x.

Postcomposing with a local diffeomorphism

theorem IsLocalDiffeomorphAt.comp_isSubmersionAtOfComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} {x : M} (hk : IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsSubmersionAtOfComplement F I J n f x) : Manifold.IsSubmersionAtOfComplement F I J n (k ∘ f) x

Postcomposing with a local diffeomorphism of the target preserves the submersion normal form at a point, with the same complement: the codomain chart is pulled back along a partial diffeomorphism representing the local diffeomorphism, after shrinking the domain chart so that the submersion maps it into the source of that partial diffeomorphism.

theorem IsLocalDiffeomorphAt.comp_isSubmersionAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace G N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace G P] {n : WithTop ℕ∞} {f : M → N} [IsManifold J n P] {k : N → P} {x : M} (hk : IsLocalDiffeomorphAt J J n k (f x)) (h : Manifold.IsSubmersionAt I J n f x) : Manifold.IsSubmersionAt I J n (k ∘ f) x

Postcomposing with a local diffeomorphism of the target preserves being a submersion at a point.