Composing immersions with diffeomorphisms

Mathlib defines Manifold.IsImmersion by a normal form in charts — f looks like u ↦ (u, 0) for suitable charts of the source and the target — and lists IsImmersion.comp as a TODO in Mathlib/Geometry/Manifold/Immersion.lean, because a general composite has to combine two complements and needs the differential to split.

This file settles the special case that is elementary: composing with a diffeomorphism on either side. Nothing has to be recombined, because a diffeomorphism carries charts to charts: if φ is a chart of M in the maximal atlas and e : M' ≃ₘ M is a diffeomorphism, then φ ∘ e is a chart of M' in the maximal atlas, and reading f ∘ e in it produces literally the same normal form that f had in φ. The same argument on the other side pulls an ambient chart back along e⁻¹. So both composites are immersions with the same complement.

Since a diffeomorphism is invertible, every composition rule here is in fact an equivalence, and each is also stated in _iff form. The one-directional statements remain the primitive ones: they need a manifold structure only on the manifold e introduces, whereas the _iff forms need one on both sides, in order to apply the rule to e.symm as well.

Main results

• TauCeti.mem_maximalAtlas_diffeomorph_transOpenPartialHomeomorph: a diffeomorphism pulls a chart of the maximal atlas back to a chart of the maximal atlas. This is the only geometric input.
• TauCeti.isImmersion_comp_diffeomorph and TauCeti.isImmersion_diffeomorph_comp, together with their Manifold.IsImmersionAt, Manifold.IsImmersionAtOfComplement and Manifold.IsImmersionOfComplement counterparts and the _iff companions of all of them: immersions are stable under composition with a diffeomorphism on either side.
• TauCeti.isImmersion_diffeomorph: a diffeomorphism is an immersion.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, for immersions and their behaviour under composition.

theorem TauCeti.mem_maximalAtlas_diffeomorph_transOpenPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M'] (e : Diffeomorph I I M' M n) {φ : OpenPartialHomeomorph M H} (hφ : φ ∈ IsManifold.maximalAtlas I n M) : e.toHomeomorph.transOpenPartialHomeomorph φ ∈ IsManifold.maximalAtlas I n M'

A diffeomorphism e : M' ≃ₘ M pulls a chart φ of the maximal atlas of M back to the chart φ ∘ e of the maximal atlas of M'. This is the only geometric input to the composition results below: it is what lets a normal form in charts be read on the other side of a diffeomorphism.

The name records the hypothesis: for a mere homeomorphism e the pullback is a chart of the topological atlas, but not of the maximal C^n atlas.

theorem TauCeti.isImmersionAtOfComplement_comp_diffeomorph {𝕜 : 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'] (e : Diffeomorph I I M' M n) {x : M'} (h : Manifold.IsImmersionAtOfComplement F I J n f (e x)) : Manifold.IsImmersionAtOfComplement F I J n (f ∘ ⇑e) x

Precomposing with a diffeomorphism of the source preserves the immersion normal form at a point, with the same complement: the domain chart of the immersion is pulled back along the diffeomorphism, and f ∘ e read in the new chart is what f was in the old one.

theorem TauCeti.isImmersionAtOfComplement_diffeomorph_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] {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] {x : M} (h : Manifold.IsImmersionAtOfComplement F I J n f x) (e : Diffeomorph J J N P n) : Manifold.IsImmersionAtOfComplement F I J n (⇑e ∘ f) x

Postcomposing with a diffeomorphism of the target preserves the immersion normal form at a point, with the same complement: the codomain chart of the immersion is pulled back along the inverse diffeomorphism, and e ∘ f read in the new chart is what f was in the old one.

theorem TauCeti.isImmersionAt_comp_diffeomorph {𝕜 : 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'] (e : Diffeomorph I I M' M n) {x : M'} (h : Manifold.IsImmersionAt I J n f (e x)) : Manifold.IsImmersionAt I J n (f ∘ ⇑e) x

Precomposing with a diffeomorphism of the source preserves being an immersion at a point.

theorem TauCeti.isImmersionAt_diffeomorph_comp {𝕜 : 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] {x : M} (h : Manifold.IsImmersionAt I J n f x) (e : Diffeomorph J J N P n) : Manifold.IsImmersionAt I J n (⇑e ∘ f) x

Postcomposing with a diffeomorphism of the target preserves being an immersion at a point.

theorem TauCeti.isImmersionOfComplement_comp_diffeomorph {𝕜 : 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'] (e : Diffeomorph I I M' M n) (h : Manifold.IsImmersionOfComplement F I J n f) : Manifold.IsImmersionOfComplement F I J n (f ∘ ⇑e)

Precomposing an immersion with a fixed complement by a diffeomorphism of the source gives an immersion with the same complement.

theorem TauCeti.isImmersionOfComplement_diffeomorph_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] {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] (h : Manifold.IsImmersionOfComplement F I J n f) (e : Diffeomorph J J N P n) : Manifold.IsImmersionOfComplement F I J n (⇑e ∘ f)

Postcomposing an immersion with a fixed complement by a diffeomorphism of the target gives an immersion with the same complement.

theorem TauCeti.isImmersion_comp_diffeomorph {𝕜 : 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'] (e : Diffeomorph I I M' M n) (h : Manifold.IsImmersion I J n f) : Manifold.IsImmersion I J n (f ∘ ⇑e)

Reparametrising an immersion by a diffeomorphism of the source gives an immersion.

theorem TauCeti.isImmersion_diffeomorph_comp {𝕜 : 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] (h : Manifold.IsImmersion I J n f) (e : Diffeomorph J J N P n) : Manifold.IsImmersion I J n (⇑e ∘ f)

Transporting an immersion by a diffeomorphism of the target gives an immersion.

theorem TauCeti.isImmersionAtOfComplement_comp_diffeomorph_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'] (e : Diffeomorph I I M' M n) {x : M'} : Manifold.IsImmersionAtOfComplement F I J n (f ∘ ⇑e) x ↔ Manifold.IsImmersionAtOfComplement F I J n f (e x)

Precomposition with a diffeomorphism of the source neither creates nor destroys the immersion normal form at a point.

theorem TauCeti.isImmersionAt_comp_diffeomorph_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'] (e : Diffeomorph I I M' M n) {x : M'} : Manifold.IsImmersionAt I J n (f ∘ ⇑e) x ↔ Manifold.IsImmersionAt I J n f (e x)

Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion at a point.

theorem TauCeti.isImmersionOfComplement_comp_diffeomorph_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'] (e : Diffeomorph I I M' M n) : Manifold.IsImmersionOfComplement F I J n (f ∘ ⇑e) ↔ Manifold.IsImmersionOfComplement F I J n f

Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion with a fixed complement.

theorem TauCeti.isImmersion_comp_diffeomorph_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'] (e : Diffeomorph I I M' M n) : Manifold.IsImmersion I J n (f ∘ ⇑e) ↔ Manifold.IsImmersion I J n f

Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion.

theorem TauCeti.isImmersionAtOfComplement_diffeomorph_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] {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 N] [IsManifold J n P] (e : Diffeomorph J J N P n) {x : M} : Manifold.IsImmersionAtOfComplement F I J n (⇑e ∘ f) x ↔ Manifold.IsImmersionAtOfComplement F I J n f x

Postcomposition with a diffeomorphism of the target neither creates nor destroys the immersion normal form at a point.

theorem TauCeti.isImmersionAt_diffeomorph_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] {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 N] [IsManifold J n P] (e : Diffeomorph J J N P n) {x : M} : Manifold.IsImmersionAt I J n (⇑e ∘ f) x ↔ Manifold.IsImmersionAt I J n f x

Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion at a point.

theorem TauCeti.isImmersionOfComplement_diffeomorph_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] {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 N] [IsManifold J n P] (e : Diffeomorph J J N P n) : Manifold.IsImmersionOfComplement F I J n (⇑e ∘ f) ↔ Manifold.IsImmersionOfComplement F I J n f

Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion with a fixed complement.

theorem TauCeti.isImmersion_diffeomorph_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] {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 N] [IsManifold J n P] (e : Diffeomorph J J N P n) : Manifold.IsImmersion I J n (⇑e ∘ f) ↔ Manifold.IsImmersion I J n f

Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion.

theorem TauCeti.isImmersion_diffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_8} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I n M'] (e : Diffeomorph I I M M' n) : Manifold.IsImmersion I I n ⇑e

A diffeomorphism is an immersion: it is the identity immersion transported by itself.

This is the statement Mathlib lists as the TODO Diffeomorph.isImmersion in Mathlib/Geometry/Manifold/Immersion.lean; the name is flat here because a Diffeomorph namespace nested in TauCeti would break dot notation on Mathlib's type.