Local properties of smooth functions which depend on both the source and target

In this file, we consider local properties of functions between manifolds, which depend on both the source and the target: more precisely, properties P of functions f : M → N such that f has property P if and only if there is a suitable pair of charts on M and N, respectively, such that f read in these charts has a particular form. The motivating example of this general description are immersions and submersions: f : M → N is an immersion at x iff there are charts φ and ψ of M and N around x and f x, respectively, such that in these charts, f looks like u ↦ (u, 0). Similarly, f is a submersion at x iff it looks like a projection (u, v) ↦ u in suitable charts near x and f x.

Studying such local properties allows proving several lemmas about immersions and submersions only once. In IsImmersionEmbedding.lean, we prove that being an immersion at x is indeed a local property of this form.

Main definitions and results

• Manifold.LocalSourceTargetPropertyAt captures a local property of the above form: for each f : M → N, and pair of charts φ of M and ψ of N, the local property is either safisfied or not. We ask that the property be stable under congruence and under restriction of φ.
• Manifold.LiftSourceTargetPropertyAt f x P, where P is a LocalSourceTargetPropertyAt, defines a local property of functions of the above shape: 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.

structure Manifold.IsLocalSourceTargetProperty {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] {N : Type u_7} [TopologicalSpace N] (P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) : Prop

Structure recording good behaviour of a property of functions M → N w.r.t. to compatible choices of both a chart on M and N. Currently, we ask for the property being stable under restriction of the domain chart, and local in the target.

Motivating examples are immersions and submersions of smooth manifolds.

• mono_source {f : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} {s : Set M} : IsOpen s → P f φ ψ → P f (φ.restr s) ψ
• congr {f g : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} : Set.EqOn f g φ.source → P f φ ψ → P g φ ψ

structure Manifold.LocalPresentationAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 F G) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) (P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) : Type (max (max (max u_4 u_5) u_6) u_7)

Data witnessing the fact that f has local property P at x

• domChart : OpenPartialHomeomorph M H

  A choice of chart on the domain M of the local property P of f at x: w.r.t. this chart and codChart, f has the local property P at x.

• codChart : OpenPartialHomeomorph N G

  A choice of chart on the target N of the local property P of f at x: w.r.t. this chart and domChart, f has the local property P at x.

• mem_domChart_source : x ∈ self.domChart.source
• mem_codChart_source : f x ∈ self.codChart.source
• domChart_mem_maximalAtlas : self.domChart ∈ IsManifold.maximalAtlas I n M
• codChart_mem_maximalAtlas : self.codChart ∈ IsManifold.maximalAtlas I' n N
• source_subset_preimage_source : self.domChart.source ⊆ f ⁻¹' self.codChart.source
• property : P f self.domChart self.codChart

def Manifold.LiftSourceTargetPropertyAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 F G) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M) (P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) : Prop

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 ψ.

The motivating example are smooth immersions and submersions: the corresponding condition is that f look like the inclusion u ↦ (u, 0) (resp. a projection (u, v) ↦ u) in the charts φ and ψ.

Equations

• Manifold.LiftSourceTargetPropertyAt I I' n f x P = Nonempty (Manifold.LocalPresentationAt I I' n f x P)

noncomputable def Manifold.LiftSourceTargetPropertyAt.localPresentationAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : LocalPresentationAt I I' n f x P

A choice of charts witnessing the local property P of f at x.

Equations

• h.localPresentationAt = Classical.choice h

noncomputable def Manifold.LiftSourceTargetPropertyAt.domChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : OpenPartialHomeomorph M 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.

Equations

• h.domChart = h.localPresentationAt.domChart

noncomputable def Manifold.LiftSourceTargetPropertyAt.codChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : OpenPartialHomeomorph N G

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.

Equations

• h.codChart = h.localPresentationAt.codChart

theorem Manifold.LiftSourceTargetPropertyAt.mem_domChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : x ∈ h.domChart.source

theorem Manifold.LiftSourceTargetPropertyAt.mem_codChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : f x ∈ h.codChart.source

theorem Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : h.domChart ∈ IsManifold.maximalAtlas I n M

theorem Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : h.codChart ∈ IsManifold.maximalAtlas I' n N

theorem Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : h.domChart.source ⊆ f ⁻¹' h.codChart.source

theorem Manifold.LiftSourceTargetPropertyAt.property {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (h : LiftSourceTargetPropertyAt I I' n f x P) : P f h.domChart h.codChart

theorem Manifold.LiftSourceTargetPropertyAt.congr_iff {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] {N : Type u_7} [TopologicalSpace N] {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (hP : IsLocalSourceTargetProperty P) {f g : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} (hfg : Set.EqOn f g φ.source) : P f φ ψ ↔ P g φ ψ

theorem Manifold.LiftSourceTargetPropertyAt.mk_of_continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (hf : ContinuousAt f x) (hP : IsLocalSourceTargetProperty P) (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

If P is a local property, by monotonicity w.r.t. restricting domChart, if f is continuous at x, to prove LiftSourceTargetPropertyAt I I' n f x P we need not check the condition f '' domChart.source ⊆ codChart.source.

theorem Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (hP : IsLocalSourceTargetProperty P) (hf : LiftSourceTargetPropertyAt I I' n f x P) (h' : f =ᶠ[nhds x] g) : LiftSourceTargetPropertyAt I I' n g x P

If P is monotone w.r.t. restricting domChart and closed under congruence, if f has property P at x and f and g are eventually equal near x, then g has property P at x.

theorem Manifold.LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (hP : IsLocalSourceTargetProperty P) (h' : f =ᶠ[nhds x] g) : LiftSourceTargetPropertyAt I I' n f x P ↔ LiftSourceTargetPropertyAt I I' n g x P

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.