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 examples 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 satisfied 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.
• IsOpen.liftSourceTargetPropertyAt: the set of points at which LiftSourceTargetPropertyAt holds is open

structure Manifold.IsLocalSourceTargetProperty {H : Type u_6} {G : Type u_8} [TopologicalSpace H] [TopologicalSpace G] {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [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. compatible choices of both a chart on M and N. Currently, we ask for the property to be 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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_10 u_12) u_6) u_8)

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 J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 examples 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 J n f x P = Nonempty (Manifold.LocalPresentationAt I J n f x P)

noncomputable def Manifold.LiftSourceTargetPropertyAt.localPresentationAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : LocalPresentationAt I J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : x ∈ h.domChart.source

theorem Manifold.LiftSourceTargetPropertyAt.mem_codChart_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : f x ∈ h.codChart.source

theorem Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : h.domChart ∈ IsManifold.maximalAtlas I n M

theorem Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : h.codChart ∈ IsManifold.maximalAtlas J n N

theorem Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : h.domChart.source ⊆ f ⁻¹' h.codChart.source

theorem Manifold.LiftSourceTargetPropertyAt.property {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) : P f h.domChart h.codChart

theorem Manifold.LiftSourceTargetPropertyAt.congr_iff {H : Type u_6} {G : Type u_8} [TopologicalSpace H] [TopologicalSpace G] {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n N) (hfP : P f domChart codChart) : LiftSourceTargetPropertyAt I J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P) (h' : f =ᶠ[nhds x] g) : LiftSourceTargetPropertyAt I J 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} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [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 J n f x P ↔ LiftSourceTargetPropertyAt I J 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.

theorem IsOpen.liftSourceTargetPropertyAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {g : M → N} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} : IsOpen {x : M | Manifold.LiftSourceTargetPropertyAt I J n g x P}

theorem Manifold.LiftSourceTargetPropertyAt.prodMap {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5} {H : Type u_6} {H' : Type u_7} {G : Type u_8} {G' : Type u_9} [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 : Type u_10} {M' : Type u_11} {N : Type u_12} {N' : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} [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