From f2597842a0fa21d17413581400598615173a9465 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:10:05 +0100 Subject: [PATCH 01/38] feat: the set of points where IsImmersionAt holds is open --- Mathlib/Geometry/Manifold/Immersion.lean | 27 +++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 81a5132e89b0e5..32e2ab13b76f07 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -45,6 +45,8 @@ This shortens the overall argument, as the definition of submersions has the sam * `IsImmersionAtOfComplement.congr_F`, `IsImmersionOfComplement.congr_F`: being an immersion (at `x`) w.r.t. `F` is stable under replacing the complement `F` by an isomorphic copy +* `isOpen_isImmersionAtOfComplement` and `isOpen_isImmersionAt`: + the set of points where `IsImmersionAt(OfComplement)` holds is open. ## Implementation notes @@ -64,7 +66,6 @@ This shortens the overall argument, as the definition of submersions has the sam ## TODO * The converse to `IsImmersionAtOfComplement.congr_F` also holds: any two complements are isomorphic, as they are isomorphic to the cokernel of the differential `mfderiv I J f x`. -* The set where `IsImmersionAt(OfComplement)` holds is open. * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. * `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`. * `IsImmersionAt.prodMap`: the product of two immersions is an immersion. @@ -356,6 +357,22 @@ lemma congr_F (e : F ≃L[π•œ] F') : IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F' I J n f x := ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩ +/- The set of points where `IsImmersionAtOfComplement` holds is open. -/ +lemma _root_.isOpen_isImmersionAtOfComplement : + IsOpen {x | IsImmersionAtOfComplement F I J n f x} := by + rw [isOpen_iff_forall_mem_open] + intro x hx + -- Suppose `f` is an immersion at `x`: choose slice charts Ο† near x and ψ near f x s.t. + -- `f` looks like `u ↦ (u, 0)` in these charts. Then the same charts witness that `f` is an + -- immersion at any `y ∈ Ο†.source`. + simp only [mem_setOf_eq, IsImmersionAtOfComplement_def] at hx + refine ⟨hx.domChart.source, ?_, hx.domChart.open_source, hx.mem_domChart_source⟩ + intro x' hx' + rw [mem_setOf_eq, IsImmersionAtOfComplement_def] + exact ⟨hx.domChart, hx.codChart, hx', hx.source_subset_preimage_source hx', + hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source, + hx.property⟩ + /-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`. Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe, @@ -515,6 +532,14 @@ lemma congr_iff (hfg : f =αΆ [𝓝 x] g) : IsImmersionAt I J n f x ↔ IsImmersionAt I J n g x := ⟨fun h ↦ h.congr_of_eventuallyEq hfg, fun h ↦ h.congr_of_eventuallyEq hfg.symm⟩ +/- The set of points where `IsImmersionAt` holds is open. -/ +lemma _root_.isOpen_isImmersionAt : + IsOpen {x | IsImmersionAt I J n f x} := by + rw [isOpen_iff_forall_mem_open] + exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x }, + fun y hy ↦ hy.isImmersionAt, + isOpen_isImmersionAtOfComplement, by simp [hx.isImmersionAtOfComplement_complement]⟩ + end IsImmersionAt variable (F I J n) in From f1be0dfa175a8ca5ac943459df7afb741d870bfb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:17:36 +0100 Subject: [PATCH 02/38] Preliminary lemmas --- .../Geometry/Manifold/IsManifold/Basic.lean | 24 +++++++++++++++++++ .../Manifold/IsManifold/ExtChartAt.lean | 3 +++ Mathlib/Topology/OpenPartialHomeomorph.lean | 5 ++++ 3 files changed, 32 insertions(+) diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean index a7515014e549b8..baa594817ac6fd 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean @@ -927,6 +927,30 @@ instance prod {π•œ : Type*} [NontriviallyNormedField π•œ] {E : Type*} [NormedA have h2 := (contDiffGroupoid n I').compatible hf2 hg2 exact contDiffGroupoid_prod h1 h2 + +section + +variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type*} + [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {n : WithTop β„•βˆž} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] + +lemma mem_maximalAtlas_prod [IsManifold I n M] [IsManifold I' n M'] + {e : OpenPartialHomeomorph M H} (he : e ∈ maximalAtlas I n M) + {e' : OpenPartialHomeomorph M' H'} (he' : e' ∈ maximalAtlas I' n M') : + e.prod e' ∈ maximalAtlas (I.prod I') n (M Γ— M') := by + simp only [maximalAtlas, mem_maximalAtlas_iff] + rintro e'' ⟨f, hf, f', hf', rfl⟩ + rw [_root_.OpenPartialHomeomorph.prod_symm_trans_prod, + _root_.OpenPartialHomeomorph.prod_symm_trans_prod] + exact ⟨contDiffGroupoid_prod + (compatible_of_mem_maximalAtlas he (subset_maximalAtlas hf)) + (compatible_of_mem_maximalAtlas he' (subset_maximalAtlas hf')), + contDiffGroupoid_prod + (compatible_of_mem_maximalAtlas (subset_maximalAtlas hf) he) + (compatible_of_mem_maximalAtlas (subset_maximalAtlas hf') he')⟩ + +end + section DisjointUnion variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index df6a02a14d842c..37a04b2aed1b8c 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -319,6 +319,9 @@ theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx, map_extend_nhdsWithin_eq_image_of_subset _ hx 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`. -/ theorem extend_coord_change_source : diff --git a/Mathlib/Topology/OpenPartialHomeomorph.lean b/Mathlib/Topology/OpenPartialHomeomorph.lean index f7f1ffbcccfa0a..fcfc642dd65048 100644 --- a/Mathlib/Topology/OpenPartialHomeomorph.lean +++ b/Mathlib/Topology/OpenPartialHomeomorph.lean @@ -1011,6 +1011,11 @@ theorem prod_eq_prod_of_nonempty' (h : (eX'.prod eY').source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY' := by rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY'] +theorem prod_symm_trans_prod + (e f : OpenPartialHomeomorph X Y) (e' f' : OpenPartialHomeomorph X' Y') : + (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f') := by + simp + end Prod /-! finite product of partial homeomorphisms -/ From 0200fd0ebf39f2531cc00b831d248eb32fd5a660 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:29:43 +0100 Subject: [PATCH 03/38] chore(LocalSourceTargetProperty): clean up variable names Use I and J consistently. Also add further variables for use when adding products. --- .../Manifold/LocalSourceTargetProperty.lean | 65 +++++++++++-------- 1 file changed, 37 insertions(+), 28 deletions(-) diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 6a666eb7f58b01..9f7b45e2a351af 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -42,14 +42,16 @@ open scoped Manifold Topology ContDiff open Function Set -variable {π•œ : Type*} [NontriviallyNormedField π•œ] - {E : Type*} [NormedAddCommGroup E] [NormedSpace π•œ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] - {H : Type*} [TopologicalSpace H] {G : Type*} [TopologicalSpace G] - {I : ModelWithCorners π•œ E H} {I' : ModelWithCorners π•œ F G} - -variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - {N : Type*} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop β„•βˆž} +variable {π•œ E E' F F' H H' G G' : Type*} [NontriviallyNormedField π•œ] + [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedAddCommGroup E'] [NormedSpace π•œ E'] + [NormedAddCommGroup F] [NormedSpace π•œ F] [NormedAddCommGroup F'] [NormedSpace π•œ F'] + [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] + {I : ModelWithCorners π•œ E H} {I' : ModelWithCorners π•œ E' H'} + {J : ModelWithCorners π•œ F G} {J' : ModelWithCorners π•œ F' G'} + {M M' N N' : Type*} [TopologicalSpace M] [ChartedSpace H M] + [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] + [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] + {n : WithTop β„•βˆž} namespace Manifold @@ -67,7 +69,7 @@ structure IsLocalSourceTargetProperty congr : βˆ€ {f g : M β†’ N}, βˆ€ {Ο† : OpenPartialHomeomorph M H}, βˆ€ {ψ : OpenPartialHomeomorph N G}, EqOn f g Ο†.source β†’ P f Ο† ψ β†’ P g Ο† ψ -variable (I I' n) in +variable (I J n) in /-- Data witnessing the fact that `f` has local property `P` at `x` -/ structure LocalPresentationAt (f : M β†’ N) (x : M) (P : (M β†’ N) β†’ OpenPartialHomeomorph M H β†’ OpenPartialHomeomorph N G β†’ Prop) where @@ -80,11 +82,11 @@ structure LocalPresentationAt (f : M β†’ N) (x : M) mem_domChart_source : x ∈ domChart.source mem_codChart_source : f x ∈ codChart.source domChart_mem_maximalAtlas : domChart ∈ IsManifold.maximalAtlas I n M - codChart_mem_maximalAtlas : codChart ∈ IsManifold.maximalAtlas I' n N + codChart_mem_maximalAtlas : codChart ∈ IsManifold.maximalAtlas J n N source_subset_preimage_source : domChart.source βŠ† f ⁻¹' codChart.source property : P f domChart codChart -variable (I I' n) in +variable (I J n) in /-- The induced property by a local property `P`: it is satisfied for `f` at `x` iff there exist charts `Ο†` and `ψ` of `M` and `N` around `x` and `f x`, respectively, such that `f` satisfies `P` w.r.t. `Ο†` and `ψ`. @@ -96,7 +98,7 @@ in the charts `Ο†` and `ψ`. @[expose] def LiftSourceTargetPropertyAt (f : M β†’ N) (x : M) (P : (M β†’ N) β†’ OpenPartialHomeomorph M H β†’ OpenPartialHomeomorph N G β†’ Prop) : Prop := - Nonempty (LocalPresentationAt I I' n f x P) + Nonempty (LocalPresentationAt I J n f x P) namespace LiftSourceTargetPropertyAt @@ -104,46 +106,46 @@ variable {f g : M β†’ N} {x : M} {P : (M β†’ N) β†’ OpenPartialHomeomorph M H β†’ OpenPartialHomeomorph N G β†’ Prop} /-- A choice of charts witnessing the local property `P` of `f` at `x`. -/ -noncomputable def localPresentationAt (h : LiftSourceTargetPropertyAt I I' n f x P) : - LocalPresentationAt I I' n f x P := +noncomputable def localPresentationAt (h : LiftSourceTargetPropertyAt I J n f x P) : + LocalPresentationAt I J n f x P := Classical.choice h /-- A choice of chart on the domain `M` of a local property of `f` at `x`: w.r.t. this chart and `h.codChart`, `f` has the local property `P` at `x`. The particular chart is arbitrary, but this choice matches the witness given by `h.codChart`. -/ -noncomputable def domChart (h : LiftSourceTargetPropertyAt I I' n f x P) : +noncomputable def domChart (h : LiftSourceTargetPropertyAt I J n f x P) : OpenPartialHomeomorph M H := h.localPresentationAt.domChart /-- A choice of chart on the co-domain `N` of a local property of `f` at `x`: w.r.t. this chart and `h.domChart`, `f` has the local property `P` at `x` The particular chart is arbitrary, but this choice matches the witness given by `h.domChart`. -/ -noncomputable def codChart (h : LiftSourceTargetPropertyAt I I' n f x P) : +noncomputable def codChart (h : LiftSourceTargetPropertyAt I J n f x P) : OpenPartialHomeomorph N G := h.localPresentationAt.codChart -lemma mem_domChart_source (h : LiftSourceTargetPropertyAt I I' n f x P) : +lemma mem_domChart_source (h : LiftSourceTargetPropertyAt I J n f x P) : x ∈ h.domChart.source := h.localPresentationAt.mem_domChart_source -lemma mem_codChart_source (h : LiftSourceTargetPropertyAt I I' n f x P) : +lemma mem_codChart_source (h : LiftSourceTargetPropertyAt I J n f x P) : f x ∈ h.codChart.source := h.localPresentationAt.mem_codChart_source -lemma domChart_mem_maximalAtlas (h : LiftSourceTargetPropertyAt I I' n f x P) : +lemma domChart_mem_maximalAtlas (h : LiftSourceTargetPropertyAt I J n f x P) : h.domChart ∈ IsManifold.maximalAtlas I n M := h.localPresentationAt.domChart_mem_maximalAtlas -lemma codChart_mem_maximalAtlas (h : LiftSourceTargetPropertyAt I I' n f x P) : - h.codChart ∈ IsManifold.maximalAtlas I' n N := +lemma codChart_mem_maximalAtlas (h : LiftSourceTargetPropertyAt I J n f x P) : + h.codChart ∈ IsManifold.maximalAtlas J n N := h.localPresentationAt.codChart_mem_maximalAtlas lemma source_subset_preimage_source - (h : LiftSourceTargetPropertyAt I I' n f x P) : + (h : LiftSourceTargetPropertyAt I J n f x P) : h.domChart.source βŠ† f ⁻¹' h.codChart.source := h.localPresentationAt.source_subset_preimage_source -lemma property (h : LiftSourceTargetPropertyAt I I' n f x P) : P f h.domChart h.codChart := +lemma property (h : LiftSourceTargetPropertyAt I J n f x P) : P f h.domChart h.codChart := h.localPresentationAt.property omit [ChartedSpace H M] [ChartedSpace G N] in @@ -160,8 +162,8 @@ lemma mk_of_continuousAt (hf : ContinuousAt f x) (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G) (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source) (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) - (hcodChart : codChart ∈ IsManifold.maximalAtlas I' n N) - (hfP : P f domChart codChart) : LiftSourceTargetPropertyAt I I' n f x P := by + (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) + (hfP : P f domChart codChart) : LiftSourceTargetPropertyAt I J n f x P := by obtain ⟨s, hs, hsopen, hxs⟩ := mem_nhds_iff.mp <| hf.preimage_mem_nhds (codChart.open_source.mem_nhds hfx) exact ⟨domChart.restr s, codChart, by grind, hfx, @@ -172,8 +174,8 @@ lemma mk_of_continuousAt (hf : ContinuousAt f x) if `f` has property `P` at `x` and `f` and `g` are eventually equal near `x`, then `g` has property `P` at `x`. -/ lemma congr_of_eventuallyEq (hP : IsLocalSourceTargetProperty P) - (hf : LiftSourceTargetPropertyAt I I' n f x P) - (h' : f =αΆ [nhds x] g) : LiftSourceTargetPropertyAt I I' n g x P := by + (hf : LiftSourceTargetPropertyAt I J n f x P) + (h' : f =αΆ [nhds x] g) : LiftSourceTargetPropertyAt I J n g x P := by obtain ⟨s', hxs', hfg⟩ := h'.exists_mem obtain ⟨s, hss', hs, hxs⟩ := mem_nhds_iff.mp hxs' refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩ @@ -191,7 +193,14 @@ lemma congr_of_eventuallyEq (hP : IsLocalSourceTargetProperty P) and `f` and `g` are eventually equal near `x`, then `f` has property `P` at `x` if and only if `g` has property `P` at `x`. -/ lemma congr_iff_of_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f =αΆ [nhds x] g) : - LiftSourceTargetPropertyAt I I' n f x P ↔ LiftSourceTargetPropertyAt I I' n g x P := + LiftSourceTargetPropertyAt I J n f x P ↔ LiftSourceTargetPropertyAt I J n g x P := + ⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩ + +/-- If `P` is monotone w.r.t. restricting `domChart` and closed under congruence, +and `f` and `g` are eventually equal near `x`, +then `f` has property `P` at `x` if and only if `g` has property `P` at `x`. -/ +lemma congr_iff_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f =αΆ [nhds x] g) : + LiftSourceTargetPropertyAt I J n f x P ↔ LiftSourceTargetPropertyAt I J n g x P := ⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩ end LiftSourceTargetPropertyAt From e9c4f480a2ad53035740cf6d5e73417080fdcb74 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:33:35 +0100 Subject: [PATCH 04/38] chore: LocalSourceTargetProperty version of the product lemma There are a bunch of CI warnings, which are all false positives. --- .../Manifold/LocalSourceTargetProperty.lean | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 9f7b45e2a351af..b6c3b7a93f1837 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -203,6 +203,28 @@ lemma congr_iff_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f =αΆ [n LiftSourceTargetPropertyAt I J n f x P ↔ LiftSourceTargetPropertyAt I J n g x P := ⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩ +lemma prodMap [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] + {Q : (M' β†’ N') β†’ OpenPartialHomeomorph M' H' β†’ OpenPartialHomeomorph N' G' β†’ Prop} + {R : ((M Γ— M') β†’ (N Γ— N')) β†’ OpenPartialHomeomorph (M Γ— M') (H Γ— H') β†’ + OpenPartialHomeomorph (N Γ— N') (G Γ— G') β†’ Prop} + (hf : LiftSourceTargetPropertyAt I J n f x P) {g : M' β†’ N'} {x' : M'} + (hg : LiftSourceTargetPropertyAt I' J' n g x' Q) + (h : βˆ€ {f : M β†’ N}, βˆ€ {φ₁ : OpenPartialHomeomorph M H}, βˆ€ {Οˆβ‚ : OpenPartialHomeomorph N G}, + βˆ€ {g : M' β†’ N'}, βˆ€ {Ο†β‚‚ : OpenPartialHomeomorph M' H'}, βˆ€ {Οˆβ‚‚ : OpenPartialHomeomorph N' G'}, + P f φ₁ Οˆβ‚ β†’ Q g Ο†β‚‚ Οˆβ‚‚ β†’ R (Prod.map f g) (φ₁.prod Ο†β‚‚) (Οˆβ‚.prod Οˆβ‚‚)) : + LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R := by + use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart + Β· simp [hf.mem_domChart_source, hg.mem_domChart_source] + Β· simp [mem_codChart_source hf, mem_codChart_source hg] + Β· exact IsManifold.mem_maximalAtlas_prod + (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg) + Β· apply IsManifold.mem_maximalAtlas_prod + (codChart_mem_maximalAtlas hf) (codChart_mem_maximalAtlas hg) + Β· simp only [OpenPartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source, + preimage_prod_map_prod] + exact prod_mono hf.source_subset_preimage_source hg.source_subset_preimage_source + Β· exact h hf.property hg.property + end LiftSourceTargetPropertyAt end Manifold From b105bfd7919e0ba36880874babaeb22d79c09c7e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:20:42 +0100 Subject: [PATCH 05/38] feat: product of immersions --- Mathlib/Geometry/Manifold/Immersion.lean | 89 +++++++++++++++++++++++- 1 file changed, 88 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 32e2ab13b76f07..c8bbac09e776a1 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -47,6 +47,8 @@ This shortens the overall argument, as the definition of submersions has the sam replacing the complement `F` by an isomorphic copy * `isOpen_isImmersionAtOfComplement` and `isOpen_isImmersionAt`: the set of points where `IsImmersionAt(OfComplement)` holds is open. +* `IsImmersionAt.prodMap` and `IsImmersion.prodMap`: the product of two immersions (at a point) + is an immersion (at a point). ## Implementation notes @@ -68,7 +70,6 @@ This shortens the overall argument, as the definition of submersions has the sam isomorphic, as they are isomorphic to the cokernel of the differential `mfderiv I J f x`. * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. * `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`. -* `IsImmersionAt.prodMap`: the product of two immersions is an immersion. * If `f` is an immersion at `x`, its differential splits, hence is injective. * If `f : M β†’ N` is a map between Banach manifolds, `mfderiv I J f x` splitting implies `f` is an immersion at `x`. (This requires the inverse function theorem.) @@ -373,6 +374,67 @@ lemma _root_.isOpen_isImmersionAtOfComplement : hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source, hx.property⟩ +-- Can grind prove the next two lemmas, after sufficient future tagging? +-- Which of these two proofs is better? +lemma _root_.aux1 {Ξ± Ξ² Ξ³ Ξ΄ : Type*} {f f' : Ξ± β†’ Ξ³} {g g' : Ξ² β†’ Ξ΄} {s : Set Ξ±} {t : Set Ξ²} + (h : EqOn (Prod.map f g) (Prod.map f' g') (s Γ—Λ’ t)) (ht : Set.Nonempty t) : + EqOn f f' s := by + choose x0 hx0 using ht + have a : f = (Prod.fst) ∘ (Prod.map f g) ∘ (Β·, x0) := by ext x; simp + have b : f' = Prod.fst ∘ (Prod.map f' g') ∘ (Β·, x0) := by ext x; simp + rw [a, b] + exact (eqOn_comp_right_iff.mpr <| h.mono (image_prodMk_subset_prod_left hx0)).comp_left + +lemma _root_.aux2 {Ξ± Ξ² Ξ³ Ξ΄ : Type*} {f f' : Ξ± β†’ Ξ³} {g g' : Ξ² β†’ Ξ΄} {s : Set Ξ±} {t : Set Ξ²} + (h : EqOn (Prod.map f g) (Prod.map f' g') (s Γ—Λ’ t)) (hs : Set.Nonempty s) : + EqOn g g' t := by + choose xs hxs using hs + intro x hx + have h' := h <| mk_mem_prod hxs hx + simp only [Prod.map_apply, Prod.mk.injEq] at h' + exact h'.2 + +-- TODO: move to Data.Set.Operations +lemma _root_.Set.EqOn.prodMap {Ξ± Ξ² Ξ³ Ξ΄ : Type*} + {f f' : Ξ± β†’ Ξ³} {g g' : Ξ² β†’ Ξ΄} {s : Set Ξ±} {t : Set Ξ²} + (hf : EqOn f f' s) (hg : EqOn g g' t) : EqOn (Prod.map f g) (Prod.map f' g') (s Γ—Λ’ t) := by + rintro ⟨x, x'⟩ ⟨hx, hx'⟩ + simp [hf hx, hg hx'] + +lemma aux {Ξ± Ξ² Ξ³ Ξ΄ : Type*} {f f' : Ξ± β†’ Ξ³} {g g' : Ξ² β†’ Ξ΄} + {s : Set Ξ±} {t : Set Ξ²} (hs : Set.Nonempty s) (ht : Set.Nonempty t) : + EqOn (Prod.map f g) (Prod.map f' g') (s Γ—Λ’ t) ↔ EqOn f f' s ∧ EqOn g g' t := + ⟨fun h ↦ ⟨aux1 h ht, aux2 h hs⟩, fun ⟨h, h'⟩ ↦ h.prodMap h'⟩ + +/-- If `f: M β†’ N` and `g: M' Γ— N'` are immersions at `x` and `x'`, respectively, +then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ +theorem prodMap {f : M β†’ N} {g : M' β†’ N'} {x' : M'} + [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] + (hf : IsImmersionAtOfComplement F I J n f x) (hg : IsImmersionAtOfComplement F' I' J' n g x') : + IsImmersionAtOfComplement (F Γ— F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := by + let P := ImmersionAtProp F I J M N + let Q := ImmersionAtProp F' I' J' M' N' + let R := ImmersionAtProp (F Γ— F') (I.prod I') (J.prod J') (M Γ— M') (N Γ— N') + -- This is the key proof: immersions are stable under products. + have key : βˆ€ {f : M β†’ N}, βˆ€ {φ₁ : OpenPartialHomeomorph M H}, βˆ€ {Οˆβ‚ : OpenPartialHomeomorph N G}, + βˆ€ {g : M' β†’ N'}, βˆ€ {Ο†β‚‚ : OpenPartialHomeomorph M' H'}, βˆ€ {Οˆβ‚‚ : OpenPartialHomeomorph N' G'}, + P f φ₁ Οˆβ‚ β†’ Q g Ο†β‚‚ Οˆβ‚‚ β†’ R (Prod.map f g) (φ₁.prod Ο†β‚‚) (Οˆβ‚.prod Οˆβ‚‚) := by + rintro f φ₁ Οˆβ‚ g Ο†β‚‚ Οˆβ‚‚ ⟨equiv₁, hfprop⟩ ⟨equivβ‚‚, hgprop⟩ + use (ContinuousLinearEquiv.prodProdProdComm π•œ E E' F F').trans (equiv₁.prodCongr equivβ‚‚) + rw [φ₁.extend_prod Ο†β‚‚, Οˆβ‚.extend_prod, PartialEquiv.prod_target] + set C := ((Οˆβ‚.extend J).prod (Οˆβ‚‚.extend J')) ∘ + Prod.map f g ∘ ((φ₁.extend I).prod (Ο†β‚‚.extend I')).symm + have hC : C = Prod.map ((Οˆβ‚.extend J) ∘ f ∘ (φ₁.extend I).symm) + ((Οˆβ‚‚.extend J') ∘ g ∘ (Ο†β‚‚.extend I').symm) := by + ext x <;> simp [C] + set Ξ¦ := (((ContinuousLinearEquiv.prodProdProdComm π•œ E E' F F').trans + (equiv₁.prodCongr equivβ‚‚)) ∘ (Β·, 0)) + have hΞ¦: Ξ¦ = Prod.map (equiv₁ ∘ (Β·, 0)) (equivβ‚‚ ∘ (Β·, 0)) := by ext x <;> simp [Ξ¦] + rw [hC, hΞ¦] + exact hfprop.prodMap hgprop + rw [IsImmersionAtOfComplement_def] + exact LiftSourceTargetPropertyAt.prodMap hf.property hg.property key + /-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`. Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe, @@ -540,6 +602,15 @@ lemma _root_.isOpen_isImmersionAt : fun y hy ↦ hy.isImmersionAt, isOpen_isImmersionAtOfComplement, by simp [hx.isImmersionAtOfComplement_complement]⟩ +/-- If `f: M β†’ N` and `g: M' Γ— N'` are immersions at `x` and `x'`, respectively, +then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ +theorem prodMap {f : M β†’ N} {g : M' β†’ N'} {x' : M'} + [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] + (hf : IsImmersionAt I J n f x) (hg : IsImmersionAt I' J' n g x') : + IsImmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := + hf.isImmersionAtOfComplement_complement.prodMap hg.isImmersionAtOfComplement_complement + |>.isImmersionAt + end IsImmersionAt variable (F I J n) in @@ -592,6 +663,14 @@ lemma congr_F (e : F ≃L[π•œ] F') : IsImmersionOfComplement F I J n f ↔ IsImmersionOfComplement F' I J n f := ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩ +/-- If `f: M β†’ N` and `g: M' Γ— N'` are immersions at `x` and `x'` (w.r.t. `F` and `F'`), +respectively, then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')` w.r.t. `F Γ— F'`. -/ +theorem prodMap {f : M β†’ N} {g : M' β†’ N'} + [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] + (h : IsImmersionOfComplement F I J n f) (h' : IsImmersionOfComplement F' I' J' n g) : + IsImmersionOfComplement (F Γ— F') (I.prod I') (J.prod J') n (Prod.map f g) := + fun ⟨x, x'⟩ ↦ (h x).prodMap (h' x') + /-- If `f` is an immersion w.r.t. some complement `F`, it is an immersion. Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe, @@ -647,6 +726,14 @@ lemma isImmersionAt (h : IsImmersion I J n f) (x : M) : IsImmersionAt I J n f x theorem congr (h : IsImmersion I J n f) (heq : f = g) : IsImmersion I J n g := heq β–Έ h +/-- If `f: M β†’ N` and `g: M' Γ— N'` are immersions at `x` and `x'`, respectively, +then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ +theorem prodMap {f : M β†’ N} {g : M' β†’ N'} + [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] + (hf : IsImmersion I J n f) (hg : IsImmersion I' J' n g) : + IsImmersion (I.prod I') (J.prod J') n (Prod.map f g) := + (hf.isImmersionOfComplement_complement.prodMap hg.isImmersionOfComplement_complement ).isImmersion + end IsImmersion end Manifold From 717b58ea7af0b4f8ce47dbcc2b5a3a18338bdb9c Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 28 Nov 2025 22:58:27 +0100 Subject: [PATCH 06/38] Deduce from a local properties lemma --- Mathlib/Geometry/Manifold/Immersion.lean | 14 ++------------ .../Manifold/LocalSourceTargetProperty.lean | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 32e2ab13b76f07..8909d01d779362 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -360,18 +360,8 @@ lemma congr_F (e : F ≃L[π•œ] F') : /- The set of points where `IsImmersionAtOfComplement` holds is open. -/ lemma _root_.isOpen_isImmersionAtOfComplement : IsOpen {x | IsImmersionAtOfComplement F I J n f x} := by - rw [isOpen_iff_forall_mem_open] - intro x hx - -- Suppose `f` is an immersion at `x`: choose slice charts Ο† near x and ψ near f x s.t. - -- `f` looks like `u ↦ (u, 0)` in these charts. Then the same charts witness that `f` is an - -- immersion at any `y ∈ Ο†.source`. - simp only [mem_setOf_eq, IsImmersionAtOfComplement_def] at hx - refine ⟨hx.domChart.source, ?_, hx.domChart.open_source, hx.mem_domChart_source⟩ - intro x' hx' - rw [mem_setOf_eq, IsImmersionAtOfComplement_def] - exact ⟨hx.domChart, hx.codChart, hx', hx.source_subset_preimage_source hx', - hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source, - hx.property⟩ + simp_rw [IsImmersionAtOfComplement_def] + exact isOpen_liftSourceTargetPropertyAt /-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`. diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 6a666eb7f58b01..c0811bddca28ce 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -33,6 +33,8 @@ local property of this form. `f` has this property at `x` if there exist charts `Ο†` and `ψ` such that `P f Ο† ψ` holds. * `Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq`: if `f` has property `P` at `x` and `g` equals `f` near `x`, then `g` also has property `P` at `x`. +* `isOpen_liftSourceTargetPropertyAt`: the set of points at which `LiftSourceTargetPropertyAt` + holds is open -/ @@ -194,6 +196,19 @@ lemma congr_iff_of_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f = LiftSourceTargetPropertyAt I I' n f x P ↔ LiftSourceTargetPropertyAt I I' n g x P := ⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩ +/- The set of points where `LiftSourceTargetPropertyAt` holds is open. -/ +lemma _root_.isOpen_liftSourceTargetPropertyAt : + IsOpen {x | LiftSourceTargetPropertyAt I I' n g x P} := by + rw [isOpen_iff_forall_mem_open] + intro x hx + -- Suppose the lifted property `P` holds at `x`: + -- choose slice charts `Ο†` near `x` and `ψ` near `f x` s.t. `P f Ο† ψ` holds. + -- Then the same charts witness that `P f Ο† ψ` holds at any `y ∈ Ο†.source`. + refine ⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩ + exact ⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy, + hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source, + hx.property⟩ + end LiftSourceTargetPropertyAt end Manifold From b8f71f4483b67044c282a03da507f95bc622df75 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:35:12 +0100 Subject: [PATCH 07/38] Preliminary lemmas --- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 0bbf03512bf312..6419c6293ae1f5 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -944,6 +944,24 @@ theorem contDiffWithinAt_snd {s : Set (E Γ— F)} {p : E Γ— F} : ContDiffWithinAt π•œ n (Prod.snd : E Γ— F β†’ F) s p := contDiff_snd.contDiffWithinAt +-- If there is a need, add `contDiffWithinAt_prod_iff`; this will require +-- `ContMDiffWithinAt.{fst,snd}`. + +theorem contDiffAt_prod_iff (f : E β†’ F Γ— G) : + ContDiffAt π•œ n f x ↔ + ContDiffAt π•œ n (Prod.fst ∘ f) x ∧ ContDiffAt π•œ n (Prod.snd ∘ f) x := + ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩ + +theorem contDiffOn_prod_iff (f : E β†’ F Γ— G) : + ContDiffOn π•œ n f s ↔ + ContDiffOn π•œ n (Prod.fst ∘ f) s ∧ ContDiffOn π•œ n (Prod.snd ∘ f) s := + ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩ + +theorem contDiff_prod_iff (f : E β†’ F Γ— G) : + ContDiff π•œ n f ↔ + ContDiff π•œ n (Prod.fst ∘ f) ∧ ContDiff π•œ n (Prod.snd ∘ f) := + ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩ + section NAry variable {E₁ Eβ‚‚ E₃ : Type*} From 417f6cc6d3eeea5ac842e2c0c2c764bab3da6592 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:36:24 +0100 Subject: [PATCH 08/38] chore: generalise contMDiffOn_extChartAt --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index d7a1af646a5e55..18cffd6d4851ae 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -89,8 +89,12 @@ theorem contMDiffAt_extChartAt : ContMDiffAt I π“˜(π•œ, E) n (extChartAt I x) filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy exact PartialEquiv.right_inv (extChartAt I x) hy +theorem contMDiffOn_extend (he : e ∈ maximalAtlas I n M) : + ContMDiffOn I π“˜(π•œ, E) n (e.extend I) e.source := + contMDiffOn_extend (chart_mem_maximalAtlas x) + theorem contMDiffOn_extChartAt : ContMDiffOn I π“˜(π•œ, E) n (extChartAt I x) (chartAt H x).source := - fun _x' hx' => (contMDiffAt_extChartAt' hx').contMDiffWithinAt + contMDiffOn_extend (chart_mem_maximalAtlas x) theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) : ContMDiffOn π“˜(π•œ, E) I n (e.extend I).symm (I '' e.target) := by From d91581ba97b68b2248f1601941d7712fad6cb0e5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:37:47 +0100 Subject: [PATCH 09/38] key lemma about atlasses: TODO finish generalising the proof! --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 18cffd6d4851ae..c9cb895b12b311 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -293,3 +293,104 @@ theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : OpenPartialHomeomorph M Β· simp only [c, c', hx', mfld_simps] end IsLocalStructomorph + +open Set Filter Function + +variable {π•œ : Type*} [NontriviallyNormedField π•œ] + {E F : Type*} [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedAddCommGroup F] [NormedSpace π•œ F] + {H G : Type*} [TopologicalSpace H] [TopologicalSpace G] + {I : ModelWithCorners π•œ E H} {J : ModelWithCorners π•œ F G} + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] + {N : Type*} [TopologicalSpace N] [ChartedSpace G N] + {n : WithTop β„•βˆž} + [IsManifold I n M] [IsManifold J n N] {f : M β†’ N} {s : Set M} + {Ο† : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} + +-- there is no definition `writtenInExtend` but we already use some made-up names in this file + +/- The following proof is a warm-up for the real case; it should contain the main idea. +-- TODO: complete the proof, and refactor the proof +-- to prove ContMDiffWithinAt and ContMDiffAt versions first. +-- More bare hands proof, but actually clearer. -/ +theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) + (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : + ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ + ContMDiffOn I J n f s := by + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + Β· set f' := (ψ.extend J) ∘ f ∘ (Ο†.extend I).symm + have eq1 : EqOn (f' ∘ Ο†.extend I) (ψ.extend J ∘ f) s := by + have : (f' ∘ Ο†.extend I) = (ψ.extend J ∘ f) ∘ ((Ο†.extend I).symm ∘ (Ο†.extend I)) := by + simp only [f', Function.comp_assoc] + intro x hx + rw [this, Function.comp_apply] + congr + simp only [comp_apply] + apply Ο†.extend_left_inv (hs hx) + have : ContMDiffOn I π“˜(π•œ, F) n (f' ∘ (Ο†.extend I)) s := by + apply h.comp ((contMDiffOn_extend hΟ†).mono hs) + exact subset_preimage_image (↑(Ο†.extend I)) s + have : ContMDiffOn I J n ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := by + apply ContMDiffOn.comp (t := (ψ.extend J).target) ?_ this ?_ + Β· rw [ψ.extend_target'] + exact contMDiffOn_extend_symm hψ + Β· refine image_subset_iff.mp ?_ + rintro x ⟨x', hx's, rfl⟩ + rw [eq1 hx's, ψ.extend_target_eq_image_source] + exact mem_image_of_mem (ψ.extend J) (hmaps hx's) + have eq2 : EqOn ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) f s := by + intro x hx + rw [Function.comp_apply, eq1 hx, Function.comp_apply] + exact PartialEquiv.left_inv _ (by simpa using hmaps hx) + exact this.congr eq2.symm + Β· -- Easy direction: extended charts and their inverse is smooth on their source, + -- so composing with them preserves smoothness. + have : (Ο†.extend I) '' s βŠ† ↑I '' Ο†.target := by + rw [Ο†.extend_coe, ← Ο†.image_source_eq_target, image_comp]; gcongr + have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by + rintro x ⟨x', hx', rfl⟩ + rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] + have := ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux + apply this.mono le_rfl + +#exit + +/-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ +theorem contMDiffWithinAt_writtenInExtend_iff {y : M} + (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) + (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) : + ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) + ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by + refine ⟨?_, ?_⟩ + Β· intro h + sorry + Β· intro h + have h1 := contMDiffOn_extend_symm hψ + --have h1' := h1 (ψ (f y)) hgy + have h2 := contMDiffAt_extend hΟ† hy (I := I) (n := n) + --have aux2 := h.comp y h1 (t := Set.univ) + -- apply (h1'.comp _ h).comp _ aux2 does it, morally + sorry + +theorem contMDiffAt_writtenInExtend_iff {y : M} + (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) + (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) : + ContMDiffAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) + (Ο†.extend I y) ↔ ContMDiffAt I J n f y := by + sorry /- TODO: can this be deduced from the withinAt version? + nth_rw 2 [← contMDiffWithinAt_univ] + rw [← contMDiffWithinAt_writtenInExtend_iff hΟ† hψ hy hgy] + simp only [preimage_univ, univ_inter] -- two goals left, which might be unprovable -/ + +/-- If `s βŠ† Ο†.source` and `f x ∈ ψ.source` whenever `x ∈ s`, then `f` is `C^n` on `s` if and +only if `f` written in charts `Ο†.extend I` and `ψ.extend I'` is `C^n` on `Ο†.extend I '' s`. +This is a smooth analogue of `continuousOn_writtenInExtend_iff`. -/ +theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) + (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : + ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ + ContMDiffOn I J n f s := by + refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ + refine (contMDiffWithinAt_congr_set ?_).trans + (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hmaps) + rw [← nhdsWithin_eq_iff_eventuallyEq, ← Ο†.map_extend_nhdsWithin_eq_image_of_subset, + ← Ο†.map_extend_nhdsWithin] + exacts [hs hx, hs hx, hs] From b8548707d9c6d65dbdfdac9442461aefd7bc8fad Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:39:35 +0100 Subject: [PATCH 10/38] One more preliminary lemma, and add to overview --- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean | 3 +++ docs/overview.yaml | 1 + 2 files changed, 4 insertions(+) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 37a04b2aed1b8c..81c99a25e3df30 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -84,6 +84,9 @@ theorem extend_target : (f.extend I).target = I.symm ⁻¹' f.target ∩ range I theorem extend_target' : (f.extend I).target = I '' f.target := by rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe] +theorem extend_target_eq_image_source : (f.extend I).target = (f.extend I) '' f.source := by + rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe] + lemma isOpen_extend_target [I.Boundaryless] : IsOpen (f.extend I).target := by rw [extend_target, I.range_eq_univ, inter_univ] exact I.continuous_symm.isOpen_preimage _ f.open_target diff --git a/docs/overview.yaml b/docs/overview.yaml index 24312cfd59a3ef..a6d621e101a050 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -424,6 +424,7 @@ Geometry: Differentiable manifolds: smooth or analytic manifold (with boundary and corners): 'IsManifold' smooth map between manifolds: 'ContMDiff' + smooth immersion: 'IsImmersion' product of manifolds: 'IsManifold.prod' disjoint union of manifolds: 'IsManifold.disjointUnion' interior of a manifold: 'ModelWithCorners.interior' From 34844a169a737fc576d8fa2d5be97e77c2501ed5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:41:20 +0100 Subject: [PATCH 11/38] fixup refactor --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index c9cb895b12b311..72eb9e81481c55 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -91,7 +91,7 @@ theorem contMDiffAt_extChartAt : ContMDiffAt I π“˜(π•œ, E) n (extChartAt I x) theorem contMDiffOn_extend (he : e ∈ maximalAtlas I n M) : ContMDiffOn I π“˜(π•œ, E) n (e.extend I) e.source := - contMDiffOn_extend (chart_mem_maximalAtlas x) + fun _x' hx' ↦ (contMDiffAt_extend he hx').contMDiffWithinAt theorem contMDiffOn_extChartAt : ContMDiffOn I π“˜(π•œ, E) n (extChartAt I x) (chartAt H x).source := contMDiffOn_extend (chart_mem_maximalAtlas x) From 75cfe739e3bdf4aa90e560abe3cc471a73257d2e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:42:18 +0100 Subject: [PATCH 12/38] fix merge with isOpen lemma --- Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index dd26606c9681b1..4b9be721d4101f 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -207,7 +207,7 @@ lemma congr_iff_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f =αΆ [n /- The set of points where `LiftSourceTargetPropertyAt` holds is open. -/ lemma _root_.isOpen_liftSourceTargetPropertyAt : - IsOpen {x | LiftSourceTargetPropertyAt I I' n g x P} := by + IsOpen {x | LiftSourceTargetPropertyAt I J n g x P} := by rw [isOpen_iff_forall_mem_open] intro x hx -- Suppose the lifted property `P` holds at `x`: From 810ae9cf1265d2df5d33562bd029957f2960def3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:44:49 +0100 Subject: [PATCH 13/38] feat: smoothness of IsImmersionAtOfComplement --- Mathlib/Geometry/Manifold/Immersion.lean | 41 ++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index a4bd3d61c317c7..3360913b1ca317 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -5,6 +5,8 @@ Authors: Michael Rothgang -/ module +public import Mathlib.Geometry.Manifold.ContMDiff.Atlas +public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt public import Mathlib.Geometry.Manifold.LocalSourceTargetProperty public import Mathlib.Analysis.Normed.Operator.Banach @@ -437,6 +439,45 @@ lemma isImmersionAt (h : IsImmersionAtOfComplement F I J n f x) : use h.smallComplement, by infer_instance, by infer_instance exact (IsImmersionAtOfComplement.congr_F h.smallEquiv).mp h +/-- This lemma is marked private since `h.domChart` is an arbitrary representative: +`continuousAt` is part of the public API -/ +private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : + ContinuousOn f h.domChart.source := by + have mapsto : MapsTo f h.domChart.source h.codChart.source := + fun x hx ↦ h.source_subset_preimage_source hx + rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl mapsto (I' := J) (I := I), + ← h.domChart.extend_target_eq_image_source] + have : ContinuousOn (h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target := by fun_prop + exact this.congr h.writtenInCharts + +/-- A `C^k` immersion at `x` is continuous at `x`. -/ +theorem continuousAt (h : IsImmersionAtOfComplement F I J n f x) : ContinuousAt f x := + h.continuousOn.continuousAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) + +variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] + +/-- This lemma is marked private since `h.domChart` is an arbitrary representative: +`contMDiffAt` is part of the public API -/ +private theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : + ContMDiffOn I J n f h.domChart.source := by + have mapsto : MapsTo f h.domChart.source h.codChart.source := + fun x hx ↦ h.source_subset_preimage_source hx + rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas + h.codChart_mem_maximalAtlas le_rfl mapsto, + ← h.domChart.extend_target_eq_image_source] + have : ContMDiff π“˜(π•œ, E) π“˜(π•œ, E'') n (h.equiv ∘ fun x ↦ (x, 0)) := by + have : ContMDiff (π“˜(π•œ, E Γ— F)) π“˜(π•œ, E'') n h.equiv := by + rw [contMDiff_iff_contDiff] + exact h.equiv.contDiff + apply this.comp + rw [contMDiff_iff_contDiff, contDiff_prod_iff] + exact ⟨contDiff_id, contDiff_const (c := (0 : F))⟩ + exact this.contMDiffOn.congr h.writtenInCharts + +/-- A `C^k` immersion at `x` is `C^k` at `x`. -/ +theorem contMDiffAt (h : IsImmersionAtOfComplement F I J n f x) : ContMDiffAt I J n f x := + h.contMDiffOn.contMDiffAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) + end IsImmersionAtOfComplement namespace IsImmersionAt From 858f8bb422807dd0b369929d1ce9efb64a9855fc Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 00:50:54 +0100 Subject: [PATCH 14/38] Remaining ones --- Mathlib/Geometry/Manifold/Immersion.lean | 36 ++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 3360913b1ca317..d0ebc829ad8fa2 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -51,6 +51,8 @@ This shortens the overall argument, as the definition of submersions has the sam the set of points where `IsImmersionAt(OfComplement)` holds is open. * `IsImmersionAt.prodMap` and `IsImmersion.prodMap`: the product of two immersions (at a point) is an immersion (at a point). +* `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. +* `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`. ## Implementation notes @@ -70,8 +72,6 @@ This shortens the overall argument, as the definition of submersions has the sam ## TODO * The converse to `IsImmersionAtOfComplement.congr_F` also holds: any two complements are isomorphic, as they are isomorphic to the cokernel of the differential `mfderiv I J f x`. -* `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. -* `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`. * If `f` is an immersion at `x`, its differential splits, hence is injective. * If `f : M β†’ N` is a map between Banach manifolds, `mfderiv I J f x` splitting implies `f` is an immersion at `x`. (This requires the inverse function theorem.) @@ -642,6 +642,28 @@ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} {x' : M'} hf.isImmersionAtOfComplement_complement.prodMap hg.isImmersionAtOfComplement_complement |>.isImmersionAt +/-- This lemma is marked private since `h.domChart` is an arbitrary representative: +`continuousAt` is part of the public API -/ +private theorem continuousOn (h : IsImmersionAt I J n f x) : + ContinuousOn f h.domChart.source := + h.isImmersionAtOfComplement_complement.continuousOn + +/-- A `C^k` immersion at `x` is continuous at `x`. -/ +theorem continuousAt (h : IsImmersionAt I J n f x) : ContinuousAt f x := + h.isImmersionAtOfComplement_complement.continuousAt + +variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] + +/-- This lemma is marked private since `h.domChart` is an arbitrary representative: +`contMDiffAt` is part of the public API -/ +private theorem contMDiffOn (h : IsImmersionAt I J n f x) : + ContMDiffOn I J n f h.domChart.source := + h.isImmersionAtOfComplement_complement.contMDiffOn + +/-- A `C^k` immersion at `x` is `C^k` at `x`. -/ +theorem contMDiffAt (h : IsImmersionAt I J n f x) : ContMDiffAt I J n f x := + h.isImmersionAtOfComplement_complement.contMDiffAt + end IsImmersionAt variable (F I J n) in @@ -718,6 +740,11 @@ lemma isImmersion (h : IsImmersionOfComplement F I J n f) : IsImmersion I J n f use (h x).smallComplement, by infer_instance, by infer_instance exact (IsImmersionOfComplement.congr_F (h x).smallEquiv).mp h +/-- A `C^k` immersion is `C^k` -/ +theorem contMDiff [IsManifold I n M] [IsManifold J n N] + (h : IsImmersionOfComplement F I J n f) : ContMDiff I J n f := + fun x ↦ (h x).contMDiffAt + end IsImmersionOfComplement namespace IsImmersion @@ -765,6 +792,11 @@ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} IsImmersion (I.prod I') (J.prod J') n (Prod.map f g) := (hf.isImmersionOfComplement_complement.prodMap hg.isImmersionOfComplement_complement ).isImmersion +/-- A `C^k` immersion is `C^k` -/ +theorem contMDiff [IsManifold I n M] [IsManifold J n N] + (h : IsImmersion I J n f) : ContMDiff I J n f := + h.isImmersionOfComplement_complement.contMDiff + end IsImmersion end Manifold From f6a127187880f597d99d9a3b8b6578e278e019de Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 10:14:45 +0100 Subject: [PATCH 15/38] Golf proof a bit --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 72eb9e81481c55..1c8347f2a805ba 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -322,13 +322,9 @@ theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : have : (f' ∘ Ο†.extend I) = (ψ.extend J ∘ f) ∘ ((Ο†.extend I).symm ∘ (Ο†.extend I)) := by simp only [f', Function.comp_assoc] intro x hx - rw [this, Function.comp_apply] - congr - simp only [comp_apply] - apply Ο†.extend_left_inv (hs hx) - have : ContMDiffOn I π“˜(π•œ, F) n (f' ∘ (Ο†.extend I)) s := by - apply h.comp ((contMDiffOn_extend hΟ†).mono hs) - exact subset_preimage_image (↑(Ο†.extend I)) s + simp_rw [this, comp_apply, Ο†.extend_left_inv (hs hx)] + have : ContMDiffOn I π“˜(π•œ, F) n (f' ∘ (Ο†.extend I)) s := + h.comp ((contMDiffOn_extend hΟ†).mono hs) <| subset_preimage_image (↑(Ο†.extend I)) s have : ContMDiffOn I J n ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := by apply ContMDiffOn.comp (t := (ψ.extend J).target) ?_ this ?_ Β· rw [ψ.extend_target'] @@ -349,10 +345,7 @@ theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by rintro x ⟨x', hx', rfl⟩ rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] - have := ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux - apply this.mono le_rfl - -#exit + exact ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux /-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} From e24087ec1979b8ce437cb2321b0258b8ae47b620 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 29 Nov 2025 10:46:42 +0100 Subject: [PATCH 16/38] small progress on generalising --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 38 +++++++++++++++---- 1 file changed, 30 insertions(+), 8 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 1c8347f2a805ba..5c6789ac873033 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -345,23 +345,44 @@ theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by rintro x ⟨x', hx', rfl⟩ rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] + -- + have h1 := (contMDiffOn_extend hψ).comp h hmaps + have h2 := (contMDiffOn_extend_symm hΟ†).mono this exact ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux /-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) - (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) : + (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by - refine ⟨?_, ?_⟩ - Β· intro h - sorry - Β· intro h - have h1 := contMDiffOn_extend_symm hψ + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + Β· sorry + Β· have h1 := contMDiffOn_extend_symm hψ --have h1' := h1 (ψ (f y)) hgy have h2 := contMDiffAt_extend hΟ† hy (I := I) (n := n) --have aux2 := h.comp y h1 (t := Set.univ) -- apply (h1'.comp _ h).comp _ aux2 does it, morally + + have : (Ο†.extend I) '' s βŠ† I '' Ο†.target := by + rw [Ο†.extend_coe, ← Ο†.image_source_eq_target, image_comp]; gcongr -- seems to need hs! + -- TODO: don't need this for the actual proofs below; remove once done! + have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by + rintro x ⟨x', hx', rfl⟩ + rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] + + have h0 := contMDiffOn_extend hψ|>.contMDiffAt (ψ.open_source.mem_nhds hgy) + have h1 : ContMDiffWithinAt I π“˜(π•œ, F) n ((ψ.extend J) ∘ f) s y := + h0.contMDiffWithinAt.comp _ h (mapsTo_image f s) + + have h2' := (contMDiffOn_extend_symm hΟ†).mono this + have h2 : ContMDiffWithinAt π“˜(π•œ, E) I + n ((Ο†.extend I).symm) ((Ο†.extend I) '' s) ((Ο†.extend I) y) := by + apply h2' ((Ο†.extend I) y) + apply mem_image_of_mem + sorry -- need a stronger lemma on extend's differentiability here! + clear h0 h2' + --have aux := ContMDiffWithinAt.comp (Ο†.extend I y) h2--1 --_ h2 aux sorry theorem contMDiffAt_writtenInExtend_iff {y : M} @@ -377,13 +398,14 @@ theorem contMDiffAt_writtenInExtend_iff {y : M} /-- If `s βŠ† Ο†.source` and `f x ∈ ψ.source` whenever `x ∈ s`, then `f` is `C^n` on `s` if and only if `f` written in charts `Ο†.extend I` and `ψ.extend I'` is `C^n` on `Ο†.extend I '' s`. This is a smooth analogue of `continuousOn_writtenInExtend_iff`. -/ -theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) +-- same result, but a shorter, golfed proof +theorem contMDiffOn_writtenInExtend_iff' (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ ContMDiffOn I J n f s := by refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ refine (contMDiffWithinAt_congr_set ?_).trans - (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hmaps) + (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) sorry hmaps) rw [← nhdsWithin_eq_iff_eventuallyEq, ← Ο†.map_extend_nhdsWithin_eq_image_of_subset, ← Ο†.map_extend_nhdsWithin] exacts [hs hx, hs hx, hs] From 4127f8a7f7e575d88c6c874fc7d6dab593a6e839 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 10 Dec 2025 10:15:19 +0100 Subject: [PATCH 17/38] Remove sorried part --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 67 +------------------ 1 file changed, 2 insertions(+), 65 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 5c6789ac873033..e1f68d539f2a65 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -308,10 +308,8 @@ variable {π•œ : Type*} [NontriviallyNormedField π•œ] -- there is no definition `writtenInExtend` but we already use some made-up names in this file -/- The following proof is a warm-up for the real case; it should contain the main idea. --- TODO: complete the proof, and refactor the proof --- to prove ContMDiffWithinAt and ContMDiffAt versions first. --- More bare hands proof, but actually clearer. -/ +-- TODO: prove the analogous statement for `ContMDiffWithinAt`, and deduce a `ContMDiffAt` version +-- and this statement from it theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ @@ -345,67 +343,6 @@ theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by rintro x ⟨x', hx', rfl⟩ rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] - -- have h1 := (contMDiffOn_extend hψ).comp h hmaps have h2 := (contMDiffOn_extend_symm hΟ†).mono this exact ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux - -/-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ -theorem contMDiffWithinAt_writtenInExtend_iff {y : M} - (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) - (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : - ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) - ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - Β· sorry - Β· have h1 := contMDiffOn_extend_symm hψ - --have h1' := h1 (ψ (f y)) hgy - have h2 := contMDiffAt_extend hΟ† hy (I := I) (n := n) - --have aux2 := h.comp y h1 (t := Set.univ) - -- apply (h1'.comp _ h).comp _ aux2 does it, morally - - have : (Ο†.extend I) '' s βŠ† I '' Ο†.target := by - rw [Ο†.extend_coe, ← Ο†.image_source_eq_target, image_comp]; gcongr -- seems to need hs! - -- TODO: don't need this for the actual proofs below; remove once done! - have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by - rintro x ⟨x', hx', rfl⟩ - rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] - - have h0 := contMDiffOn_extend hψ|>.contMDiffAt (ψ.open_source.mem_nhds hgy) - have h1 : ContMDiffWithinAt I π“˜(π•œ, F) n ((ψ.extend J) ∘ f) s y := - h0.contMDiffWithinAt.comp _ h (mapsTo_image f s) - - have h2' := (contMDiffOn_extend_symm hΟ†).mono this - have h2 : ContMDiffWithinAt π“˜(π•œ, E) I - n ((Ο†.extend I).symm) ((Ο†.extend I) '' s) ((Ο†.extend I) y) := by - apply h2' ((Ο†.extend I) y) - apply mem_image_of_mem - sorry -- need a stronger lemma on extend's differentiability here! - clear h0 h2' - --have aux := ContMDiffWithinAt.comp (Ο†.extend I y) h2--1 --_ h2 aux - sorry - -theorem contMDiffAt_writtenInExtend_iff {y : M} - (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) - (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) : - ContMDiffAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) - (Ο†.extend I y) ↔ ContMDiffAt I J n f y := by - sorry /- TODO: can this be deduced from the withinAt version? - nth_rw 2 [← contMDiffWithinAt_univ] - rw [← contMDiffWithinAt_writtenInExtend_iff hΟ† hψ hy hgy] - simp only [preimage_univ, univ_inter] -- two goals left, which might be unprovable -/ - -/-- If `s βŠ† Ο†.source` and `f x ∈ ψ.source` whenever `x ∈ s`, then `f` is `C^n` on `s` if and -only if `f` written in charts `Ο†.extend I` and `ψ.extend I'` is `C^n` on `Ο†.extend I '' s`. -This is a smooth analogue of `continuousOn_writtenInExtend_iff`. -/ --- same result, but a shorter, golfed proof -theorem contMDiffOn_writtenInExtend_iff' (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) - (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : - ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ - ContMDiffOn I J n f s := by - refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ - refine (contMDiffWithinAt_congr_set ?_).trans - (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) sorry hmaps) - rw [← nhdsWithin_eq_iff_eventuallyEq, ← Ο†.map_extend_nhdsWithin_eq_image_of_subset, - ← Ο†.map_extend_nhdsWithin] - exacts [hs hx, hs hx, hs] From 95f734c1c7ce826c428c5fa90a4690df92b5a4f5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 10 Dec 2025 14:57:23 +0100 Subject: [PATCH 18/38] Add contMDiffWithinAt_prod_iff --- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 5fe21854491488..58df4f88c280d7 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -893,6 +893,12 @@ theorem contDiffWithinAt_fst {s : Set (E Γ— F)} {p : E Γ— F} : ContDiffWithinAt π•œ n (Prod.fst : E Γ— F β†’ E) s p := contDiff_fst.contDiffWithinAt +/-- Postcomposing `f` with `Prod.fst` is `C^n` at `x` -/ +@[fun_prop] +theorem ContDiffWithinAt.fst {f : E β†’ F Γ— G} {x : E} (hf : ContDiffWithinAt π•œ n f s x) : + ContDiffWithinAt π•œ n (fun x => (f x).1) (s) x := + contDiffWithinAt_fst.comp x hf (mapsTo_image f s) + /-- The second projection in a product is `C^∞`. -/ @[fun_prop] theorem contDiff_snd : ContDiff π•œ n (Prod.snd : E Γ— F β†’ F) := @@ -917,11 +923,23 @@ theorem ContDiffOn.snd {f : E β†’ F Γ— G} {s : Set E} (hf : ContDiffOn π•œ n f ContDiffOn π•œ n (fun x => (f x).2) s := contDiff_snd.comp_contDiffOn hf +/-- The second projection at a point in a product is `C^∞`. -/ +@[fun_prop] +theorem contDiffWithinAt_snd {s : Set (E Γ— F)} {p : E Γ— F} : + ContDiffWithinAt π•œ n (Prod.snd : E Γ— F β†’ F) s p := + contDiff_snd.contDiffWithinAt + /-- The second projection at a point in a product is `C^∞`. -/ @[fun_prop] theorem contDiffAt_snd {p : E Γ— F} : ContDiffAt π•œ n (Prod.snd : E Γ— F β†’ F) p := contDiff_snd.contDiffAt +/-- Postcomposing `f` with `Prod.snd` is `C^n` at `x` -/ +@[fun_prop] +theorem ContDiffWithinAt.snd {f : E β†’ F Γ— G} {x : E} (hf : ContDiffWithinAt π•œ n f s x) : + ContDiffWithinAt π•œ n (fun x => (f x).2) (s) x := + contDiffWithinAt_snd.comp x hf (mapsTo_image f s) + /-- Postcomposing `f` with `Prod.snd` is `C^n` at `x` -/ @[fun_prop] theorem ContDiffAt.snd {f : E β†’ F Γ— G} {x : E} (hf : ContDiffAt π•œ n f x) : @@ -938,14 +956,10 @@ theorem ContDiffAt.snd'' {f : F β†’ G} {x : E Γ— F} (hf : ContDiffAt π•œ n f x. ContDiffAt π•œ n (fun x : E Γ— F => f x.2) x := hf.comp x contDiffAt_snd -/-- The second projection within a domain at a point in a product is `C^∞`. -/ -@[fun_prop] -theorem contDiffWithinAt_snd {s : Set (E Γ— F)} {p : E Γ— F} : - ContDiffWithinAt π•œ n (Prod.snd : E Γ— F β†’ F) s p := - contDiff_snd.contDiffWithinAt - --- If there is a need, add `contDiffWithinAt_prod_iff`; this will require --- `ContMDiffWithinAt.{fst,snd}`. +theorem contDiffWithinAt_prod_iff (f : E β†’ F Γ— G) : + ContDiffWithinAt π•œ n f s x ↔ + ContDiffWithinAt π•œ n (Prod.fst ∘ f) s x ∧ ContDiffWithinAt π•œ n (Prod.snd ∘ f) s x := + ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩ theorem contDiffAt_prod_iff (f : E β†’ F Γ— G) : ContDiffAt π•œ n f x ↔ From 6998a9a44ebf88df816a7352c3a6e17baa7e17da Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 10 Dec 2025 17:21:24 +0100 Subject: [PATCH 19/38] Apply suggestions from code review Co-authored-by: Christian Merten --- Mathlib/Geometry/Manifold/Immersion.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 404a59715ee4ae..2f6f540f772bc0 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -693,7 +693,7 @@ lemma isImmersion (h : IsImmersionOfComplement F I J n f) : IsImmersion I J n f use (h x).smallComplement, by infer_instance, by infer_instance exact (IsImmersionOfComplement.congr_F (h x).smallEquiv).mp h -/-- A `C^k` immersion is `C^k` -/ +/-- A `C^k` immersion is `C^k`. -/ theorem contMDiff [IsManifold I n M] [IsManifold J n N] (h : IsImmersionOfComplement F I J n f) : ContMDiff I J n f := fun x ↦ (h x).contMDiffAt @@ -745,7 +745,7 @@ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} IsImmersion (I.prod I') (J.prod J') n (Prod.map f g) := (hf.isImmersionOfComplement_complement.prodMap hg.isImmersionOfComplement_complement ).isImmersion -/-- A `C^k` immersion is `C^k` -/ +/-- A `C^k` immersion is `C^k`. -/ theorem contMDiff [IsManifold I n M] [IsManifold J n N] (h : IsImmersion I J n f) : ContMDiff I J n f := h.isImmersionOfComplement_complement.contMDiff From 9d86918c614f91a85da684173c185d45d99463bd Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 13 Dec 2025 10:37:41 +0100 Subject: [PATCH 20/38] Mapsto lemma --- Mathlib/Geometry/Manifold/Immersion.lean | 12 ++++++++---- .../Manifold/LocalSourceTargetProperty.lean | 14 ++++++++++++-- 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 2f6f540f772bc0..c6819de7b6dac4 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -249,7 +249,12 @@ lemma codChart_mem_maximalAtlas (h : IsImmersionAtOfComplement F I J n f x) : lemma source_subset_preimage_source (h : IsImmersionAtOfComplement F I J n f x) : h.domChart.source βŠ† f ⁻¹' h.codChart.source := by rw [IsImmersionAtOfComplement_def] at h - exact LiftSourceTargetPropertyAt.source_subset_preimage_source h + exact h.source_subset_preimage_source + +lemma mapsto_domChart_source_codChart_source (h : IsImmersionAtOfComplement F I J n f x) : + MapsTo f h.domChart.source h.codChart.source := by + rw [IsImmersionAtOfComplement_def] at h + exact h.source_subset_preimage_source /-- A linear equivalence `E Γ— F ≃L[π•œ] E''` which belongs to the data of an immersion `f` at `x`: the particular equivalence is arbitrary, but this choice matches the witnesses given by @@ -396,9 +401,8 @@ lemma isImmersionAt (h : IsImmersionAtOfComplement F I J n f x) : `continuousAt` is part of the public API -/ private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : ContinuousOn f h.domChart.source := by - have mapsto : MapsTo f h.domChart.source h.codChart.source := - fun x hx ↦ h.source_subset_preimage_source hx - rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl mapsto (I' := J) (I := I), + rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl + h.mapsto_domChart_source_codChart_source (I' := J) (I := I), ← h.domChart.extend_target_eq_image_source] have : ContinuousOn (h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target := by fun_prop exact this.congr h.writtenInCharts diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 3f93bfca736e5f..4b0cb30d6d48a5 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -102,6 +102,17 @@ def LiftSourceTargetPropertyAt (f : M β†’ N) (x : M) (P : (M β†’ N) β†’ OpenPartialHomeomorph M H β†’ OpenPartialHomeomorph N G β†’ Prop) : Prop := Nonempty (LocalPresentationAt I J n f x P) +namespace LocalPresentationAt + +variable {f g : M β†’ N} {x : M} + {P : (M β†’ N) β†’ OpenPartialHomeomorph M H β†’ OpenPartialHomeomorph N G β†’ Prop} + +lemma mapsto_domChart_source_codChart_source (h : LocalPresentationAt I J n f x P) : + MapsTo f h.domChart.source h.codChart.source := + h.source_subset_preimage_source + +end LocalPresentationAt + namespace LiftSourceTargetPropertyAt variable {f g : M β†’ N} {x : M} @@ -142,8 +153,7 @@ lemma codChart_mem_maximalAtlas (h : LiftSourceTargetPropertyAt I J n f x P) : h.codChart ∈ IsManifold.maximalAtlas J n N := h.localPresentationAt.codChart_mem_maximalAtlas -lemma source_subset_preimage_source - (h : LiftSourceTargetPropertyAt I J n f x P) : +lemma source_subset_preimage_source (h : LiftSourceTargetPropertyAt I J n f x P) : h.domChart.source βŠ† f ⁻¹' h.codChart.source := h.localPresentationAt.source_subset_preimage_source From 1b7b2e0bd25bdf0f6a31342f0d63139b7a120a28 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 13 Dec 2025 10:49:31 +0100 Subject: [PATCH 21/38] Try extracting a localPresentationAt lemma --- Mathlib/Geometry/Manifold/Immersion.lean | 10 +++++++++- .../Geometry/Manifold/LocalSourceTargetProperty.lean | 7 +++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index c6819de7b6dac4..a2a82dc37ecb2d 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -401,7 +401,15 @@ lemma isImmersionAt (h : IsImmersionAtOfComplement F I J n f x) : `continuousAt` is part of the public API -/ private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : ContinuousOn f h.domChart.source := by - rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl + have h' := h + rw [IsImmersionAtOfComplement_def] at h' + have aux := h'.localPresentationAt.continuousOn + have : h'.localPresentationAt.domChart = h.domChart := sorry + rw [← this] + apply aux + intro Ο† ψ hf + -- now the actual proof starts... + rw [← hf.domChart.continuousOn_writtenInExtend_iff le_rfl h.mapsto_domChart_source_codChart_source (I' := J) (I := I), ← h.domChart.extend_target_eq_image_source] have : ContinuousOn (h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target := by fun_prop diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 4b0cb30d6d48a5..2a572ecb94ff36 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -111,6 +111,13 @@ lemma mapsto_domChart_source_codChart_source (h : LocalPresentationAt I J n f x MapsTo f h.domChart.source h.codChart.source := h.source_subset_preimage_source +/-- If `f` has local property `P`, then `f` is continuous on `domcChart.source`, +provided the local property is sufficiently nice. -/ +lemma continuousOn (h : LocalPresentationAt I J n f x P) + (hP : βˆ€ {Ο† : OpenPartialHomeomorph M H}, βˆ€ {ψ : OpenPartialHomeomorph N G}, + P f Ο† ψ β†’ ContinuousOn f Ο†.source) : ContinuousOn f h.domChart.source := + hP h.property + end LocalPresentationAt namespace LiftSourceTargetPropertyAt From abbe8bb1fbb7354658eb170ba1aa65aff2a379c8 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 13 Dec 2025 10:49:35 +0100 Subject: [PATCH 22/38] Revert "Try extracting a localPresentationAt lemma" This reverts commit 1b7b2e0bd25bdf0f6a31342f0d63139b7a120a28. --- Mathlib/Geometry/Manifold/Immersion.lean | 10 +--------- .../Geometry/Manifold/LocalSourceTargetProperty.lean | 7 ------- 2 files changed, 1 insertion(+), 16 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index a2a82dc37ecb2d..c6819de7b6dac4 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -401,15 +401,7 @@ lemma isImmersionAt (h : IsImmersionAtOfComplement F I J n f x) : `continuousAt` is part of the public API -/ private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : ContinuousOn f h.domChart.source := by - have h' := h - rw [IsImmersionAtOfComplement_def] at h' - have aux := h'.localPresentationAt.continuousOn - have : h'.localPresentationAt.domChart = h.domChart := sorry - rw [← this] - apply aux - intro Ο† ψ hf - -- now the actual proof starts... - rw [← hf.domChart.continuousOn_writtenInExtend_iff le_rfl + rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl h.mapsto_domChart_source_codChart_source (I' := J) (I := I), ← h.domChart.extend_target_eq_image_source] have : ContinuousOn (h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target := by fun_prop diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean index 2a572ecb94ff36..4b0cb30d6d48a5 100644 --- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean +++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean @@ -111,13 +111,6 @@ lemma mapsto_domChart_source_codChart_source (h : LocalPresentationAt I J n f x MapsTo f h.domChart.source h.codChart.source := h.source_subset_preimage_source -/-- If `f` has local property `P`, then `f` is continuous on `domcChart.source`, -provided the local property is sufficiently nice. -/ -lemma continuousOn (h : LocalPresentationAt I J n f x P) - (hP : βˆ€ {Ο† : OpenPartialHomeomorph M H}, βˆ€ {ψ : OpenPartialHomeomorph N G}, - P f Ο† ψ β†’ ContinuousOn f Ο†.source) : ContinuousOn f h.domChart.source := - hP h.property - end LocalPresentationAt namespace LiftSourceTargetPropertyAt From bade1d807e904ff045794087e20e59a9b522e2c2 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 13 Dec 2025 11:40:42 +0100 Subject: [PATCH 23/38] Fix linter --- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 58df4f88c280d7..8375f75e73fad7 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -1522,3 +1522,5 @@ theorem ContDiff.iterate_deriv' (n : β„•) : | k + 1, _, hf => ContDiff.iterate_deriv' _ k (contDiff_succ_iff_deriv.mp hf).2.2 end deriv + +set_option linter.style.longLine 1700 From ad11c6edec0cb760220bf3502a1a4b11686cd86c Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 13 Dec 2025 12:00:54 +0100 Subject: [PATCH 24/38] fixup --- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 8375f75e73fad7..40e10f3691e199 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -1523,4 +1523,4 @@ theorem ContDiff.iterate_deriv' (n : β„•) : end deriv -set_option linter.style.longLine 1700 +set_option linter.style.longFile 1700 From 38de4293754d42e0058c65096b6c6212efbbd576 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 15 Dec 2025 11:55:43 +0100 Subject: [PATCH 25/38] Update docs/overview.yaml Co-authored-by: Christian Merten --- docs/overview.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index a6d621e101a050..10d1606326225d 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -424,7 +424,7 @@ Geometry: Differentiable manifolds: smooth or analytic manifold (with boundary and corners): 'IsManifold' smooth map between manifolds: 'ContMDiff' - smooth immersion: 'IsImmersion' + smooth immersion: 'Manifold.IsImmersion' product of manifolds: 'IsManifold.prod' disjoint union of manifolds: 'IsManifold.disjointUnion' interior of a manifold: 'ModelWithCorners.interior' From 54228acbf469f869e039d49055af82419993e5bd Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 16 Dec 2025 23:11:47 +0100 Subject: [PATCH 26/38] Smooth embeddings are also smooth --- Mathlib/Geometry/Manifold/SmoothEmbedding.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean index 6d09d1b711fb93..f74a1b2f0ee7a6 100644 --- a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean +++ b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean @@ -22,6 +22,7 @@ This will be useful to define embedded submanifolds. * `IsSmoothEmbedding.id`: the identity map is a smooth embedding * `IsSmoothEmbedding.of_opens`: the inclusion of an open subset `s β†’ M` of a smooth manifold is a smooth embedding +* `IsSmoothEmbedding.contMDiff`: if `f` is a smooth embedding, it is `C^n`. ## Implementation notes @@ -33,7 +34,6 @@ This will be useful to define embedded submanifolds. https://math.stackexchange.com/a/3769328 for counterexamples. ## TODO -* `IsSmoothEmbedding.contMDiff`: if `f` is a smooth embedding, it is `C^n`. * `IsSmoothEmbedding.comp`: the composition of smooth embeddings (between Banach manifolds) is a smooth embedding * `IsLocalDiffeomorph.isSmoothEmbedding`, `Diffeomorph.isSmoothEmbedding`: @@ -75,9 +75,6 @@ namespace IsSmoothEmbedding variable {f g : M β†’ N} --- combine isImmersion with `hf.isImmersion.contMDiff` (once proven) -proof_wanted contMDiff (hf : IsSmoothEmbedding I J n f) : ContMDiff I J n f - protected lemma id [IsManifold I n M] : IsSmoothEmbedding I I n (@id M) := ⟨.id, .id⟩ /-- If `f: M β†’ N` and `g: M' Γ— N'` are smooth embeddings, respectively, @@ -94,6 +91,11 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) : rw [isSmoothEmbedding_iff] exact ⟨IsImmersion.of_opens s, IsEmbedding.subtypeVal⟩ +/-- A smooth embedding is smooth. -/ +lemma contMDiff [IsManifold I n M] [IsManifold J n N] (hf : IsSmoothEmbedding I J n f) : + ContMDiff I J n f := + hf.isImmersion.contMDiff + -- use IsImmersion.comp and IsEmbedding.comp /-- The composition of two smooth embeddings between Banach manifolds is a smooth embedding. -/ proof_wanted comp -- [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F] [CompleteSpace F'] From 9806f61442158c6beee87034281ea8e24ae9f78f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 16 Dec 2025 23:19:47 +0100 Subject: [PATCH 27/38] Add general lemma, due to Winston's AI --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index e1f68d539f2a65..e50b1415a23627 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -308,6 +308,69 @@ variable {π•œ : Type*} [NontriviallyNormedField π•œ] -- there is no definition `writtenInExtend` but we already use some made-up names in this file +/-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ +theorem contMDiffWithinAt_writtenInExtend_iff {y : M} + (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) + (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : + ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) + ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + Β· -- Backward direction: from smoothness in coordinates to smoothness on manifold + -- Strategy: decompose f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) + -- where f' is the coordinate expression + set f' := (ψ.extend J) ∘ f ∘ (Ο†.extend I).symm + -- Use the characterization with the given charts + rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] + refine ⟨?_, ?_⟩ + Β· -- Continuity part + -- Decompose: f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) on s + have eq1 : EqOn (f' ∘ Ο†.extend I) (ψ.extend J ∘ f) s := by + intro x hx + simp only [f', Function.comp_apply] + rw [Ο†.extend_left_inv (hs hx)] + -- Step 1: f' ∘ (Ο†.extend I) is continuous at y within s + have step1 : ContinuousWithinAt (f' ∘ (Ο†.extend I)) s y := by + refine h.continuousWithinAt.comp (((contMDiffOn_extend hΟ†).continuousOn y hy).mono hs) ?_ + intro x hx + constructor + Β· rw [mem_preimage, Ο†.extend_left_inv (hs hx)] + exact hx + Β· exact mem_range_self _ + -- Step 2: (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) is continuous at y within s + have step2 : ContinuousWithinAt ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s y := by + -- TODO: same hold proven three times! + refine ContinuousWithinAt.comp (t := J '' ψ.target) ?_ step1 (fun x hx ↦ ?_) + Β· refine (contMDiffOn_extend_symm hψ).continuousOn ?_ ?_ + all_goals + simp only [Function.comp_apply, f', Ο†.extend_left_inv hy] + exact mem_image_of_mem J (ψ.mapsTo hgy) + Β· simp only [Function.comp_apply, f', Ο†.extend_left_inv (hs hx)] + exact mem_image_of_mem J (ψ.mapsTo (hmaps hx)) + -- Step 3: this equals f on s + have eq2 : EqOn f ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := by + intro x hx + simp only [Function.comp_apply, f'] + rw [Ο†.extend_left_inv (hs hx), ψ.extend_left_inv (hmaps hx)] + -- Also need the equality at y + have eq_at_y : f y = ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) y := by + simp only [Function.comp_apply, f'] + rw [Ο†.extend_left_inv hy, ψ.extend_left_inv hgy] + exact step2.congr_of_eventuallyEq (eventually_nhdsWithin_of_forall eq2) eq_at_y + Β· -- ContDiffWithinAt part + simp only [ContMDiffWithinAt, liftPropWithinAt_iff', ContDiffWithinAtProp, mfld_simps] at h + exact h.2 + Β· -- Forward direction: from smoothness on manifold to smoothness in coordinates + -- Apply the characterization to h + rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] at h + -- XXX: proof has a code smell! + -- Now h : ContinuousWithinAt f s y ∧ + -- ContDiffWithinAt π•œ n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) + -- ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) + -- For model spaces π“˜(π•œ, E) and π“˜(π•œ, F), ContMDiffWithinAt is equivalent to ContDiffWithinAt + -- We prove this directly by unfolding definitions + simp only [ContMDiffWithinAt, liftPropWithinAt_iff', ContDiffWithinAtProp, mfld_simps] + exact ⟨h.2.continuousWithinAt, h.2⟩ + -- TODO: prove the analogous statement for `ContMDiffWithinAt`, and deduce a `ContMDiffAt` version -- and this statement from it theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) From 6768ca2575e78f826227cdd444921e964195fead Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 16 Dec 2025 23:20:04 +0100 Subject: [PATCH 28/38] Golf AI proof a bit --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index e50b1415a23627..70a6c5ebecf0c9 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -6,6 +6,7 @@ Authors: SΓ©bastien GouΓ«zel, Floris van Doorn module public import Mathlib.Geometry.Manifold.ContMDiff.Basic +import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace /-! ## Smoothness of charts and local structomorphisms @@ -356,20 +357,11 @@ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} simp only [Function.comp_apply, f'] rw [Ο†.extend_left_inv hy, ψ.extend_left_inv hgy] exact step2.congr_of_eventuallyEq (eventually_nhdsWithin_of_forall eq2) eq_at_y - Β· -- ContDiffWithinAt part - simp only [ContMDiffWithinAt, liftPropWithinAt_iff', ContDiffWithinAtProp, mfld_simps] at h - exact h.2 + Β· rwa [← contMDiffWithinAt_iff_contDiffWithinAt] Β· -- Forward direction: from smoothness on manifold to smoothness in coordinates - -- Apply the characterization to h rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] at h - -- XXX: proof has a code smell! - -- Now h : ContinuousWithinAt f s y ∧ - -- ContDiffWithinAt π•œ n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) - -- ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) - -- For model spaces π“˜(π•œ, E) and π“˜(π•œ, F), ContMDiffWithinAt is equivalent to ContDiffWithinAt - -- We prove this directly by unfolding definitions - simp only [ContMDiffWithinAt, liftPropWithinAt_iff', ContDiffWithinAtProp, mfld_simps] - exact ⟨h.2.continuousWithinAt, h.2⟩ + rw [contMDiffWithinAt_iff_contDiffWithinAt] + exact h.2 -- TODO: prove the analogous statement for `ContMDiffWithinAt`, and deduce a `ContMDiffAt` version -- and this statement from it From f8c6f70acb064c6d554c12b95822906657c247f6 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 16 Dec 2025 23:20:42 +0100 Subject: [PATCH 29/38] Golf contMDiffOn proof using it --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 40 +++---------------- 1 file changed, 6 insertions(+), 34 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 70a6c5ebecf0c9..dcab0721ddb0f5 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -363,41 +363,13 @@ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} rw [contMDiffWithinAt_iff_contDiffWithinAt] exact h.2 --- TODO: prove the analogous statement for `ContMDiffWithinAt`, and deduce a `ContMDiffAt` version --- and this statement from it theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ ContMDiffOn I J n f s := by - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - Β· set f' := (ψ.extend J) ∘ f ∘ (Ο†.extend I).symm - have eq1 : EqOn (f' ∘ Ο†.extend I) (ψ.extend J ∘ f) s := by - have : (f' ∘ Ο†.extend I) = (ψ.extend J ∘ f) ∘ ((Ο†.extend I).symm ∘ (Ο†.extend I)) := by - simp only [f', Function.comp_assoc] - intro x hx - simp_rw [this, comp_apply, Ο†.extend_left_inv (hs hx)] - have : ContMDiffOn I π“˜(π•œ, F) n (f' ∘ (Ο†.extend I)) s := - h.comp ((contMDiffOn_extend hΟ†).mono hs) <| subset_preimage_image (↑(Ο†.extend I)) s - have : ContMDiffOn I J n ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := by - apply ContMDiffOn.comp (t := (ψ.extend J).target) ?_ this ?_ - Β· rw [ψ.extend_target'] - exact contMDiffOn_extend_symm hψ - Β· refine image_subset_iff.mp ?_ - rintro x ⟨x', hx's, rfl⟩ - rw [eq1 hx's, ψ.extend_target_eq_image_source] - exact mem_image_of_mem (ψ.extend J) (hmaps hx's) - have eq2 : EqOn ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) f s := by - intro x hx - rw [Function.comp_apply, eq1 hx, Function.comp_apply] - exact PartialEquiv.left_inv _ (by simpa using hmaps hx) - exact this.congr eq2.symm - Β· -- Easy direction: extended charts and their inverse is smooth on their source, - -- so composing with them preserves smoothness. - have : (Ο†.extend I) '' s βŠ† ↑I '' Ο†.target := by - rw [Ο†.extend_coe, ← Ο†.image_source_eq_target, image_comp]; gcongr - have aux : (Ο†.extend I) '' s βŠ† (Ο†.extend I).symm ⁻¹' s := by - rintro x ⟨x', hx', rfl⟩ - rwa [mem_preimage, Ο†.extend_left_inv (hs hx')] - have h1 := (contMDiffOn_extend hψ).comp h hmaps - have h2 := (contMDiffOn_extend_symm hΟ†).mono this - exact ((contMDiffOn_extend hψ).comp h hmaps).comp ((contMDiffOn_extend_symm hΟ†).mono this) aux + refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ + refine (contMDiffWithinAt_congr_set ?_).trans + (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hs hmaps) + rw [← nhdsWithin_eq_iff_eventuallyEq, ← Ο†.map_extend_nhdsWithin_eq_image_of_subset, + ← Ο†.map_extend_nhdsWithin] + exacts [hs hx, hs hx, hs] From 73c762ee94fbe0ed58fd0862474ed85ba4501027 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 18 Dec 2025 17:14:06 +0100 Subject: [PATCH 30/38] chore: golf proof of contMDiffWithinAt_writtenInExtend_iff With an AI attempt as a starting point; cleaned up by me. --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 65 ++++++------------- 1 file changed, 20 insertions(+), 45 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index dcab0721ddb0f5..fa29df88577dbf 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -315,52 +315,27 @@ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - Β· -- Backward direction: from smoothness in coordinates to smoothness on manifold - -- Strategy: decompose f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) - -- where f' is the coordinate expression + rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] + refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩ + Β· -- Decompose `f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)` on `s`, + -- where `f'` is the expression in the charts `Ο†` and `ψ`. set f' := (ψ.extend J) ∘ f ∘ (Ο†.extend I).symm - -- Use the characterization with the given charts - rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] - refine ⟨?_, ?_⟩ - Β· -- Continuity part - -- Decompose: f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) on s - have eq1 : EqOn (f' ∘ Ο†.extend I) (ψ.extend J ∘ f) s := by - intro x hx - simp only [f', Function.comp_apply] - rw [Ο†.extend_left_inv (hs hx)] - -- Step 1: f' ∘ (Ο†.extend I) is continuous at y within s - have step1 : ContinuousWithinAt (f' ∘ (Ο†.extend I)) s y := by - refine h.continuousWithinAt.comp (((contMDiffOn_extend hΟ†).continuousOn y hy).mono hs) ?_ - intro x hx - constructor - Β· rw [mem_preimage, Ο†.extend_left_inv (hs hx)] - exact hx - Β· exact mem_range_self _ - -- Step 2: (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I) is continuous at y within s - have step2 : ContinuousWithinAt ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s y := by - -- TODO: same hold proven three times! - refine ContinuousWithinAt.comp (t := J '' ψ.target) ?_ step1 (fun x hx ↦ ?_) - Β· refine (contMDiffOn_extend_symm hψ).continuousOn ?_ ?_ - all_goals - simp only [Function.comp_apply, f', Ο†.extend_left_inv hy] - exact mem_image_of_mem J (ψ.mapsTo hgy) - Β· simp only [Function.comp_apply, f', Ο†.extend_left_inv (hs hx)] - exact mem_image_of_mem J (ψ.mapsTo (hmaps hx)) - -- Step 3: this equals f on s - have eq2 : EqOn f ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := by - intro x hx - simp only [Function.comp_apply, f'] - rw [Ο†.extend_left_inv (hs hx), ψ.extend_left_inv (hmaps hx)] - -- Also need the equality at y - have eq_at_y : f y = ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) y := by - simp only [Function.comp_apply, f'] - rw [Ο†.extend_left_inv hy, ψ.extend_left_inv hgy] - exact step2.congr_of_eventuallyEq (eventually_nhdsWithin_of_forall eq2) eq_at_y - Β· rwa [← contMDiffWithinAt_iff_contDiffWithinAt] - Β· -- Forward direction: from smoothness on manifold to smoothness in coordinates - rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] at h - rw [contMDiffWithinAt_iff_contDiffWithinAt] + have eq : EqOn f ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := fun x hx ↦ by + simp only [f', comp_apply, Ο†.extend_left_inv (hs hx), ψ.extend_left_inv (hmaps hx)] + have step1 : ContinuousWithinAt (f' ∘ (Ο†.extend I)) s y := + h.continuousWithinAt.comp (((contMDiffOn_extend hΟ†).continuousOn y hy).mono hs) + fun x hx ↦ ⟨by rwa [mem_preimage, Ο†.extend_left_inv (hs hx)], mem_range_self _⟩ + have step2 : ContinuousWithinAt ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s y := by + refine ContinuousWithinAt.comp (t := J '' ψ.target) ?_ step1 ?_ + Β· refine (contMDiffOn_extend_symm hψ).continuousOn ?_ ?_ + all_goals + simp only [f', comp_apply, Ο†.extend_left_inv hy]; exact mem_image_of_mem J (ψ.mapsTo hgy) + Β· intro x hx; simp only [f', comp_apply, Ο†.extend_left_inv (hs hx)] + exact mem_image_of_mem J (ψ.mapsTo (hmaps hx)) + exact step2.congr_of_eventuallyEq (eventually_nhdsWithin_of_forall eq) + (by simp only [f', comp_apply, Ο†.extend_left_inv hy, ψ.extend_left_inv hgy]) + Β· rwa [← contMDiffWithinAt_iff_contDiffWithinAt] + Β· rw [contMDiffWithinAt_iff_contDiffWithinAt] exact h.2 theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) From 8fdfda6ca626b18505c2ef0849c8268f69e081e0 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 18 Dec 2025 17:16:55 +0100 Subject: [PATCH 31/38] Tweak --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index fa29df88577dbf..c4479c602ba321 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -307,9 +307,9 @@ variable {π•œ : Type*} [NontriviallyNormedField π•œ] [IsManifold I n M] [IsManifold J n N] {f : M β†’ N} {s : Set M} {Ο† : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} --- there is no definition `writtenInExtend` but we already use some made-up names in this file +-- There is no definition `writtenInExtend`, but we already use some made-up names in this file. -/-- This is a smooth analogue of `continuousWithinAt_writtenInExtend_iff`. -/ +/-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`. -/ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : From 7a748482981629f4982a7b1acda8f831beed2587 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 18 Dec 2025 17:18:38 +0100 Subject: [PATCH 32/38] Clarify comment --- Mathlib/Geometry/Manifold/Immersion.lean | 3 +-- Mathlib/Geometry/Manifold/SmoothEmbedding.lean | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 77db6176603aeb..75783266425d64 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -55,8 +55,7 @@ This shortens the overall argument, as the definition of submersions has the sam * `IsImmersion.of_opens`: the inclusion of an open subset `s β†’ M` of a smooth manifold is a smooth immersion * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. -* `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`. - +* `IsImmersion.contMDiff`: if f is a `C^n` immersion, it is automatically `C^n`. ## Implementation notes diff --git a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean index f74a1b2f0ee7a6..2ec1f1888579d1 100644 --- a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean +++ b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean @@ -22,7 +22,7 @@ This will be useful to define embedded submanifolds. * `IsSmoothEmbedding.id`: the identity map is a smooth embedding * `IsSmoothEmbedding.of_opens`: the inclusion of an open subset `s β†’ M` of a smooth manifold is a smooth embedding -* `IsSmoothEmbedding.contMDiff`: if `f` is a smooth embedding, it is `C^n`. +* `IsSmoothEmbedding.contMDiff`: if `f` is a `C^n` embedding, it is automatically `C^n`. ## Implementation notes @@ -91,7 +91,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) : rw [isSmoothEmbedding_iff] exact ⟨IsImmersion.of_opens s, IsEmbedding.subtypeVal⟩ -/-- A smooth embedding is smooth. -/ +/-- A smooth embedding is automatically smooth. -/ lemma contMDiff [IsManifold I n M] [IsManifold J n N] (hf : IsSmoothEmbedding I J n f) : ContMDiff I J n f := hf.isImmersion.contMDiff From 6f727511ecf311e8f51e9a56909811a5708d829d Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:10:31 +0100 Subject: [PATCH 33/38] Big golf --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 23 ++++--------------- 1 file changed, 4 insertions(+), 19 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index c4479c602ba321..13276ddab6290d 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -312,28 +312,13 @@ variable {π•œ : Type*} [NontriviallyNormedField π•œ] /-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`. -/ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) - (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : + (hy : y ∈ Ο†.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) : ContMDiffWithinAt π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) ((Ο†.extend I).symm ⁻¹' s ∩ range I) (Ο†.extend I y) ↔ ContMDiffWithinAt I J n f s y := by rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hΟ† hψ hy hgy] refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩ - Β· -- Decompose `f = (ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)` on `s`, - -- where `f'` is the expression in the charts `Ο†` and `ψ`. - set f' := (ψ.extend J) ∘ f ∘ (Ο†.extend I).symm - have eq : EqOn f ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s := fun x hx ↦ by - simp only [f', comp_apply, Ο†.extend_left_inv (hs hx), ψ.extend_left_inv (hmaps hx)] - have step1 : ContinuousWithinAt (f' ∘ (Ο†.extend I)) s y := - h.continuousWithinAt.comp (((contMDiffOn_extend hΟ†).continuousOn y hy).mono hs) - fun x hx ↦ ⟨by rwa [mem_preimage, Ο†.extend_left_inv (hs hx)], mem_range_self _⟩ - have step2 : ContinuousWithinAt ((ψ.extend J).symm ∘ f' ∘ (Ο†.extend I)) s y := by - refine ContinuousWithinAt.comp (t := J '' ψ.target) ?_ step1 ?_ - Β· refine (contMDiffOn_extend_symm hψ).continuousOn ?_ ?_ - all_goals - simp only [f', comp_apply, Ο†.extend_left_inv hy]; exact mem_image_of_mem J (ψ.mapsTo hgy) - Β· intro x hx; simp only [f', comp_apply, Ο†.extend_left_inv (hs hx)] - exact mem_image_of_mem J (ψ.mapsTo (hmaps hx)) - exact step2.congr_of_eventuallyEq (eventually_nhdsWithin_of_forall eq) - (by simp only [f', comp_apply, Ο†.extend_left_inv hy, ψ.extend_left_inv hgy]) + Β· rw [← Ο†.continuousWithinAt_writtenInExtend_iff (I := I) (I' := J) hy hgy hmaps] + exact h.continuousWithinAt Β· rwa [← contMDiffWithinAt_iff_contDiffWithinAt] Β· rw [contMDiffWithinAt_iff_contDiffWithinAt] exact h.2 @@ -344,7 +329,7 @@ theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ContMDiffOn I J n f s := by refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ refine (contMDiffWithinAt_congr_set ?_).trans - (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hs hmaps) + (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hmaps) rw [← nhdsWithin_eq_iff_eventuallyEq, ← Ο†.map_extend_nhdsWithin_eq_image_of_subset, ← Ο†.map_extend_nhdsWithin] exacts [hs hx, hs hx, hs] From 0168bb877071ae7cfaa5b1711807a00ccfcd6a21 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:13:47 +0100 Subject: [PATCH 34/38] Apply suggestions from code review Co-authored-by: Christian Merten --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 2 +- Mathlib/Geometry/Manifold/Immersion.lean | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 13276ddab6290d..a4217bf154d5d0 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -326,7 +326,7 @@ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} theorem contMDiffOn_writtenInExtend_iff (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) (hs : s βŠ† Ο†.source) (hmaps : MapsTo f s ψ.source) : ContMDiffOn π“˜(π•œ, E) π“˜(π•œ, F) n (ψ.extend J ∘ f ∘ (Ο†.extend I).symm) (Ο†.extend I '' s) ↔ - ContMDiffOn I J n f s := by + ContMDiffOn I J n f s := by refine forall_mem_image.trans <| forallβ‚‚_congr fun x hx ↦ ?_ refine (contMDiffWithinAt_congr_set ?_).trans (contMDiffWithinAt_writtenInExtend_iff hΟ† hψ (hs hx) (hmaps hx) hmaps) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 75783266425d64..104db0821abc9b 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -437,10 +437,8 @@ variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] `contMDiffAt` is part of the public API -/ private theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : ContMDiffOn I J n f h.domChart.source := by - have mapsto : MapsTo f h.domChart.source h.codChart.source := - fun x hx ↦ h.source_subset_preimage_source hx rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas - h.codChart_mem_maximalAtlas le_rfl mapsto, + h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source, ← h.domChart.extend_target_eq_image_source] have : ContMDiff π“˜(π•œ, E) π“˜(π•œ, E'') n (h.equiv ∘ fun x ↦ (x, 0)) := by have : ContMDiff (π“˜(π•œ, E Γ— F)) π“˜(π•œ, E'') n h.equiv := by @@ -803,7 +801,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) : IsImmersion I I n (Subtype.val : s β†’ M) := ⟨PUnit, by infer_instance, by infer_instance, IsImmersionOfComplement.of_opens s⟩ -/-- A `C^k` immersion is `C^k`. -/ +/-- A `C^n` immersion is `C^n`. -/ theorem contMDiff [IsManifold I n M] [IsManifold J n N] (h : IsImmersion I J n f) : ContMDiff I J n f := h.isImmersionOfComplement_complement.contMDiff From 77583c9ece94be9a33084bf278fdfa7cb8feb777 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:19:50 +0100 Subject: [PATCH 35/38] More review comments --- Mathlib/Geometry/Manifold/Immersion.lean | 34 ++++++++----------- .../Geometry/Manifold/SmoothEmbedding.lean | 7 ++-- 2 files changed, 19 insertions(+), 22 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 104db0821abc9b..1435ca73dd7038 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -55,7 +55,8 @@ This shortens the overall argument, as the definition of submersions has the sam * `IsImmersion.of_opens`: the inclusion of an open subset `s β†’ M` of a smooth manifold is a smooth immersion * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`. -* `IsImmersion.contMDiff`: if f is a `C^n` immersion, it is automatically `C^n`. +* `IsImmersion.contMDiff`: if f is a `C^n` immersion, it is automatically `C^n` + in the sense of `ContMDiff`.. ## Implementation notes @@ -417,9 +418,8 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (y : s) : simp_all Β· exact I.right_inv (by simp_all) -/-- This lemma is marked private since `h.domChart` is an arbitrary representative: -`continuousAt` is part of the public API -/ -private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : +/-- Prefer using `IsImmersionAtOfComplement.continuousAt` instead -/ +theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : ContinuousOn f h.domChart.source := by rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl h.mapsto_domChart_source_codChart_source (I' := J) (I := I), @@ -427,15 +427,14 @@ private theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : have : ContinuousOn (h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target := by fun_prop exact this.congr h.writtenInCharts -/-- A `C^k` immersion at `x` is continuous at `x`. -/ +/-- A `C^n` immersion at `x` is continuous at `x`. -/ theorem continuousAt (h : IsImmersionAtOfComplement F I J n f x) : ContinuousAt f x := h.continuousOn.continuousAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] -/-- This lemma is marked private since `h.domChart` is an arbitrary representative: -`contMDiffAt` is part of the public API -/ -private theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : +/-- Prefer using `IsImmersionAtOfComplement.contMDiffAt` instead -/ +theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : ContMDiffOn I J n f h.domChart.source := by rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source, @@ -449,7 +448,7 @@ private theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : exact ⟨contDiff_id, contDiff_const (c := (0 : F))⟩ exact this.contMDiffOn.congr h.writtenInCharts -/-- A `C^k` immersion at `x` is `C^k` at `x`. -/ +/-- A `C^n` immersion at `x` is `C^n` at `x`. -/ theorem contMDiffAt (h : IsImmersionAtOfComplement F I J n f x) : ContMDiffAt I J n f x := h.contMDiffOn.contMDiffAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) @@ -624,25 +623,22 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (hx : x ∈ s) use PUnit, by infer_instance, by infer_instance apply Manifold.IsImmersionAtOfComplement.of_opens -/-- This lemma is marked private since `h.domChart` is an arbitrary representative: -`continuousAt` is part of the public API -/ -private theorem continuousOn (h : IsImmersionAt I J n f x) : - ContinuousOn f h.domChart.source := +/-- Prefer using `IsImmersionAt.continuousAt` instead -/ +theorem continuousOn (h : IsImmersionAt I J n f x) : ContinuousOn f h.domChart.source := h.isImmersionAtOfComplement_complement.continuousOn -/-- A `C^k` immersion at `x` is continuous at `x`. -/ +/-- A `C^n` immersion at `x` is continuous at `x`. -/ theorem continuousAt (h : IsImmersionAt I J n f x) : ContinuousAt f x := h.isImmersionAtOfComplement_complement.continuousAt variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] -/-- This lemma is marked private since `h.domChart` is an arbitrary representative: -`contMDiffAt` is part of the public API -/ -private theorem contMDiffOn (h : IsImmersionAt I J n f x) : +/-- Prefer using `IsImmersionAt.contMDiffAt` instead -/ +theorem contMDiffOn (h : IsImmersionAt I J n f x) : ContMDiffOn I J n f h.domChart.source := h.isImmersionAtOfComplement_complement.contMDiffOn -/-- A `C^k` immersion at `x` is `C^k` at `x`. -/ +/-- A `C^n` immersion at `x` is `C^n` at `x`. -/ theorem contMDiffAt (h : IsImmersionAt I J n f x) : ContMDiffAt I J n f x := h.isImmersionAtOfComplement_complement.contMDiffAt @@ -739,7 +735,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) : IsImmersionOfComplement PUnit I I n (Subtype.val : s β†’ M) := fun y ↦ IsImmersionAtOfComplement.of_opens s y -/-- A `C^k` immersion is `C^k`. -/ +/-- A `C^n` immersion is `C^n`. -/ theorem contMDiff [IsManifold I n M] [IsManifold J n N] (h : IsImmersionOfComplement F I J n f) : ContMDiff I J n f := fun x ↦ (h x).contMDiffAt diff --git a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean index 2ec1f1888579d1..f222c50f7ec035 100644 --- a/Mathlib/Geometry/Manifold/SmoothEmbedding.lean +++ b/Mathlib/Geometry/Manifold/SmoothEmbedding.lean @@ -22,7 +22,8 @@ This will be useful to define embedded submanifolds. * `IsSmoothEmbedding.id`: the identity map is a smooth embedding * `IsSmoothEmbedding.of_opens`: the inclusion of an open subset `s β†’ M` of a smooth manifold is a smooth embedding -* `IsSmoothEmbedding.contMDiff`: if `f` is a `C^n` embedding, it is automatically `C^n`. +* `IsSmoothEmbedding.contMDiff`: if `f` is a `C^n` embedding, it is automatically `C^n` + in the sense of `ContMDiff`.. ## Implementation notes @@ -64,8 +65,8 @@ variable {π•œ : Type*} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} variable (I J n) in -/-- A `C^k` map `f : M β†’ M'` is a smooth `C^k` embedding if it is a topological embedding -and a `C^k` immersion. -/ +/-- A `C^n` map `f : M β†’ M'` is a smooth `C^n` embedding if it is a topological embedding +and a `C^n` immersion. -/ @[mk_iff] structure IsSmoothEmbedding (f : M β†’ N) where isImmersion : IsImmersion I J n f From a0680ef3bd10836c2a812aabd49a6d6ac73cf1f3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:26:22 +0100 Subject: [PATCH 36/38] Explain writtenInExtend, and re-use more variables --- .../Geometry/Manifold/ContMDiff/Atlas.lean | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index a4217bf154d5d0..d5741724614926 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -9,10 +9,18 @@ public import Mathlib.Geometry.Manifold.ContMDiff.Basic import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace /-! -## Smoothness of charts and local structomorphisms +# Smoothness of charts and local structomorphisms We show that the model with corners, charts, extended charts and their inverses are `C^n`, and that local structomorphisms are `C^n` with `C^n` inverses. + +## Implementation notes + +This file uses the name `writtenInExtend` (in analogy to `writtenInExtChart`) to refer to a +composition `ψ.extend J ∘ f ∘ Ο†.extend I` of `f : M β†’ N` with charts `ψ` and `Ο†` extended by the +appropriate models with corners. This is not a definition, so technically deviating from the naming +convention. + -/ @[expose] public section @@ -295,20 +303,12 @@ theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : OpenPartialHomeomorph M end IsLocalStructomorph -open Set Filter Function - -variable {π•œ : Type*} [NontriviallyNormedField π•œ] - {E F : Type*} [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedAddCommGroup F] [NormedSpace π•œ F] - {H G : Type*} [TopologicalSpace H] [TopologicalSpace G] - {I : ModelWithCorners π•œ E H} {J : ModelWithCorners π•œ F G} - {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - {N : Type*} [TopologicalSpace N] [ChartedSpace G N] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type*} [TopologicalSpace G] + {J : ModelWithCorners π•œ F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop β„•βˆž} [IsManifold I n M] [IsManifold J n N] {f : M β†’ N} {s : Set M} {Ο† : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} --- There is no definition `writtenInExtend`, but we already use some made-up names in this file. - /-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`. -/ theorem contMDiffWithinAt_writtenInExtend_iff {y : M} (hΟ† : Ο† ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N) From 0174bc37b79e47c0bdf110fb1533675a5e0e224b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:28:22 +0100 Subject: [PATCH 37/38] One more --- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 2 ++ Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean | 12 +++++++++--- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index d5741724614926..44f0b886bea153 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -21,6 +21,8 @@ composition `ψ.extend J ∘ f ∘ Ο†.extend I` of `f : M β†’ N` with charts `ψ appropriate models with corners. This is not a definition, so technically deviating from the naming convention. +`isLocalStructomorphOn` is another made-up name. + -/ @[expose] public section diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index b2af90ac2fd2a6..6d4520f8b24759 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -39,6 +39,15 @@ in general, but we can still register them as `PartialEquiv`. * `FiniteDimensional.of_locallyCompact_manifold`: a locally compact manifold must be modelled on a finite-dimensional space +## Implementation notes + +This file uses the name `writtenInExtend` (in analogy to `writtenInExtChart`) to refer to a +composition `ψ.extend J ∘ f ∘ Ο†.extend I` of `f : M β†’ N` with charts `ψ` and `Ο†` extended by the +appropriate models with corners. This is not a definition, so technically deviating from the naming +convention. + +TODO: this file uses more made-up names; document these as well + -/ @[expose] public section @@ -251,7 +260,6 @@ theorem tendsto_extend_comp_iff {Ξ± : Type*} {l : Filter Ξ±} {g : Ξ± β†’ M} filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu simpa only [(Β· ∘ Β·), extend_left_inv _ hz, mem_preimage] using hzu --- there is no definition `writtenInExtend` but we already use some made-up names in this file theorem continuousWithinAt_writtenInExtend_iff {f' : OpenPartialHomeomorph M' H'} {g : M β†’ M'} {y : M} (hy : y ∈ f.source) (hgy : g y ∈ f'.source) (hmaps : MapsTo g s f'.source) : ContinuousWithinAt (f'.extend I' ∘ g ∘ (f.extend I).symm) @@ -265,8 +273,6 @@ theorem continuousWithinAt_writtenInExtend_iff {f' : OpenPartialHomeomorph M' H' rw [comp_apply, extend_left_inv _ hz.2] exact hmaps hz.1 --- there is no definition `writtenInExtend` but we already use some made-up names in this file - /-- If `s βŠ† f.source` and `g x ∈ f'.source` whenever `x ∈ s`, then `g` is continuous on `s` if and only if `g` written in charts `f.extend I` and `f'.extend I'` is continuous on `f.extend I '' s`. -/ theorem continuousOn_writtenInExtend_iff {f' : OpenPartialHomeomorph M' H'} {g : M β†’ M'} From 0d97a6641b0eaf3d90785e7744a8e1d702e4c6db Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 16:08:35 +0100 Subject: [PATCH 38/38] feat/chore: add and use custom elaborators for immersions And golf the fail using it, a bit. Other usage sites expose bugs or unexpected error messages... TODO: add basic tests for basic usage TODO: fix those errors (then try to golf further! --- Mathlib/Geometry/Manifold/Immersion.lean | 186 +++++++++++++---------- 1 file changed, 107 insertions(+), 79 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean index 1435ca73dd7038..9a24ee3819fe3c 100644 --- a/Mathlib/Geometry/Manifold/Immersion.lean +++ b/Mathlib/Geometry/Manifold/Immersion.lean @@ -13,6 +13,8 @@ public import Mathlib.Analysis.Normed.Operator.Banach public import Mathlib.Analysis.Normed.Module.Shrink public import Mathlib.Topology.Algebra.Module.TransferInstance +public import Mathlib.Geometry.Manifold.Notation + /-! # Smooth immersions In this file, we define `C^n` immersions between `C^n` manifolds. @@ -166,6 +168,17 @@ Unless you have a particular reason, prefer to use `IsImmersionAt` instead. irreducible_def IsImmersionAtOfComplement (f : M β†’ N) (x : M) : Prop := LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp F I J M N) +open Lean Elab Meta Qq Manifold.Elab in +/-- `IsImmersionAtOfComplement% F n f x` elaborates to `IsImmersionAtOfComplement F I J n f x`, +trying to determine `I` and `J` from the local context. -/ +scoped elab:max "IsImmersionAtOfComplement%" ppSpace F:term:arg ppSpace nt:term:arg ppSpace + f:term:arg : term => do + let eF ← Term.elabTerm F none + let ne ← Term.elabTermEnsuringType nt q(WithTop β„•βˆž) + let ef ← ensureIsFunction <|← Term.elabTerm f none + let (srcI, tgtI) ← findModels ef none + mkAppM ``IsImmersionAtOfComplement #[eF, srcI, tgtI, ne, ef] + -- Lift the universe from `E''`, to avoid a free universe parameter. variable (I J n) in /-- `f : M β†’ N` is a `C^n` immersion at `x` if there are charts `Ο†` and `ψ` of `M` and `N` @@ -184,6 +197,15 @@ irreducible_def IsImmersionAt (f : M β†’ N) (x : M) : Prop := βˆƒ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace π•œ F), IsImmersionAtOfComplement F I J n f x +open Lean Elab Meta Qq Manifold.Elab in +/-- `IsImmersionAt% n f x` elaborates to `IsImmersionAt I J n f x`, +trying to determine `I` and `J` from the local context. -/ +scoped elab:max "IsImmersionAt%" ppSpace nt:term:arg ppSpace f:term:arg : term => do + let ne ← Term.elabTermEnsuringType nt q(WithTop β„•βˆž) + let ef ← ensureIsFunction <|← Term.elabTerm f none + let (srcI, tgtI) ← findModels ef none + mkAppM ``IsImmersionAt #[srcI, tgtI, ne, ef] + variable {f g : M β†’ N} {x : M} namespace IsImmersionAtOfComplement @@ -195,7 +217,7 @@ lemma mk_of_charts (equiv : (E Γ— F) ≃L[π•œ] E'') (domChart : OpenPartialHome (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hsource : domChart.source βŠ† f ⁻¹' codChart.source) (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (Β·, 0)) - (domChart.extend I).target) : IsImmersionAtOfComplement F I J n f x := by + (domChart.extend I).target) : IsImmersionAtOfComplement% F n f x := by rw [IsImmersionAtOfComplement_def] use domChart, codChart use equiv @@ -210,7 +232,7 @@ lemma mk_of_continuousAt {f : M β†’ N} {x : M} (hf : ContinuousAt f x) (equiv : (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (Β·, 0)) - (domChart.extend I).target) : IsImmersionAtOfComplement F I J n f x := by + (domChart.extend I).target) : IsImmersionAtOfComplement% F n f x := by rw [IsImmersionAtOfComplement_def] exact LiftSourceTargetPropertyAt.mk_of_continuousAt hf isLocalSourceTargetProperty_immersionAtProp _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩ @@ -220,7 +242,7 @@ 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. The particular chart is arbitrary, but this choice matches the witnesses given by `h.codChart` and `h.codChart`. -/ -def domChart (h : IsImmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph M H := by +def domChart (h : IsImmersionAtOfComplement% F n f x) : OpenPartialHomeomorph M H := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.domChart h @@ -229,35 +251,35 @@ w.r.t. this chart and the data `h.domChart` and `h.equiv`, `f` will look like an inclusion `u ↦ (u, 0)` in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by `h.equiv` and `h.domChart`. -/ -def codChart (h : IsImmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph N G := by +def codChart (h : IsImmersionAtOfComplement% F n f x) : OpenPartialHomeomorph N G := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.codChart h -lemma mem_domChart_source (h : IsImmersionAtOfComplement F I J n f x) : x ∈ h.domChart.source := by +lemma mem_domChart_source (h : IsImmersionAtOfComplement% F n f x) : x ∈ h.domChart.source := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.mem_domChart_source h -lemma mem_codChart_source (h : IsImmersionAtOfComplement F I J n f x) : +lemma mem_codChart_source (h : IsImmersionAtOfComplement% F n f x) : f x ∈ h.codChart.source := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.mem_codChart_source h -lemma domChart_mem_maximalAtlas (h : IsImmersionAtOfComplement F I J n f x) : +lemma domChart_mem_maximalAtlas (h : IsImmersionAtOfComplement% F n f x) : h.domChart ∈ IsManifold.maximalAtlas I n M := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas h -lemma codChart_mem_maximalAtlas (h : IsImmersionAtOfComplement F I J n f x) : +lemma codChart_mem_maximalAtlas (h : IsImmersionAtOfComplement% F n f x) : h.codChart ∈ IsManifold.maximalAtlas J n N := by rw [IsImmersionAtOfComplement_def] at h exact LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas h -lemma source_subset_preimage_source (h : IsImmersionAtOfComplement F I J n f x) : +lemma source_subset_preimage_source (h : IsImmersionAtOfComplement% F n f x) : h.domChart.source βŠ† f ⁻¹' h.codChart.source := by rw [IsImmersionAtOfComplement_def] at h exact h.source_subset_preimage_source -lemma mapsto_domChart_source_codChart_source (h : IsImmersionAtOfComplement F I J n f x) : +lemma mapsto_domChart_source_codChart_source (h : IsImmersionAtOfComplement% F n f x) : MapsTo f h.domChart.source h.codChart.source := by rw [IsImmersionAtOfComplement_def] at h exact h.source_subset_preimage_source @@ -265,17 +287,17 @@ lemma mapsto_domChart_source_codChart_source (h : IsImmersionAtOfComplement F I /-- A linear equivalence `E Γ— F ≃L[π•œ] E''` which belongs to the data of an immersion `f` at `x`: the particular equivalence is arbitrary, but this choice matches the witnesses given by `h.domChart` and `h.codChart`. -/ -def equiv (h : IsImmersionAtOfComplement F I J n f x) : (E Γ— F) ≃L[π•œ] E'' := by +def equiv (h : IsImmersionAtOfComplement% F n f x) : (E Γ— F) ≃L[π•œ] E'' := by rw [IsImmersionAtOfComplement_def] at h exact Classical.choose <| LiftSourceTargetPropertyAt.property h -lemma writtenInCharts (h : IsImmersionAtOfComplement F I J n f x) : +lemma writtenInCharts (h : IsImmersionAtOfComplement% F n f x) : EqOn ((h.codChart.extend J) ∘ f ∘ (h.domChart.extend I).symm) (h.equiv ∘ (Β·, 0)) (h.domChart.extend I).target := by rw [IsImmersionAtOfComplement_def] at h exact Classical.choose_spec <| LiftSourceTargetPropertyAt.property h -lemma property (h : IsImmersionAtOfComplement F I J n f x) : +lemma property (h : IsImmersionAtOfComplement% F n f x) : LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp F I J M N) := by rwa [IsImmersionAtOfComplement_def] at h @@ -298,7 +320,7 @@ continuous at `x` (see `mk_of_continuousAt`), which is easy to ascertain in prac See `target_subset_preimage_target` for a version stated using preimages instead of images. -/ -lemma map_target_subset_target (h : IsImmersionAtOfComplement F I J n f x) : +lemma map_target_subset_target (h : IsImmersionAtOfComplement% F n f x) : (h.equiv ∘ (Β·, 0)) '' (h.domChart.extend I).target βŠ† (h.codChart.extend J).target := by rw [← h.writtenInCharts.image_eq, Set.image_comp, Set.image_comp, PartialEquiv.symm_image_target_eq_source, OpenPartialHomeomorph.extend_source, @@ -310,14 +332,14 @@ lemma map_target_subset_target (h : IsImmersionAtOfComplement F I J n f x) : /-- If `f` is an immersion at `x`, its domain chart's target `(h.domChart.extend I).target` is mapped to its codomain chart's target `(h.domChart.extend J).target`: see `map_target_subset_target` for a version stated using images. -/ -lemma target_subset_preimage_target (h : IsImmersionAtOfComplement F I J n f x) : +lemma target_subset_preimage_target (h : IsImmersionAtOfComplement% F n f x) : (h.domChart.extend I).target βŠ† (h.equiv ∘ (Β·, 0)) ⁻¹' (h.codChart.extend J).target := fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx) /-- If `f` is an immersion at `x` and `g = f` on some neighbourhood of `x`, then `g` is an immersion at `x`. -/ -lemma congr_of_eventuallyEq (hf : IsImmersionAtOfComplement F I J n f x) (hfg : f =αΆ [𝓝 x] g) : - IsImmersionAtOfComplement F I J n g x := by +lemma congr_of_eventuallyEq (hf : IsImmersionAtOfComplement% F n f x) (hfg : f =αΆ [𝓝 x] g) : + IsImmersionAtOfComplement% F n g x := by rw [IsImmersionAtOfComplement_def] exact LiftSourceTargetPropertyAt.congr_of_eventuallyEq isLocalSourceTargetProperty_immersionAtProp hf.property hfg @@ -325,26 +347,26 @@ lemma congr_of_eventuallyEq (hf : IsImmersionAtOfComplement F I J n f x) (hfg : /-- If `f = g` on some neighbourhood of `x`, then `f` is an immersion at `x` if and only if `g` is an immersion at `x`. -/ lemma congr_iff_of_eventuallyEq (hfg : f =αΆ [𝓝 x] g) : - IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F I J n g x := by + IsImmersionAtOfComplement% F n f x ↔ IsImmersionAtOfComplement% F n g x := by simpa only [IsImmersionAtOfComplement_def] using LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq isLocalSourceTargetProperty_immersionAtProp hfg -lemma small (hf : IsImmersionAtOfComplement F I J n f x) : Small.{u} F := +lemma small (hf : IsImmersionAtOfComplement% F n f x) : Small.{u} F := small_of_injective <| hf.equiv.injective.comp (Prod.mk_right_injective 0) /-- Given an immersion `f` at `x`, this is a choice of complement which lives in the same universe as the model space for the co-domain of `f`: this is useful to avoid universe restrictions. -/ -def smallComplement (hf : IsImmersionAtOfComplement F I J n f x) : Type u := +def smallComplement (hf : IsImmersionAtOfComplement% F n f x) : Type u := haveI := hf.small Shrink.{u} F -instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement := by +instance (hf : IsImmersionAtOfComplement% F n f x) : NormedAddCommGroup hf.smallComplement := by haveI := hf.small unfold smallComplement infer_instance -instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace π•œ hf.smallComplement := by +instance (hf : IsImmersionAtOfComplement% F n f x) : NormedSpace π•œ hf.smallComplement := by haveI := hf.small unfold smallComplement infer_instance @@ -353,12 +375,12 @@ instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace π•œ hf.smal a continuous linear equivalence from `F` to the small complement of `F`: mathematically, this is just the identity map; however, this is technically useful as it enables us to always work with `hf.smallComplement`. -/ -def smallEquiv (hf : IsImmersionAtOfComplement F I J n f x) : F ≃L[π•œ] hf.smallComplement := +def smallEquiv (hf : IsImmersionAtOfComplement% F n f x) : F ≃L[π•œ] hf.smallComplement := haveI := hf.small ((equivShrink F).symm.continuousLinearEquiv π•œ).symm -lemma trans_F (h : IsImmersionAtOfComplement F I J n f x) (e : F ≃L[π•œ] F') : - IsImmersionAtOfComplement F' I J n f x := by +lemma trans_F (h : IsImmersionAtOfComplement% F n f x) (e : F ≃L[π•œ] F') : + IsImmersionAtOfComplement% F' n f x := by rewrite [IsImmersionAtOfComplement_def] refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source, h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩ @@ -369,12 +391,12 @@ lemma trans_F (h : IsImmersionAtOfComplement F I J n f x) (e : F ≃L[π•œ] F') /-- Being an immersion at `x` w.r.t. `F` is stable under replacing `F` by an isomorphic copy. -/ lemma congr_F (e : F ≃L[π•œ] F') : - IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F' I J n f x := + IsImmersionAtOfComplement% F n f x ↔ IsImmersionAtOfComplement% F' n f x := ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩ /- The set of points where `IsImmersionAtOfComplement` holds is open. -/ lemma _root_.IsOpen.isImmersionAtOfComplement : - IsOpen {x | IsImmersionAtOfComplement F I J n f x} := by + IsOpen {x | IsImmersionAtOfComplement% F n f x} := by simp_rw [IsImmersionAtOfComplement_def] exact .liftSourceTargetPropertyAt @@ -382,7 +404,7 @@ lemma _root_.IsOpen.isImmersionAtOfComplement : then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] - (hf : IsImmersionAtOfComplement F I J n f x) (hg : IsImmersionAtOfComplement F' I' J' n g x') : + (hf : IsImmersionAtOfComplement% F n f x) (hg : IsImmersionAtOfComplement% F' n g x') : IsImmersionAtOfComplement (F Γ— F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := by rw [IsImmersionAtOfComplement_def] apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property @@ -397,8 +419,7 @@ Note that the proof contains a small formalisation-related subtlety: `F` can liv while being an immersion at `x` requires the existence of a complement in the same universe as the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`. -/ -lemma isImmersionAt (h : IsImmersionAtOfComplement F I J n f x) : - IsImmersionAt I J n f x := by +lemma isImmersionAt (h : IsImmersionAtOfComplement% F n f x) : IsImmersionAt% n f x := by rw [IsImmersionAt_def] use h.smallComplement, by infer_instance, by infer_instance exact (IsImmersionAtOfComplement.congr_F h.smallEquiv).mp h @@ -419,7 +440,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (y : s) : Β· exact I.right_inv (by simp_all) /-- Prefer using `IsImmersionAtOfComplement.continuousAt` instead -/ -theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : +theorem continuousOn (h : IsImmersionAtOfComplement% F n f x) : ContinuousOn f h.domChart.source := by rw [← h.domChart.continuousOn_writtenInExtend_iff le_rfl h.mapsto_domChart_source_codChart_source (I' := J) (I := I), @@ -428,14 +449,13 @@ theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) : exact this.congr h.writtenInCharts /-- A `C^n` immersion at `x` is continuous at `x`. -/ -theorem continuousAt (h : IsImmersionAtOfComplement F I J n f x) : ContinuousAt f x := +theorem continuousAt (h : IsImmersionAtOfComplement% F n f x) : ContinuousAt f x := h.continuousOn.continuousAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] /-- Prefer using `IsImmersionAtOfComplement.contMDiffAt` instead -/ -theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : - ContMDiffOn I J n f h.domChart.source := by +theorem contMDiffOn (h : IsImmersionAtOfComplement% F n f x) : CMDiff[h.domChart.source] n f := by rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source, ← h.domChart.extend_target_eq_image_source] @@ -449,7 +469,7 @@ theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) : exact this.contMDiffOn.congr h.writtenInCharts /-- A `C^n` immersion at `x` is `C^n` at `x`. -/ -theorem contMDiffAt (h : IsImmersionAtOfComplement F I J n f x) : ContMDiffAt I J n f x := +theorem contMDiffAt (h : IsImmersionAtOfComplement% F n f x) : CMDiffAt n f x := h.contMDiffOn.contMDiffAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) end IsImmersionAtOfComplement @@ -463,9 +483,9 @@ lemma mk_of_charts (equiv : (E Γ— F) ≃L[π•œ] E'') (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hsource : domChart.source βŠ† f ⁻¹' codChart.source) (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (Β·, 0)) - (domChart.extend I).target) : IsImmersionAt I J n f x := by + (domChart.extend I).target) : IsImmersionAt% n f x := by rw [IsImmersionAt_def] - have aux : IsImmersionAtOfComplement F I J n f x := by + have aux : IsImmersionAtOfComplement% F n f x := by apply IsImmersionAtOfComplement.mk_of_charts <;> assumption use aux.smallComplement, by infer_instance, by infer_instance rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv] @@ -480,29 +500,29 @@ lemma mk_of_continuousAt {f : M β†’ N} {x : M} (hf : ContinuousAt f x) (equiv : (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M) (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N) (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (Β·, 0)) - (domChart.extend I).target) : IsImmersionAt I J n f x := by + (domChart.extend I).target) : IsImmersionAt% n f x := by rw [IsImmersionAt_def] - have aux : IsImmersionAtOfComplement F I J n f x := by + have aux : IsImmersionAtOfComplement% F n f x := by apply IsImmersionAtOfComplement.mk_of_continuousAt <;> assumption use aux.smallComplement, by infer_instance, by infer_instance rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv] /-- A choice of complement of the model normed space `E` of `M` in the model normed space `E'` of `N` -/ -def complement (h : IsImmersionAt I J n f x) : Type u := by +def complement (h : IsImmersionAt% n f x) : Type u := by rw [IsImmersionAt_def] at h exact Classical.choose h -noncomputable instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement := by +noncomputable instance (h : IsImmersionAt% n f x) : NormedAddCommGroup h.complement := by rw [IsImmersionAt_def] at h exact Classical.choose <| Classical.choose_spec h -noncomputable instance (h : IsImmersionAt I J n f x) : NormedSpace π•œ h.complement := by +noncomputable instance (h : IsImmersionAt% n f x) : NormedSpace π•œ h.complement := by rw [IsImmersionAt_def] at h exact Classical.choose <| Classical.choose_spec <| Classical.choose_spec h -lemma isImmersionAtOfComplement_complement (h : IsImmersionAt I J n f x) : - IsImmersionAtOfComplement h.complement I J n f x := by +lemma isImmersionAtOfComplement_complement (h : IsImmersionAt% n f x) : + IsImmersionAtOfComplement% h.complement n f x := by rw [IsImmersionAt_def] at h exact Classical.choose_spec <| Classical.choose_spec <| Classical.choose_spec h @@ -511,7 +531,7 @@ 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. The particular chart is arbitrary, but this choice matches the witnesses given by `h.codChart` and `h.codChart`. -/ -def domChart (h : IsImmersionAt I J n f x) : OpenPartialHomeomorph M H := +def domChart (h : IsImmersionAt% n f x) : OpenPartialHomeomorph M H := h.isImmersionAtOfComplement_complement.domChart /-- A choice of chart on the co-domain `N` of an immersion `f` at `x`: @@ -519,39 +539,39 @@ w.r.t. this chart and the data `h.domChart` and `h.equiv`, `f` will look like an inclusion `u ↦ (u, 0)` in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by `h.equiv` and `h.domChart`. -/ -def codChart (h : IsImmersionAt I J n f x) : OpenPartialHomeomorph N G := +def codChart (h : IsImmersionAt% n f x) : OpenPartialHomeomorph N G := h.isImmersionAtOfComplement_complement.codChart -lemma mem_domChart_source (h : IsImmersionAt I J n f x) : x ∈ h.domChart.source := +lemma mem_domChart_source (h : IsImmersionAt% n f x) : x ∈ h.domChart.source := h.isImmersionAtOfComplement_complement.mem_domChart_source -lemma mem_codChart_source (h : IsImmersionAt I J n f x) : f x ∈ h.codChart.source := +lemma mem_codChart_source (h : IsImmersionAt% n f x) : f x ∈ h.codChart.source := h.isImmersionAtOfComplement_complement.mem_codChart_source -lemma domChart_mem_maximalAtlas (h : IsImmersionAt I J n f x) : +lemma domChart_mem_maximalAtlas (h : IsImmersionAt% n f x) : h.domChart ∈ IsManifold.maximalAtlas I n M := h.isImmersionAtOfComplement_complement.domChart_mem_maximalAtlas -lemma codChart_mem_maximalAtlas (h : IsImmersionAt I J n f x) : +lemma codChart_mem_maximalAtlas (h : IsImmersionAt% n f x) : h.codChart ∈ IsManifold.maximalAtlas J n N := h.isImmersionAtOfComplement_complement.codChart_mem_maximalAtlas -lemma source_subset_preimage_source (h : IsImmersionAt I J n f x) : +lemma source_subset_preimage_source (h : IsImmersionAt% n f x) : h.domChart.source βŠ† f ⁻¹' h.codChart.source := h.isImmersionAtOfComplement_complement.source_subset_preimage_source /-- A linear equivalence `E Γ— F ≃L[π•œ] E''` which belongs to the data of an immersion `f` at `x`: the particular equivalence is arbitrary, but this choice matches the witnesses given by `h.domChart` and `h.codChart`. -/ -def equiv (h : IsImmersionAt I J n f x) : (E Γ— h.complement) ≃L[π•œ] E'' := +def equiv (h : IsImmersionAt% n f x) : (E Γ— h.complement) ≃L[π•œ] E'' := h.isImmersionAtOfComplement_complement.equiv -lemma writtenInCharts (h : IsImmersionAt I J n f x) : +lemma writtenInCharts (h : IsImmersionAt% n f x) : EqOn ((h.codChart.extend J) ∘ f ∘ (h.domChart.extend I).symm) (h.equiv ∘ (Β·, 0)) (h.domChart.extend I).target := h.isImmersionAtOfComplement_complement.writtenInCharts -lemma property (h : IsImmersionAt I J n f x) : +lemma property (h : IsImmersionAt% n f x) : LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp h.complement I J M N) := h.isImmersionAtOfComplement_complement.property @@ -574,21 +594,21 @@ continuous at `x` (see `mk_of_continuousAt`), which is easy to ascertain in prac See `target_subset_preimage_target` for a version stated using preimages instead of images. -/ -lemma map_target_subset_target (h : IsImmersionAt I J n f x) : +lemma map_target_subset_target (h : IsImmersionAt% n f x) : (h.equiv ∘ (Β·, 0)) '' (h.domChart.extend I).target βŠ† (h.codChart.extend J).target := h.isImmersionAtOfComplement_complement.map_target_subset_target /-- If `f` is an immersion at `x`, its domain chart's target `(h.domChart.extend I).target` is mapped to its codomain chart's target `(h.domChart.extend J).target`: see `map_target_subset_target` for a version stated using images. -/ -lemma target_subset_preimage_target (h : IsImmersionAt I J n f x) : +lemma target_subset_preimage_target (h : IsImmersionAt% n f x) : (h.domChart.extend I).target βŠ† (h.equiv ∘ (Β·, 0)) ⁻¹' (h.codChart.extend J).target := fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx) /-- If `f` is an immersion at `x` and `g = f` on some neighbourhood of `x`, then `g` is an immersion at `x`. -/ -lemma congr_of_eventuallyEq (hf : IsImmersionAt I J n f x) (hfg : f =αΆ [𝓝 x] g) : - IsImmersionAt I J n g x := by +lemma congr_of_eventuallyEq (hf : IsImmersionAt% n f x) (hfg : f =αΆ [𝓝 x] g) : + IsImmersionAt% n g x := by rw [IsImmersionAt_def] use hf.complement, by infer_instance, by infer_instance exact hf.isImmersionAtOfComplement_complement.congr_of_eventuallyEq hfg @@ -596,14 +616,14 @@ lemma congr_of_eventuallyEq (hf : IsImmersionAt I J n f x) (hfg : f =αΆ [𝓝 x] /-- If `f = g` on some neighbourhood of `x`, then `f` is an immersion at `x` if and only if `g` is an immersion at `x`. -/ lemma congr_iff (hfg : f =αΆ [𝓝 x] g) : - IsImmersionAt I J n f x ↔ IsImmersionAt I J n g x := + IsImmersionAt% n f x ↔ IsImmersionAt% n g x := ⟨fun h ↦ h.congr_of_eventuallyEq hfg, fun h ↦ h.congr_of_eventuallyEq hfg.symm⟩ /- The set of points where `IsImmersionAt` holds is open. -/ lemma _root_.IsOpen.isImmersionAt : - IsOpen {x | IsImmersionAt I J n f x} := by + IsOpen {x | IsImmersionAt% n f x} := by rw [isOpen_iff_forall_mem_open] - exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x }, + exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement% hx.complement n f x }, fun y hy ↦ hy.isImmersionAt, .isImmersionAtOfComplement, by simp [hx.isImmersionAtOfComplement_complement]⟩ @@ -611,7 +631,7 @@ lemma _root_.IsOpen.isImmersionAt : then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] - (hf : IsImmersionAt I J n f x) (hg : IsImmersionAt I' J' n g x') : + (hf : IsImmersionAt% n f x) (hg : IsImmersionAt I' J' n g x') : IsImmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := hf.isImmersionAtOfComplement_complement.prodMap hg.isImmersionAtOfComplement_complement |>.isImmersionAt @@ -624,22 +644,21 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (hx : x ∈ s) apply Manifold.IsImmersionAtOfComplement.of_opens /-- Prefer using `IsImmersionAt.continuousAt` instead -/ -theorem continuousOn (h : IsImmersionAt I J n f x) : ContinuousOn f h.domChart.source := +theorem continuousOn (h : IsImmersionAt% n f x) : ContinuousOn f h.domChart.source := h.isImmersionAtOfComplement_complement.continuousOn /-- A `C^n` immersion at `x` is continuous at `x`. -/ -theorem continuousAt (h : IsImmersionAt I J n f x) : ContinuousAt f x := +theorem continuousAt (h : IsImmersionAt% n f x) : ContinuousAt f x := h.isImmersionAtOfComplement_complement.continuousAt variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] /-- Prefer using `IsImmersionAt.contMDiffAt` instead -/ -theorem contMDiffOn (h : IsImmersionAt I J n f x) : - ContMDiffOn I J n f h.domChart.source := +theorem contMDiffOn (h : IsImmersionAt% n f x) : CMDiff[h.domChart.source] n f := h.isImmersionAtOfComplement_complement.contMDiffOn /-- A `C^n` immersion at `x` is `C^n` at `x`. -/ -theorem contMDiffAt (h : IsImmersionAt I J n f x) : ContMDiffAt I J n f x := +theorem contMDiffAt (h : IsImmersionAt% n f x) : CMDiffAt n f x := h.isImmersionAtOfComplement_complement.contMDiffAt end IsImmersionAt @@ -672,13 +691,23 @@ each `x ∈ M` w.r.t. potentially varying complements: see `isImmersionAt` for d def IsImmersion (f : M β†’ N) : Prop := βˆƒ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace π•œ F), IsImmersionOfComplement F I J n f +open Lean Elab Meta Qq Manifold.Elab in +/-- `IsImmersion% n f` elaborates to `IsImmersion I J n f`, +trying to determine `I` and `J` from the local context. -/ +scoped elab:max "IsImmersion%" ppSpace nt:term:arg ppSpace f:term:arg : term => do + let ne ← Term.elabTermEnsuringType nt q(WithTop β„•βˆž) + let ef ← ensureIsFunction <|← Term.elabTerm f none + let (srcI, tgtI) ← findModels ef none + mkAppM ``IsImmersion #[srcI, tgtI, ne, ef] + namespace IsImmersionOfComplement variable {f g : M β†’ N} /-- If `f` is an immersion, it is an immersion at each point. -/ +-- TODO: using the elaborator in the hypothesis fails; investigate and fix! lemma isImmersionAt (h : IsImmersionOfComplement F I J n f) (x : M) : - IsImmersionAtOfComplement F I J n f x := h x + IsImmersionAtOfComplement% F n f x := h x /-- If `f = g` and `f` is an immersion, so is `g`. -/ theorem congr (h : IsImmersionOfComplement F I J n f) (heq : f = g) : @@ -748,16 +777,16 @@ variable {f g : M β†’ N} /-- A choice of complement of the model normed space `E` of `M` in the model normed space `E'` of `N` -/ -def complement (h : IsImmersion I J n f) : Type u := Classical.choose h +def complement (h : IsImmersion% n f) : Type u := Classical.choose h -noncomputable instance (h : IsImmersion I J n f) : NormedAddCommGroup h.complement := +noncomputable instance (h : IsImmersion% n f) : NormedAddCommGroup h.complement := Classical.choose <| Classical.choose_spec h -noncomputable instance (h : IsImmersion I J n f) : NormedSpace π•œ h.complement := +noncomputable instance (h : IsImmersion% n f) : NormedSpace π•œ h.complement := Classical.choose <| Classical.choose_spec <| Classical.choose_spec h -lemma isImmersionOfComplement_complement (h : IsImmersion I J n f) : - IsImmersionOfComplement h.complement I J n f := +lemma isImmersionOfComplement_complement (h : IsImmersion% n f) : + IsImmersionOfComplement h.complement I J n f := -- TODO: using the elaborator here errors! Classical.choose_spec <| Classical.choose_spec <| Classical.choose_spec h /-- If `f` is an immersion, it is an immersion at each point. @@ -771,25 +800,25 @@ of `f` at (even nearby) points `x` and `x'` are not directly related. They have is not conclusive. If `E''` is infinite-dimensional, this dimension can indeed change between different connected of `M`. -/ -lemma isImmersionAt (h : IsImmersion I J n f) (x : M) : IsImmersionAt I J n f x := by +lemma isImmersionAt (h : IsImmersion% n f) (x : M) : IsImmersionAt% n f x := by rw [IsImmersionAt_def] use h.complement, by infer_instance, by infer_instance, h.isImmersionOfComplement_complement x /-- If `f = g` and `f` is an immersion, so is `g`. -/ -theorem congr (h : IsImmersion I J n f) (heq : f = g) : IsImmersion I J n g := +theorem congr (h : IsImmersion% n f) (heq : f = g) : IsImmersion% n g := heq β–Έ h /-- If `f: M β†’ N` and `g: M' Γ— N'` are immersions at `x` and `x'`, respectively, then `f Γ— g: M Γ— N β†’ M' Γ— N'` is an immersion at `(x, x')`. -/ theorem prodMap {f : M β†’ N} {g : M' β†’ N'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] - (hf : IsImmersion I J n f) (hg : IsImmersion I' J' n g) : + (hf : IsImmersion% n f) (hg : IsImmersion% n g) : IsImmersion (I.prod I') (J.prod J') n (Prod.map f g) := (hf.isImmersionOfComplement_complement.prodMap hg.isImmersionOfComplement_complement).isImmersion open IsManifold in /-- The identity map is an immersion. -/ -protected lemma id [IsManifold I n M] : IsImmersion I I n (@id M) := +protected lemma id [IsManifold I n M] : IsImmersion% n (@id M) := ⟨PUnit, by infer_instance, by infer_instance, IsImmersionOfComplement.id⟩ /- The inclusion of an open subset `s` of a smooth manifold `M` is an immersion. -/ @@ -798,8 +827,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) : ⟨PUnit, by infer_instance, by infer_instance, IsImmersionOfComplement.of_opens s⟩ /-- A `C^n` immersion is `C^n`. -/ -theorem contMDiff [IsManifold I n M] [IsManifold J n N] - (h : IsImmersion I J n f) : ContMDiff I J n f := +theorem contMDiff [IsManifold I n M] [IsManifold J n N] (h : IsImmersion% n f) : CMDiff n f := h.isImmersionOfComplement_complement.contMDiff end IsImmersion