Immersions under boundaryless model transport

Replacing a boundaryless model I : ModelWithCorners 𝕜 E H of M by its vector space E, as in TauCeti.BoundarylessModel I M, neither creates nor destroys immersions or smooth embeddings, on either the source or the target side.

The comparison is made chart by chart. An H-valued chart c of M and the E-valued chart TauCeti.BoundarylessModel.chart I c of the copy have the same extended coordinates, and every maximal chart of the copy arises in this way from TauCeti.BoundarylessModel.originalChart. So a normal form u ↦ (u, 0) of a map in one pair of charts is literally a normal form of the transported map in the corresponding pair, with the same complement and the same linear equivalence. In particular no composition theorem for immersions is used: Mathlib's Manifold.IsImmersionAtOfComplement.comp_diffeomorph only treats diffeomorphisms for a single model, and the identity M → BoundarylessModel I M changes the model from H to E.

This lets an immersion constructed on a self-modelled manifold, for instance from an implicit-function chart, be read as an immersion into the original manifold.

Main results

• TauCeti.BoundarylessModel.isImmersionAtOfComplement_target_iff and TauCeti.BoundarylessModel.isImmersionAtOfComplement_source_iff: the pointwise normal form with a fixed complement is preserved by changing the target or the source model.
• The corresponding statements for Manifold.IsImmersionAt, Manifold.IsImmersionOfComplement, Manifold.IsImmersion and Manifold.IsSmoothEmbedding.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionAtOfComplement_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : N → M} {x : N} : Manifold.IsImmersionAtOfComplement F J (modelWithCornersSelf 𝕜 E) n (⇑(homeomorph I M) ∘ g) x ↔ Manifold.IsImmersionAtOfComplement F J I n g x

Changing the target model preserves the immersion normal form at a point. A map g into M is an immersion at x with complement F exactly when it is one as a map into the self-modelled copy of M. The charts of the two normal forms correspond under TauCeti.BoundarylessModel.chart and TauCeti.BoundarylessModel.originalChart, with the same linear equivalence.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionOfComplement_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : N → M} : Manifold.IsImmersionOfComplement F J (modelWithCornersSelf 𝕜 E) n (⇑(homeomorph I M) ∘ g) ↔ Manifold.IsImmersionOfComplement F J I n g

Changing the target model preserves immersions with a fixed complement.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionAt_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : N → M} {x : N} : Manifold.IsImmersionAt J (modelWithCornersSelf 𝕜 E) n (⇑(homeomorph I M) ∘ g) x ↔ Manifold.IsImmersionAt J I n g x

Changing the target model preserves being an immersion at a point.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersion_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : N → M} : Manifold.IsImmersion J (modelWithCornersSelf 𝕜 E) n (⇑(homeomorph I M) ∘ g) ↔ Manifold.IsImmersion J I n g

Changing the target model preserves immersions.

@[simp]

theorem TauCeti.BoundarylessModel.isSmoothEmbedding_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : N → M} : Manifold.IsSmoothEmbedding J (modelWithCornersSelf 𝕜 E) n (⇑(homeomorph I M) ∘ g) ↔ Manifold.IsSmoothEmbedding J I n g

Changing the target model preserves smooth embeddings.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionAtOfComplement_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : M → N} {x : BoundarylessModel I M} : Manifold.IsImmersionAtOfComplement F (modelWithCornersSelf 𝕜 E) J n (g ∘ ⇑(homeomorph I M).symm) x ↔ Manifold.IsImmersionAtOfComplement F I J n g ((homeomorph I M).symm x)

Changing the source model preserves the immersion normal form at a point. A map g on M is an immersion at a point with complement F exactly when it is one as a map on the self-modelled copy of M. The charts of the two normal forms correspond under TauCeti.BoundarylessModel.chart and TauCeti.BoundarylessModel.originalChart, with the same linear equivalence.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionOfComplement_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : M → N} : Manifold.IsImmersionOfComplement F (modelWithCornersSelf 𝕜 E) J n (g ∘ ⇑(homeomorph I M).symm) ↔ Manifold.IsImmersionOfComplement F I J n g

Changing the source model preserves immersions with a fixed complement.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersionAt_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : M → N} {x : BoundarylessModel I M} : Manifold.IsImmersionAt (modelWithCornersSelf 𝕜 E) J n (g ∘ ⇑(homeomorph I M).symm) x ↔ Manifold.IsImmersionAt I J n g ((homeomorph I M).symm x)

Changing the source model preserves being an immersion at a point.

@[simp]

theorem TauCeti.BoundarylessModel.isImmersion_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : M → N} : Manifold.IsImmersion (modelWithCornersSelf 𝕜 E) J n (g ∘ ⇑(homeomorph I M).symm) ↔ Manifold.IsImmersion I J n g

Changing the source model preserves immersions.

@[simp]

theorem TauCeti.BoundarylessModel.isSmoothEmbedding_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {G : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {J : ModelWithCorners 𝕜 E' G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : M → N} : Manifold.IsSmoothEmbedding (modelWithCornersSelf 𝕜 E) J n (g ∘ ⇑(homeomorph I M).symm) ↔ Manifold.IsSmoothEmbedding I J n g

Changing the source model preserves smooth embeddings.