Skip to content

Commit 6829f56

Browse files
grunweggrunweg
committed
change
1 parent e5ca88b commit 6829f56

2 files changed

Lines changed: 275 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3794,6 +3794,7 @@ import Mathlib.Geometry.Manifold.IntegralCurve.Basic
37943794
import Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
37953795
import Mathlib.Geometry.Manifold.IntegralCurve.Transform
37963796
import Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
3797+
import Mathlib.Geometry.Manifold.IsImmersionEmbedding
37973798
import Mathlib.Geometry.Manifold.IsManifold.Basic
37983799
import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
37993800
import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

‎Mathlib/Geometry/Manifold/IsImmersionEmbedding.lean‎

Lines changed: 274 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,274 @@
1+
/-
2+
Copyright (c) 2025 Michael Rothgang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Rothgang
5+
-/
6+
import Mathlib.Geometry.Manifold.ContMDiff.Defs
7+
import Mathlib.Geometry.Manifold.MFDeriv.Defs
8+
import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
9+
import Mathlib.Geometry.Manifold.ContMDiff.Atlas
10+
11+
/-! # Smooth immersions and embeddings
12+
13+
In this file, we define `C^k` immersions and embeddings between `C^k` manifolds.
14+
The correct definition in the infinite-dimensional setting differs from the standard
15+
finite-dimensional definition (concerning the `mfderiv` being injective): future pull requests will
16+
prove that our definition implies the latter, and that both are equivalent for finite-dimensional
17+
manifolds.
18+
19+
## Main definitions
20+
* `IsImmersionAt F I I' n f x` means a map `f : M → M'` between `C^n` manifolds `M` and `M'`
21+
is an immersion at `x : M`: there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`,
22+
respectively, such that in these charts, `f` looks like `u ↦ (u, 0)`, w.r.t. some equivalence
23+
`E' ≃L[𝕜] E × F`. We do not demand that `f` be differentiable (this follows from this definition).
24+
* `IsImmersion F I I' n f` means `f: M → M'` is an immersion at every point `x : M`.
25+
26+
## Main results
27+
* `IsImmersionAt.congr_of_eventuallyEq`: being an immersion is a local property.
28+
If `f` and `g` agree near `x` and `f` is an immersion at `x`, so is `g`
29+
30+
## TODO
31+
* `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`.
32+
* `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`.
33+
* `IsImmersionAt.prodMap`: the product of two immersions is an immersion
34+
* If `f` is an immersion at `x`, its differential splits, hence is injective.
35+
* If `f: M → M'` is a map between Banach manifolds, `mfderiv I I' f x` splitting implies `f` is an
36+
immersion at `x`. (This requires the inverse function theorem.)
37+
* `IsImmersionAt.comp`: if `f: M → M'` and `g: M' → N` are maps between Banach manifolds such that
38+
`f` is an immersion at `x : M` and `g` is an immersion at `f x`, then `g ∘ f` is an immersion
39+
at `x`.
40+
* `IsImmersion.comp`: the composition of immersions (between Banach manifolds) is an immersion
41+
* If `f: M → M'` is a map between finite-dimensional manifolds, `mfderiv I I' f x` being injective
42+
implies `f` is an immersion at `x`.
43+
* define smooth embeddings, and deduce analogous results for these
44+
45+
## References
46+
47+
* [Juan Margalef-Roig and Enrique Outerelo Dominguez, *Differential topology*][roigdomingues2012]
48+
49+
-/
50+
51+
open scoped Manifold Topology ContDiff
52+
53+
open Function Set
54+
55+
-- XXX: does NontriviallyNormedField also work? Splits seems to require more...
56+
variable {𝕜 : Type*} [RCLike 𝕜]
57+
{E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
58+
{E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
59+
{F F' : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
60+
{H : Type*} [TopologicalSpace H] {H' : Type*} [TopologicalSpace H']
61+
{G : Type*} [TopologicalSpace G] {G' : Type*} [TopologicalSpace G']
62+
{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
63+
{J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'}
64+
65+
variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
66+
{M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
67+
{N : Type*} [TopologicalSpace N] [ChartedSpace G N]
68+
{N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N']
69+
{n : WithTop ℕ∞}
70+
71+
-- XXX: should the next three definitions be a class instead?
72+
-- Are these slice charts canonical enough that we want the typeclass system to kick in?
73+
74+
variable (F I I' n) in
75+
/-- `f : M → N` is a `C^k` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
76+
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
77+
Additionally, we demand that `f` map `φ.source` into `ψ.source`.
78+
79+
NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
80+
in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.
81+
-/
82+
def IsImmersionAt (f : M → M') (x : M) : Prop :=
83+
∃ equiv : (E × F) ≃L[𝕜] E',
84+
∃ domChart : PartialHomeomorph M H, ∃ codChart : PartialHomeomorph M' H',
85+
x ∈ domChart.source ∧ f x ∈ codChart.source ∧
86+
domChart ∈ IsManifold.maximalAtlas I n M ∧
87+
codChart ∈ IsManifold.maximalAtlas I' n M' ∧
88+
f '' domChart.source ⊆ codChart.source ∧
89+
EqOn ((codChart.extend I') ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (·, 0))
90+
(domChart.extend I).target
91+
92+
namespace IsImmersionAt
93+
94+
variable {f g : M → M'} {x : M}
95+
96+
/-- `f : M → N` is a `C^k` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
97+
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
98+
This version does not assume that `f` maps `φ.source` to `ψ.source`,
99+
but that `f` is continuous at `x`. -/
100+
def mk_of_continuousAt (f : M → M') (x : M) (hf : ContinuousAt f x)
101+
(equiv : (E × F) ≃L[𝕜] E')
102+
(domChart : PartialHomeomorph M H)
103+
(codChart : PartialHomeomorph M' H')
104+
(hx: x ∈ domChart.source) (hfx : f x ∈ codChart.source)
105+
(hdomChart: domChart ∈ IsManifold.maximalAtlas I n M)
106+
(hcodChart : codChart ∈ IsManifold.maximalAtlas I' n M')
107+
(hwrittenInExtend: EqOn ((codChart.extend I') ∘ f ∘ (domChart.extend I).symm) (equiv ∘ (·, 0))
108+
(domChart.extend I).target) : IsImmersionAt F I I' n f x := by
109+
obtain ⟨s, hs, hsopen, hxs⟩ := mem_nhds_iff.mp <|
110+
hf.preimage_mem_nhds (codChart.open_source.mem_nhds hfx)
111+
have : f '' (domChart.restr s).source ⊆ codChart.source := by
112+
refine Subset.trans ?_ (image_subset_iff.mpr hs)
113+
gcongr
114+
rw [domChart.restr_source' _ hsopen]
115+
exact inter_subset_right
116+
have hmono : ((domChart.restr s).extend I).target ⊆ (domChart.extend I).target := by
117+
have {a b c : Set E} : a ∩ (b ∩ c) ⊆ b := by intro; aesop
118+
simpa using this
119+
exact ⟨equiv, domChart.restr s, codChart,
120+
by rw [domChart.restr_source, interior_eq_iff_isOpen.mpr hsopen]; exact mem_inter hx hxs, hfx,
121+
restr_mem_maximalAtlas (G := contDiffGroupoid n I) hdomChart hsopen, hcodChart, this,
122+
hwrittenInExtend.mono hmono⟩
123+
124+
noncomputable def equiv (h : IsImmersionAt F I I' n f x) : (E × F) ≃L[𝕜] E' :=
125+
Classical.choose h
126+
127+
noncomputable def domChart (h : IsImmersionAt F I I' n f x) : PartialHomeomorph M H :=
128+
Classical.choose (Classical.choose_spec h)
129+
130+
noncomputable def codChart (h : IsImmersionAt F I I' n f x) : PartialHomeomorph M' H' :=
131+
Classical.choose (Classical.choose_spec (Classical.choose_spec h))
132+
133+
lemma mem_domChart_source (h : IsImmersionAt F I I' n f x) : x ∈ h.domChart.source :=
134+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).1
135+
136+
lemma mem_codChart_source (h : IsImmersionAt F I I' n f x) : f x ∈ h.codChart.source :=
137+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).2.1
138+
139+
lemma domChart_mem_maximalAtlas (h : IsImmersionAt F I I' n f x) :
140+
h.domChart ∈ IsManifold.maximalAtlas I n M :=
141+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).2.2.1
142+
143+
lemma codChart_mem_maximalAtlas (h : IsImmersionAt F I I' n f x) :
144+
h.codChart ∈ IsManifold.maximalAtlas I' n M' :=
145+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).2.2.2.1
146+
147+
lemma map_source_subset_source (h : IsImmersionAt F I I' n f x) :
148+
f '' h.domChart.source ⊆ h.codChart.source :=
149+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).2.2.2.2.1
150+
151+
lemma writtenInCharts (h : IsImmersionAt F I I' n f x) :
152+
EqOn ((h.codChart.extend I') ∘ f ∘ (h.domChart.extend I).symm) (h.equiv ∘ (·, 0))
153+
(h.domChart.extend I).target :=
154+
(Classical.choose_spec ((Classical.choose_spec (Classical.choose_spec h)))).2.2.2.2.2
155+
156+
/-- Roig and Domingues [roigdomingues1992] only require this condition on the local charts:
157+
in our setting, this is *slightly* weaker than `map_source_subset_source`: the latter implies
158+
that `h.codChart.extend I' ∘ f` maps `h.domChart.source` to
159+
`(h.codChart.extend I').target = (h.codChart.extend I) '' h.codChart.source`,
160+
but that does *not* imply `f` maps `h.domChart.source` to `h.codChartSource`;
161+
a priori `f` could map some point `f ∘ h.domChart.extend I x ∉ h.codChart.source` into the target.
162+
Note that this difference only occurs because of our design using junk values;
163+
this is not a mathematically meaningful difference.`
164+
165+
At the same time, this condition is fairly weak: it is implied, for instance, by `f` being
166+
continuous at `x` (see `mk_of_continuousAt`), which is easy to acertain in practice.
167+
-/
168+
-- TODO: golf this proof!
169+
lemma map_target_subset_target (h : IsImmersionAt F I I' n f x) :
170+
(h.equiv ∘ (·, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend I').target := by
171+
have : (h.domChart.extend I).target = (h.domChart.extend I) '' (h.domChart.extend I).source := by
172+
rw [PartialEquiv.image_source_eq_target]
173+
rw [this, PartialHomeomorph.extend_source]
174+
set Ψ := h.codChart.extend I'
175+
set Φ := h.domChart.extend I
176+
suffices (Ψ ∘ f ∘ Φ.symm) '' (Φ '' h.domChart.source) ⊆ Ψ.target by
177+
have aux : h.domChart.source = Φ.source := h.domChart.extend_source.symm
178+
rw [aux, PartialEquiv.image_source_eq_target] at this ⊢
179+
rwa [h.writtenInCharts.image_eq] at this
180+
calc
181+
_ = (Ψ ∘ f ∘ ↑Φ.symm ∘ Φ) '' h.domChart.source := by rw [← image_comp]; congr
182+
_ = (Ψ ∘ f) '' ((Φ.symm ∘ Φ) '' h.domChart.source) := by simp [← image_comp]
183+
_ = (Ψ ∘ f) '' h.domChart.source := by rw [h.domChart.extend_left_inv' fun ⦃a⦄ a ↦ a]
184+
_ = Ψ '' (f '' h.domChart.source) := by rw [image_comp]
185+
_ ⊆ Ψ '' h.codChart.source := by gcongr; exact h.map_source_subset_source
186+
_ = Ψ '' Ψ.source := by rw [PartialHomeomorph.extend_source]
187+
_ ⊆ _ := Ψ.map_source''
188+
189+
/-- If `f` is an immersion at `x` and `g = f` on some neighbourhood of `x`,
190+
then `g` is an immersion at `x`. -/
191+
lemma congr_of_eventuallyEq {x : M} (h : IsImmersionAt F I I' n f x) (h' : f =ᶠ[nhds x] g) :
192+
IsImmersionAt F I I' n g x := by
193+
obtain ⟨s', hxs', hfg⟩ := h'.exists_mem
194+
obtain ⟨s, hss', hs, hxs⟩ := mem_nhds_iff.mp hxs'
195+
refine ⟨h.equiv, h.domChart.restr s, h.codChart, ?_, ?_, ?_, h.codChart_mem_maximalAtlas, ?_, ?_⟩
196+
· simpa using ⟨mem_domChart_source h, by rwa [interior_eq_iff_isOpen.mpr hs]⟩
197+
· exact hfg (mem_of_mem_nhds hxs') ▸ mem_codChart_source h
198+
· exact restr_mem_maximalAtlas _ h.domChart_mem_maximalAtlas hs
199+
· have := h.map_source_subset_source
200+
trans f '' (h.domChart.restr s).source
201+
· have : (h.domChart.restr s).source ⊆ s' :=
202+
Subset.trans (by simp [interior_eq_iff_isOpen.mpr hs]) hss'
203+
exact (hfg.mono this).image_eq.symm.le
204+
· exact Subset.trans (image_mono (by simp)) this
205+
· have : f '' (h.domChart.restr s).source ⊆ h.codChart.source := by
206+
refine Subset.trans (image_mono ?_) h.map_source_subset_source
207+
rw [h.domChart.restr_source' _ hs]
208+
exact inter_subset_left
209+
have hmono : ((h.domChart.restr s).extend I).target ⊆ (h.domChart.extend I).target := by
210+
have {a b c : Set E} : a ∩ (b ∩ c) ⊆ b := by intro; aesop
211+
simpa using this
212+
apply EqOn.trans ?_ (h.writtenInCharts.mono hmono)
213+
intro x hx
214+
set Φ := (h.domChart.restr s).extend I
215+
have aux : Φ.source ⊆ s := by
216+
simpa only [Φ, PartialHomeomorph.extend_source, PartialHomeomorph.restr_source,
217+
interior_eq_iff_isOpen.mpr hs] using inter_subset_right
218+
have : (f ∘ Φ.symm) x = (g ∘ Φ.symm) x := hfg <| hss' <| aux (PartialEquiv.map_target _ hx)
219+
rw [Function.comp_apply, ← this]
220+
simp [Φ]
221+
222+
end IsImmersionAt
223+
224+
variable (F I I' n) in
225+
/-- `f : M → N` is a `C^k` immersion if around each point `x ∈ M`,
226+
there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
227+
such that in these charts, `f` looks like `u ↦ (u, 0)`.
228+
229+
In other words, `f` is an immersion at each `x ∈ M`.
230+
-/
231+
def IsImmersion (f : M → M') : Prop := ∀ x, IsImmersionAt F I I' n f x
232+
233+
namespace IsImmersion
234+
235+
variable {f g : M → M'}
236+
237+
/-- If `f` is an immersion, it is an immersion at each point. -/
238+
lemma isImmersionAt (h : IsImmersion F I I' n f) (x : M) : IsImmersionAt F I I' n f x := h x
239+
240+
/-- If `f = g` and `f` is an immersion, so is `g`. -/
241+
theorem congr (h : IsImmersion F I I' n f) (heq : f = g) : IsImmersion F I I' n g :=
242+
fun x ↦ (h x).congr_of_eventuallyEq heq.eventuallyEq
243+
244+
variable [IsManifold I n M] [IsManifold I' n M']
245+
246+
/-- A `C^k` immersion is `C^k`. -/
247+
theorem contMDiff (h : IsImmersion F I I' n f) : ContMDiff I I' n f := fun x ↦ (h x).contMDiffAt
248+
249+
-- These are required to argue that `Splits` composes.
250+
variable [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F] [CompleteSpace F']
251+
variable [IsManifold I 1 M] [IsManifold I' 1 M']
252+
finite-dimensional definition (concerning the `mfderiv` being injective): future pull requests will prove that
253+
/-- If `f` is a `C^k` immersion, each differential `mfderiv x` is injective. -/
254+
theorem mfderiv_injective (h : IsImmersion F I I' n f) (x : M) (hn : 1 ≤ n) : Injective (mfderiv I I' f x) :=
255+
(h x).mfderiv_injective hn
256+
257+
/- If `M` is finite-dimensional, `M` is boundaryless and each `mfderiv I I' f x` is injective,
258+
then `f: M → M'` is a `C^k` immersion. -/
259+
theorem of_mfderiv_injective [FiniteDimensional 𝕜 E] [BoundarylessManifold I M]
260+
(hf : ∀ x, Injective (mfderiv I I' f x)) (hn : 1 ≤ n) : IsImmersion F I I' n f := by
261+
refine fun x ↦ IsImmersionAt.of_finiteDimensional_of_mfderiv_injective ?_ (hf x) hn
262+
exact BoundarylessManifold.isInteriorPoint' x
263+
264+
variable [IsManifold J n N] in
265+
/-- The composition of two immersions is an immersion. -/
266+
lemma comp [BoundarylessManifold I M] [BoundarylessManifold I' M']
267+
{g : M' → N} (hg : IsImmersion F' I' J n g) (hf : IsImmersion F I I' n f) (hn : 1 ≤ n) :
268+
IsImmersion (F × F') I J n (g ∘ f) := by
269+
have : IsManifold J 1 N := IsManifold.of_le hn
270+
refine fun x ↦ (hg (f x)).comp (hf x) hn ?_ ?_
271+
· exact BoundarylessManifold.isInteriorPoint' x
272+
· exact BoundarylessManifold.isInteriorPoint' (f x)
273+
274+
end IsImmersion

0 commit comments

Comments
 (0)