chore: convenience constructor for IsImmersionAtOfComplement

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -157,21 +157,34 @@ theorem contMDiffOn_of_mem_contDiffGroupoid {e' : OpenPartialHomeomorph H H}
     (h : e' ∈ contDiffGroupoid n I) : ContMDiffOn I I n e' e'.source :=
   (contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_groupoid contDiffWithinAtProp_id h
 
-lemma OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn (φ : OpenPartialHomeomorph H H)
-    (hφ : ContMDiffOn I I n φ φ.source) (hφ' : ContMDiffOn I I n φ.symm φ.target) :
-    φ ∈ maximalAtlas I n H := by
-  simp only [mfld_simps, IsManifold.mem_maximalAtlas_iff, StructureGroupoid.maximalAtlas, forall_eq,
+lemma OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn [IsManifold I n M]
+    (φ : OpenPartialHomeomorph M H) (hφ : ContMDiffOn I I n φ φ.source)
+    (hφ' : ContMDiffOn I I n φ.symm φ.target) :
+    φ ∈ maximalAtlas I n M := by
+  simp only [mfld_simps, IsManifold.mem_maximalAtlas_iff, StructureGroupoid.maximalAtlas,
     contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid,
     ← contMDiffOn_iff_contDiffOn]
+  intro e he
+  have he' := contMDiffOn_of_mem_maximalAtlas (I := I) (n := n)
+    (StructureGroupoid.subset_maximalAtlas _ he)
+  have he'' := contMDiffOn_symm_of_mem_maximalAtlas (I := I) (n := n)
+    (StructureGroupoid.subset_maximalAtlas _ he)
   refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
   all_goals apply I.contMDiff.comp_contMDiffOn
-  · exact hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
-  · exact hφ.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
-  · exact hφ.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
-  · exact hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
-
-lemma IsManifold.mem_maximalAtlas_iff_contMDiffOn (φ : OpenPartialHomeomorph H H) :
-    φ ∈ maximalAtlas I n H ↔ ContMDiffOn I I n φ φ.source ∧ ContMDiffOn I I n φ.symm φ.target :=
+  · apply he'.comp (hφ'.comp (I.contMDiffOn_symm.mono (by simp)) ?_) (fun z hz ↦ by simp_all)
+    rw [inter_assoc]; exact inter_subset_left
+  · apply hφ.comp ?_ (fun z hz ↦ by simp_all)
+    apply he''.comp (I.contMDiffOn_symm.mono (by simp))
+    rw [inter_assoc]; exact inter_subset_left
+  · apply hφ.comp ?_ (fun z hz ↦ by simp_all)
+    apply he''.comp (I.contMDiffOn_symm.mono (by simp))
+    rw [inter_assoc]; exact inter_subset_left
+  · apply he'.comp (hφ'.comp (I.contMDiffOn_symm.mono (by simp)) ?_) (fun z hz ↦ by simp_all)
+    rw [inter_assoc]; exact inter_subset_left
+
+lemma IsManifold.mem_maximalAtlas_iff_contMDiffOn [IsManifold I n M]
+    (φ : OpenPartialHomeomorph M H) :
+    φ ∈ maximalAtlas I n M ↔ ContMDiffOn I I n φ φ.source ∧ ContMDiffOn I I n φ.symm φ.target :=
   ⟨fun h ↦ ⟨contMDiffOn_of_mem_maximalAtlas h, contMDiffOn_symm_of_mem_maximalAtlas h⟩,
    fun ⟨hφ, hφ'⟩ ↦ φ.mem_maximalAtlas_of_contMDiffOn hφ hφ'⟩
 

Mathlib/Geometry/Manifold/Immersion.lean

@@ -9,6 +9,7 @@
 public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
 public import Mathlib.Geometry.Manifold.LocalSourceTargetProperty
+public import Mathlib.Geometry.Manifold.Diffeomorph -- TODO: remove once Immersion.comp is proven!
 public import Mathlib.Geometry.Manifold.Notation
 public import Mathlib.Analysis.Normed.Module.Shrink  -- shake: keep (NormedAddCommGroup (Shrink ...)), cf. lean#13417
 public import Mathlib.Topology.Algebra.Module.TransferInstance
@@ -215,6 +216,17 @@
   LiftSourceTargetPropertyAt.mk_of_continuousAt hf isLocalSourceTargetProperty_immersionAtProp
     _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩
 
+/-- `f : M → N` is a `C^n` immersion at `x` if `f` is continuous at `x` and `f` looks like
+`u ↦ (u, 0)` in the preferred charts at `x` and `f x`.
+Special case of `mk_of_continuousAt` specialized to the preferred charts. -/
+lemma mk_of_continuousAt' [IsManifold I n M] [IsManifold J n N]
+    {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : (E × F) ≃L[𝕜] E'')
+    (hwrittenInExtend : EqOn ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm) (equiv ∘ (·, 0))
+      (extChartAt I x).target) : IsImmersionAtOfComplement F I J n f x :=
+  mk_of_continuousAt hf equiv (chartAt H x) (chartAt G (f x))
+    (mem_chart_source H x) (mem_chart_source G (f x))
+    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (f x)) hwrittenInExtend
+
 /-- A choice of chart on the domain `M` of an immersion `f` at `x`:
 w.r.t. this chart and the data `h.codChart` and `h.equiv`,
 `f` will look like an inclusion `u ↦ (u, 0)` in these extended charts.
@@ -388,20 +400,15 @@
 /- The inclusion of an open subset `s` of a smooth manifold `M` is an immersion at every point. -/
 lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (y : s) :
     IsImmersionAtOfComplement PUnit I I n (Subtype.val : s → M) y := by
-  apply IsImmersionAtOfComplement.mk_of_continuousAt (by fun_prop) (.prodUnique 𝕜 E _)
-    (chartAt H y) (chartAt H y.val) (mem_chart_source H y) (mem_chart_source H y.val)
-    (chart_mem_maximalAtlas y) (chart_mem_maximalAtlas y.val)
+  apply IsImmersionAtOfComplement.mk_of_continuousAt' (by fun_prop) (.prodUnique 𝕜 E _)
   intro x hx
   suffices I ((chartAt H ↑y) ((chartAt H y).symm (I.symm x))) = x by simpa +contextual
   simp_all
 
 /-- Every `ModelWithCorners 𝕜 E H` is an immersion when viewed as a map `H → E`. -/
 protected lemma _root_.ModelWithCorners.isImmersionAtOfComplement {n : ℕ} {x : H} :
     IsImmersionAtOfComplement PUnit I 𝓘(𝕜, E) n I x :=
-  Manifold.IsImmersionAtOfComplement.mk_of_continuousAt I.continuousAt
-    (.prodUnique _ _ _) (.refl _) (.refl _) (by simp) (by simp)
-    (IsManifold.subset_maximalAtlas (by simp)) (IsManifold.subset_maximalAtlas (by simp))
-    (by simp [Function.comp_def])
+  mk_of_continuousAt' I.continuousAt (.prodUnique _ _ _) (by simp [Function.comp_def])
 
 @[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
 
@@ -501,6 +508,26 @@
   refine ⟨hf.continuousWithinAt, ?_⟩
   exact aux hφ h' ht hxt
 
+-- A future PR will show that diffeomorphisms are immersions, and compositions are also immersions
+-- (possibly under additional hypotheses on `𝕜`). The next lemma may be golfed accordingly in the
+-- future.
+/-- Post-composing an immersion at `x` with a diffeomorphism still yields an immersion at `x`. -/
+lemma comp_diffeomorph
+    {N' : Type*} [TopologicalSpace N'] [ChartedSpace G N'] [IsManifold J n N] [IsManifold J n N']
+    (h : IsImmersionAtOfComplement F I J n f x) (Φ : Diffeomorph J J N N' n) :
+    IsImmersionAtOfComplement F I J n (Φ ∘ f) x := by
+  -- XXX: right now, `fun_prop` does not prove this (even with added tagging): investigate!
+  apply mk_of_continuousAt (Φ.continuous.continuousAt.comp h.continuousAt)
+    h.equiv (h.domChart) (Φ.symm.toHomeomorph.transOpenPartialHomeomorph h.codChart)
+    h.mem_domChart_source (by simp [h.mem_codChart_source])
+    h.domChart_mem_maximalAtlas ?_
+  · intro x hx
+    simpa using h.writtenInCharts hx
+  · apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
+    · have : Φ.symm.symm ⁻¹' Φ.symm ⁻¹' h.codChart.source = h.codChart.source := by ext; simp
+      simpa [this] using contMDiffOn_of_mem_maximalAtlas h.codChart_mem_maximalAtlas
+    · simpa using contMDiffOn_symm_of_mem_maximalAtlas h.codChart_mem_maximalAtlas
+
 end IsImmersionAtOfComplement
 
 namespace IsImmersionAt
@@ -696,6 +723,14 @@
     CMDiffAt n f x ↔ ContinuousAt f x ∧ CMDiffAt n (φ ∘ f) x := by
   rw [← ContMDiffAt.iff_comp_isImmersionAtOfComplement hφ.isImmersionAtOfComplement_complement]
 
+/-- Post-composing an immersion at `x` with a diffeomorphism still yields an immersion at `x`. -/
+lemma comp_diffeomorph
+    {N' : Type*} [TopologicalSpace N'] [ChartedSpace G N'] [IsManifold J n N] [IsManifold J n N']
+    (h : IsImmersionAt I J n f x) (Φ : Diffeomorph J J N N' n) :
+    IsImmersionAt I J n (Φ ∘ f) x := by
+  use h.complement, by infer_instance, by infer_instance
+  exact h.isImmersionAtOfComplement_complement.comp_diffeomorph Φ
+
 end IsImmersionAt
 
 variable (F I J n) in
@@ -777,9 +812,7 @@
 /-- The identity map is an immersion with complement `PUnit`. -/
 protected lemma id [IsManifold I n M] : IsImmersionOfComplement PUnit I I n (@id M) := by
   intro x
-  apply IsImmersionAtOfComplement.mk_of_continuousAt (continuousAt_id) (.prodUnique 𝕜 E _)
-    (chartAt H x) (chartAt H x) (mem_chart_source H x) (mem_chart_source H x)
-    (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x)
+  apply IsImmersionAtOfComplement.mk_of_continuousAt' (continuousAt_id) (.prodUnique 𝕜 E _)
   intro y hy
   have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
     rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
@@ -795,31 +828,32 @@
     IsImmersionOfComplement PUnit I (modelWithCornersSelf 𝕜 E) n I :=
   fun _ ↦ I.isImmersionAtOfComplement
 
+/-- Post-composing an immersion with a diffeomorphism still yields an immersion. -/
+lemma comp_diffeomorph
+    {N' : Type*} [TopologicalSpace N'] [ChartedSpace G N'] [IsManifold J n N] [IsManifold J n N']
+    (h : IsImmersionOfComplement F I J n f) (Φ : Diffeomorph J J N N' n) :
+    IsImmersionOfComplement F I J n (Φ ∘ f) :=
+  fun x ↦ (h x).comp_diffeomorph Φ
+
 /-- Given `C^n` manifolds `M` and `N` over the same model `I`,
 `Sum.inl : M → M ⊕ N` is a `C^n` immersion with complement `Unit` -/
-lemma sumInl {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M]
-    [IsManifold I n M'] : IsImmersionOfComplement Unit I I n (@Sum.inl M M') := by
+lemma sumInl {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M']
+    [IsManifold I n M] [IsManifold I n M'] :
+    IsImmersionOfComplement Unit I I n (@Sum.inl M M') := by
   intro x
-  apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
-    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inl x))
-    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inl x))
+  apply IsImmersionAtOfComplement.mk_of_continuousAt' (by fun_prop) (.prodUnique 𝕜 E _)
   intro y hy
   have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
     rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
   simpa
 
 /-- Given `C^n` manifolds `M` and `N` over the same model `I`,
 `Sum.inr : N → M ⊕ N` is a `C^n` immersion with complement `Unit` -/
-lemma sumInr {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M]
-    [IsManifold I n M'] : IsImmersionOfComplement Unit I I n (@Sum.inr M M') := by
-  intro x
-  apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
-    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inr x))
-    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inr x))
-  intro y hy
-  have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
-    rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
-  simpa
+lemma sumInr {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M']
+    [IsManifold I n M] [IsManifold I n M'] :
+    IsImmersionOfComplement Unit I I n (@Sum.inr M M') := by
+  rw [← Diffeomorph.sumComm_inl I M' n M]
+  exact IsImmersionOfComplement.sumInl.comp_diffeomorph (Diffeomorph.sumComm I M' n M)
 
 @[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
 
@@ -915,6 +949,14 @@
     CMDiff n f ↔ Continuous f ∧ CMDiff n (φ ∘ f) := by
   rw [ContMDiff.iff_comp_isImmersionOfComplement hφ.isImmersionOfComplement_complement]
 
+/-- Post-composing an immersion with a diffeomorphism still yields an immersion. -/
+lemma comp_diffeomorph
+    {N' : Type*} [TopologicalSpace N'] [ChartedSpace G N'] [IsManifold J n N] [IsManifold J n N']
+    (h : IsImmersion I J n f) (Φ : Diffeomorph J J N N' n) :
+    IsImmersion I J n (Φ ∘ f) := by
+  use h.complement, by infer_instance, by infer_instance
+  exact h.isImmersionOfComplement_complement.comp_diffeomorph Φ
+
 end IsImmersion
 
 end Manifold