feat(Geometry/Manifold): API for extended coordinate changes

Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

@@ -23,11 +23,12 @@ in general, but we can still register them as `PartialEquiv`s.
 * `extChartAt I x`: the extended chart at `x`, obtained by composing the `chartAt H x` with `I`.
   Since the target is in general not open, this is not an open partial homeomorphism in general, but
   we register them as `PartialEquiv`s.
+* `I.extendCoordChange e e'`: the change of extended charts `(e.extend I).symm ≫ e'.extend I`.
 
 ## Main results
 
-* `contDiffOn_extend_coord_change`: if `f` and `f'` lie in the maximal atlas on `M`,
-  `f.extend I ∘ (f'.extend I).symm` is continuous on its source
+* `ModelWithCorners.contDiffOn_extendCoordChange`: if `f` and `f'` lie in the maximal atlas on `M`,
+  `I.extendCoordChange f f'` is Cⁿ on its source
 
 * `contDiffOn_ext_coord_change`: for `x x' : M`, the coordinate change
   `(extChartAt I x').symm ≫ extChartAt I x` is continuous on its source
@@ -315,58 +316,135 @@ theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs :
 lemma extend_prod (f' : OpenPartialHomeomorph M' H') :
     (f.prod f').extend (I.prod I') = (f.extend I).prod (f'.extend I') := by simp
 
-/-! We use the name `extend_coord_change` for `(f'.extend I).symm ≫ f.extend I`. -/
+end OpenPartialHomeomorph
+
+namespace ModelWithCorners
+
+/-- The change of charts from `e` to `e'` in the model vector space `E`. -/
+@[simps! apply symm_apply]
+def extendCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E :=
+  (e.extend I).symm ≫ e'.extend I
+
+variable {e e' : OpenPartialHomeomorph M H}
 
-theorem extend_coord_change_source :
-    ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source := by
-  simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source,
-    extend_target, inter_right_comm _ (range I)]
+lemma extendCoordChange_symm : (I.extendCoordChange e e').symm = I.extendCoordChange e' e := by
   rfl
 
-theorem extend_image_source_inter :
-    f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source := by
-  simp_rw [f.extend_coord_change_source, f.extend_coe, image_comp I f, trans_source'', symm_symm,
-    symm_target]
+lemma extendCoordChange_source :
+    (I.extendCoordChange e e').source = I '' (e.symm ≫ₕ e').source := by
+  simp_rw [extendCoordChange, PartialEquiv.trans_source, I.image_eq, e'.extend_source,
+    PartialEquiv.symm_source, e.extend_target, inter_right_comm _ (range I)]
+  rfl
 
-theorem extend_coord_change_source_mem_nhdsWithin {x : E}
-    (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) :
-    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x := by
-  rw [f.extend_coord_change_source] at hx ⊢
+lemma extendCoordChange_target :
+    (I.extendCoordChange e e').target = I '' (e.symm ≫ₕ e').target := by
+  rw [← PartialEquiv.symm_source, ← OpenPartialHomeomorph.symm_source]
+  exact I.extendCoordChange_source
+
+lemma _root_.OpenPartialHomeomorph.extend_image_source_inter :
+    f.extend I '' (f.source ∩ f'.source) = (I.extendCoordChange f f').source := by
+  simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
+    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
+    OpenPartialHomeomorph.symm_target]
+
+lemma extendCoordChange_source_mem_nhdsWithin {x : E}
+    (hx : x ∈ (I.extendCoordChange e e').source) :
+    (I.extendCoordChange e e').source ∈ 𝓝[range I] x := by
+  rw [I.extendCoordChange_source] at hx ⊢
   obtain ⟨x, hx, rfl⟩ := hx
   refine I.image_mem_nhdsWithin ?_
   exact (OpenPartialHomeomorph.open_source _).mem_nhds hx
 
-theorem extend_coord_change_source_mem_nhdsWithin' {x : M} (hxf : x ∈ f.source)
-    (hxf' : x ∈ f'.source) :
-    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x := by
-  apply extend_coord_change_source_mem_nhdsWithin
-  rw [← extend_image_source_inter]
-  exact mem_image_of_mem _ ⟨hxf, hxf'⟩
+lemma extendCoordChange_source_mem_nhdsWithin' {x : M} (hxe : x ∈ e.source)
+    (hxe' : x ∈ e'.source) :
+    (I.extendCoordChange e e').source ∈ 𝓝[range I] e.extend I x := by
+  apply extendCoordChange_source_mem_nhdsWithin
+  rw [← OpenPartialHomeomorph.extend_image_source_inter]
+  exact mem_image_of_mem _ ⟨hxe, hxe'⟩
+
+lemma uniqueDiffOn_extendCoordChange_source : UniqueDiffOn 𝕜 (I.extendCoordChange e e').source := by
+  rw [extendCoordChange_source, I.image_eq]
+  exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source
 
-variable {f f'}
+lemma uniqueDiffOn_extendCoordChange_target : UniqueDiffOn 𝕜 (I.extendCoordChange e e').target := by
+  rw [← extendCoordChange_symm, PartialEquiv.symm_target]
+  exact uniqueDiffOn_extendCoordChange_source
 
 open IsManifold
 
-theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) :
-    ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source := by
-  rw [extend_coord_change_source, I.image_eq]
-  exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1
-
-theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
-    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x := by
-  apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem_nhdsWithin
-  rw [extend_coord_change_source] at hx ⊢
+variable [ChartedSpace H M]
+
+lemma contDiffOn_extendCoordChange (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M) :
+    ContDiffOn 𝕜 n (I.extendCoordChange e e') (I.extendCoordChange e e').source := by
+  rw [I.extendCoordChange_source, I.image_eq]
+  exact (StructureGroupoid.compatible_of_mem_maximalAtlas he he').1
+
+lemma contDiffWithinAt_extendCoordChange (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ (I.extendCoordChange e e').source) :
+    ContDiffWithinAt 𝕜 n (I.extendCoordChange e e') (range I) x := by
+  apply (I.contDiffOn_extendCoordChange he he' x hx).mono_of_mem_nhdsWithin
+  rw [I.extendCoordChange_source] at hx ⊢
   obtain ⟨z, hz, rfl⟩ := hx
   exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)
 
-theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
-    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) := by
-  refine contDiffWithinAt_extend_coord_change hf hf' ?_
-  rw [← extend_image_source_inter]
-  exact mem_image_of_mem _ ⟨hxf', hxf⟩
+lemma contDiffWithinAt_extendCoordChange' (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) {x : M} (hxe : x ∈ e.source) (hxe' : x ∈ e'.source) :
+    ContDiffWithinAt 𝕜 n (I.extendCoordChange e e') (range I) (e.extend I x) := by
+  refine I.contDiffWithinAt_extendCoordChange he he' ?_
+  rw [← OpenPartialHomeomorph.extend_image_source_inter]
+  exact mem_image_of_mem _ ⟨hxe, hxe'⟩
+
+lemma contDiffOn_extendCoordChange_symm (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) :
+    ContDiffOn 𝕜 n (I.extendCoordChange e e').symm (I.extendCoordChange e e').target :=
+  I.contDiffOn_extendCoordChange he' he
+
+lemma isInvertible_fderivWithin_extendCoordChange (hn : n ≠ 0)
+    (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M)
+    {x : E} (hx : x ∈ (I.extendCoordChange e e').source) :
+    ContinuousLinearMap.IsInvertible <|
+      fderivWithin 𝕜 (I.extendCoordChange e e') (I.extendCoordChange e e').source x := by
+  set φ := I.extendCoordChange e e'
+  have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extendCoordChange he he'
+  have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extendCoordChange_symm he he'
+  refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
+  · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
+      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
+    · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
+    · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):)
+    · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
+    · exact φ.symm_mapsTo
+    · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
+  · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
+    · exact I.uniqueDiffOn_extendCoordChange_source _ hx
+    · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
+    · exact (hφ _ hx).differentiableWithinAt hn
+    · exact φ.mapsTo
+    · exact I.uniqueDiffOn_extendCoordChange_source _ hx
+
+end ModelWithCorners
+
+namespace OpenPartialHomeomorph
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source := ModelWithCorners.extendCoordChange_source
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source_mem_nhdsWithin :=
+  ModelWithCorners.extendCoordChange_source_mem_nhdsWithin
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source_mem_nhdsWithin' :=
+  ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffOn_extend_coord_change := ModelWithCorners.contDiffOn_extendCoordChange
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffWithinAt_extend_coord_change := ModelWithCorners.contDiffWithinAt_extendCoordChange
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffWithinAt_extend_coord_change' := ModelWithCorners.contDiffWithinAt_extendCoordChange'
 
 end OpenPartialHomeomorph
 
@@ -707,19 +785,19 @@ theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq
 theorem ext_coord_change_source (x x' : M) :
     ((extChartAt I x').symm ≫ extChartAt I x).source =
       I '' ((chartAt H x').symm ≫ₕ chartAt H x).source :=
-  extend_coord_change_source _ _
+  I.extendCoordChange_source
 
 open IsManifold
 
 theorem contDiffOn_ext_coord_change [IsManifold I n M] (x x' : M) :
     ContDiffOn 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm)
       ((extChartAt I x').symm ≫ extChartAt I x).source :=
-  contDiffOn_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')
+  I.contDiffOn_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x)
 
 theorem contDiffWithinAt_ext_coord_change [IsManifold I n M] (x x' : M) {y : E}
     (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
     ContDiffWithinAt 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) (range I) y :=
-  contDiffWithinAt_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x') hy
+  I.contDiffWithinAt_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x) hy
 
 variable (I I') in
 /-- Conjugating a function to write it in the preferred charts around `x`.

Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

@@ -60,13 +60,13 @@ theorem contDiffOn_fderiv_coord_change [IsManifold I (n + 1) M]
     ContDiffOn 𝕜 n (fderivWithin 𝕜 (j.1.extend I ∘ (i.1.extend I).symm) (range I))
       ((i.1.extend I).symm ≫ j.1.extend I).source := by
   have h : ((i.1.extend I).symm ≫ j.1.extend I).source ⊆ range I := by
-    rw [i.1.extend_coord_change_source]; apply image_subset_range
+    refine I.extendCoordChange_source.trans_subset ?_; apply image_subset_range
   intro x hx
   refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
     <| h hx).mono h
-  refine (OpenPartialHomeomorph.contDiffOn_extend_coord_change (subset_maximalAtlas j.2)
-    (subset_maximalAtlas i.2) x hx).mono_of_mem_nhdsWithin ?_
-  exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 hx
+  refine (I.contDiffOn_extendCoordChange (subset_maximalAtlas i.2)
+    (subset_maximalAtlas j.2) x hx).mono_of_mem_nhdsWithin ?_
+  exact I.extendCoordChange_source_mem_nhdsWithin hx
 
 open IsManifold
 
@@ -101,7 +101,7 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where
     refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
       (i.1.continuousOn_extend.mono ?_) ?_
     · rw [i.1.extend_source]; exact inter_subset_left
-    simp_rw [← i.1.extend_image_source_inter, mapsTo_image]
+    exact mapsTo_iff_image_subset.2 (i.1.extend_image_source_inter j.1).subset
   coordChange_comp := by
     have : IsManifold I (0 + 1) M := by simpa
     rintro i j k x ⟨⟨hxi, hxj⟩, hxk⟩ v
@@ -110,10 +110,10 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where
       filter_upwards [nhdsWithin_le_nhds this] with y hy
       simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]
     · simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
-    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas k.2)
-        (subset_maximalAtlas j.2) hxk hxj).differentiableWithinAt one_ne_zero
-    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas j.2)
-        (subset_maximalAtlas i.2) hxj hxi).differentiableWithinAt one_ne_zero
+    · exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas j.2)
+        (subset_maximalAtlas k.2) hxj hxk).differentiableWithinAt one_ne_zero
+    · exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas i.2)
+        (subset_maximalAtlas j.2) hxi hxj).differentiableWithinAt one_ne_zero
     · intro x _; exact mem_range_self _
     · exact I.uniqueDiffWithinAt_image
     · rw [Function.comp_apply, i.1.extend_left_inv hxi]

scripts/nolints_prime_decls.txt

@@ -3028,6 +3028,8 @@ Miu.le_pow2_and_pow2_eq_mod3'
 mk_eq_mk_of_basis'
 Mod_.comp_hom'
 Mod_.id_hom'
+ModelWithCorners.contDiffWithinAt_extendCoordChange'
+ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'
 ModularCyclotomicCharacter.toFun_spec'
 ModularCyclotomicCharacter.toFun_spec''
 ModularCyclotomicCharacter.toFun_unique'