Notes by Patrick:

The goal of this file is to explore how to prove exists_surrounding_loops and the local to global inductive homotopy construction in a way that uncouples the general topological argument from the things specific to loops or homotopies of jet sections.

First there is a lemma inductive_construction which abstracts the locally ultimately constant arguments, assuming we work with a fixed covering. It builds on LocallyFinite.exists_forall_eventually_of_indexType.

From inductive_construction alone we deduce inductive_htpy_construction which builds a homotopy in a similar context. This is meant to be used to go from Chapter 2 to Chapter 3.

Combining inductive_construction with an argument using local existence and exhaustions, we get inductive_construction_of_loc building a function from local existence and patching assumptions. It also has a version relative_inductive_construction_of_loc which does this relative to a closed set. This is used for exists_surrounding_loops.

This file also contains supporting lemmas about IndexType. A short term goal will be to get rid of the indexing abstraction and do everything in terms of IndexType, unless indexing makes those supporting lemmas really cleaner to prove.

theorem LocallyFinite.exists_forall_eventually_of_indexType {α : Type u_1} {X : Type u_2} [TopologicalSpace X] {N : ℕ} {f : IndexType N → X → α} {V : IndexType N → Set X} (hV : LocallyFinite V) (h : ∀ (n : IndexType N), ¬IsMax n → ∀ x ∉ V n.succ, f n.succ x = f n x) : ∃ (F : X → α), ∀ (x : X), ∀ᶠ (n : IndexType N) in Filter.atTop, f n =ᶠ[nhds x] F

theorem inductive_construction {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {N : ℕ} {U : IndexType N → Set X} (P₀ : (x : X) → (nhds x).Germ Y → Prop) (P₁ : IndexType N → (x : X) → (nhds x).Germ Y → Prop) (P₂ : IndexType N → (X → Y) → Prop) (U_fin : LocallyFinite U) (init : ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ P₂ 0 f) (ind : ∀ (i : IndexType N) (f : X → Y), (∀ (x : X), P₀ x ↑f) → P₂ i f → (∀ j < i, ∀ (x : X), P₁ j x ↑f) → ∃ (f' : X → Y), (∀ (x : X), P₀ x ↑f') ∧ (¬IsMax i → P₂ i.succ f') ∧ (∀ j ≤ i, ∀ (x : X), P₁ j x ↑f') ∧ ∀ x ∉ U i, f' x = f x) : ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ ∀ (j : IndexType N) (x : X), P₁ j x ↑f

theorem inductive_construction_of_loc' {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₀' P₁ : (x : X) → (nhds x).Germ Y → Prop) {f₀ : X → Y} (hP₀f₀ : ∀ (x : X), P₀ x ↑f₀ ∧ P₀' x ↑f₀) (loc : ∀ (x : X), ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ ∀ᶠ (x' : X) in nhds x, P₁ x' ↑f) (ind : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → IsCompact K₁ → IsCompact K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → (∀ (x : X), P₀ x ↑f₁ ∧ P₀' x ↑f₁) → (∀ (x : X), P₀ x ↑f₂) → (∀ x ∈ U₁, P₁ x ↑f₁) → (∀ x ∈ U₂, P₁ x ↑f₂) → ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f ∧ P₀' x ↑f) ∧ (∀ᶠ (x : X) in nhdsSet (K₁ ∪ K₂), P₁ x ↑f) ∧ ∀ᶠ (x : X) in nhdsSet (K₁ ∪ U₂ᶜ), f x = f₁ x) : ∃ (f : X → Y), ∀ (x : X), P₀ x ↑f ∧ P₀' x ↑f ∧ P₁ x ↑f

theorem inductive_construction_of_loc {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₀' P₁ : (x : X) → (nhds x).Germ Y → Prop) {f₀ : X → Y} (hP₀f₀ : ∀ (x : X), P₀ x ↑f₀ ∧ P₀' x ↑f₀) (loc : ∀ (x : X), ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ ∀ᶠ (x' : X) in nhds x, P₁ x' ↑f) (ind : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → IsCompact K₁ → IsCompact K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → (∀ (x : X), P₀ x ↑f₁ ∧ P₀' x ↑f₁) → (∀ (x : X), P₀ x ↑f₂) → (∀ x ∈ U₁, P₁ x ↑f₁) → (∀ x ∈ U₂, P₁ x ↑f₂) → ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f ∧ P₀' x ↑f) ∧ (∀ᶠ (x : X) in nhdsSet (K₁ ∪ K₂), P₁ x ↑f) ∧ ∀ᶠ (x : X) in nhdsSet (K₁ ∪ U₂ᶜ), f x = f₁ x) : ∃ (f : X → Y), ∀ (x : X), P₀ x ↑f ∧ P₀' x ↑f ∧ P₁ x ↑f

We are given a suitably nice extended metric space X and three local constraints P₀,P₀' and P₁ on maps from X to some type Y. All maps entering the discussion are required to statisfy P₀ everywhere. The goal is to turn a map f₀ satisfying P₁ near a compact set K into one satisfying everywhere without changing f₀ near K. The assumptions are:

• For every x in X there is a map which satisfies P₁ near x
• One can patch two maps f₁ f₂ satisfying P₁ on open sets U₁ and U₂ respectively and such that f₁ satisfies P₀' everywhere into a map satisfying P₁ on K₁ ∪ K₂ for any compact sets Kᵢ ⊆ Uᵢ and P₀' everywhere.

theorem set_juggling {X : Type u_1} [TopologicalSpace X] [NormalSpace X] [T2Space X] {K : Set X} (hK : IsClosed K) {U₁ U₂ K₁ K₂ : Set X} (U₁_op : IsOpen U₁) (U₂_op : IsOpen U₂) (K₁_cpct : IsCompact K₁) (K₂_cpct : IsCompact K₂) (hK₁U₁ : K₁ ⊆ U₁) (hK₂U₂ : K₂ ⊆ U₂) (U : Set X) (U_op : IsOpen U) (hKU : K ⊆ U) : ∃ (K₁' : Set X) (K₂' : Set X) (U₁' : Set X) (U₂' : Set X), IsOpen U₁' ∧ IsOpen U₂' ∧ IsCompact K₁' ∧ IsCompact K₂' ∧ K₁ ⊆ K₁' ∧ K₁' ⊆ U₁' ∧ K₂' ⊆ U₂' ∧ K₁' ∪ K₂' = K₁ ∪ K₂ ∧ K ⊆ U₂'ᶜ ∧ U₁' ⊆ U ∪ U₁ ∧ U₂' ⊆ U₂

theorem relative_inductive_construction_of_loc {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₁ : (x : X) → (nhds x).Germ Y → Prop) {K : Set X} (hK : IsClosed K) {f₀ : X → Y} (hP₀f₀ : ∀ (x : X), P₀ x ↑f₀) (hP₁f₀ : ∀ᶠ (x : X) in nhdsSet K, P₁ x ↑f₀) (loc : ∀ (x : X), ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ ∀ᶠ (x' : X) in nhds x, P₁ x' ↑f) (ind : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → IsCompact K₁ → IsCompact K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → (∀ (x : X), P₀ x ↑f₁) → (∀ (x : X), P₀ x ↑f₂) → (∀ x ∈ U₁, P₁ x ↑f₁) → (∀ x ∈ U₂, P₁ x ↑f₂) → ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f) ∧ (∀ᶠ (x : X) in nhdsSet (K₁ ∪ K₂), P₁ x ↑f) ∧ ∀ᶠ (x : X) in nhdsSet (K₁ ∪ U₂ᶜ), f x = f₁ x) : ∃ (f : X → Y), (∀ (x : X), P₀ x ↑f ∧ P₁ x ↑f) ∧ ∀ᶠ (x : X) in nhdsSet K, f x = f₀ x

We are given a suitably nice extended metric space X and three local constraints P₀,P₀' and P₁ on maps from X to some type Y. All maps entering the discussion are required to statisfy P₀ everywhere. The goal is to turn a map f₀ satisfying P₁ near a compact set K into one satisfying everywhere without changing f₀ near K. The assumptions are:

• For every x in X there is a map which satisfies P₁ near x
• One can patch two maps f₁ f₂ satisfying P₁ on open sets U₁ and U₂ respectively into a map satisfying P₁ on K₁ ∪ K₂ for any compact sets Kᵢ ⊆ Uᵢ. This is deduced this version from the version where K is empty but adding some P'₀, see inductive_construction_of_loc.

theorem inductive_htpy_construction' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {N : ℕ} {U K : IndexType N → Set X} (P₀ P₁ : (x : X) → (nhds x).Germ Y → Prop) (P₂ : (p : ℝ × X) → (nhds p).Germ Y → Prop) (hP₂ : ∀ (a b : ℝ) (p : ℝ × X) (f : ℝ × X → Y), P₂ (a * p.1 + b, p.2) ↑f → P₂ p ↑fun (p : ℝ × X) => f (a * p.1 + b, p.2)) (U_fin : LocallyFinite U) (K_cover : ⋃ (i : IndexType N), K i = Set.univ) {f₀ : X → Y} (init : ∀ (x : X), P₀ x ↑f₀) (init' : ∀ (p : ℝ × X), P₂ p ↑fun (p : ℝ × X) => f₀ p.2) (ind : ∀ (i : IndexType N) (f : X → Y), (∀ (x : X), P₀ x ↑f) → (∀ᶠ (x : X) in nhdsSet (⋃ (j : IndexType N), ⋃ (_ : j < i), K j), P₁ x ↑f) → ∃ (F : ℝ → X → Y), (∀ (t : ℝ) (x : X), P₀ x ↑(F t)) ∧ (∀ᶠ (x : X) in nhdsSet (⋃ (j : IndexType N), ⋃ (_ : j ≤ i), K j), P₁ x ↑(F 1)) ∧ (∀ (p : ℝ × X), P₂ p ↑↿F) ∧ (∀ (t : ℝ), ∀ x ∉ U i, F t x = f x) ∧ (∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), F t = f) ∧ ∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), F t = F 1) : ∃ (F : ℝ → X → Y), F 0 = f₀ ∧ (∀ (t : ℝ) (x : X), P₀ x ↑(F t)) ∧ (∀ (x : X), P₁ x ↑(F 1)) ∧ ∀ (p : ℝ × X), P₂ p ↑↿F

theorem inductive_htpy_construction {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₁ : (x : X) → (nhds x).Germ Y → Prop) (P₂ : (p : ℝ × X) → (nhds p).Germ Y → Prop) (hP₂ : ∀ (a b : ℝ) (p : ℝ × X) (f : ℝ × X → Y), P₂ (a * p.1 + b, p.2) ↑f → P₂ p ↑fun (p : ℝ × X) => f (a * p.1 + b, p.2)) (hP₂' : ∀ (t : ℝ) (x : X) (f : X → Y), P₀ x ↑f → P₂ (t, x) ↑fun (p : ℝ × X) => f p.2) {f₀ : X → Y} (init : ∀ (x : X), P₀ x ↑f₀) (ind : ∀ (x : X), ∃ V ∈ nhds x, ∀ K₁ ⊆ V, ∀ K₀ ⊆ interior K₁, IsCompact K₀ → IsCompact K₁ → ∀ (C : Set X) (f : X → Y), IsClosed C → (∀ (x : X), P₀ x ↑f) → (∀ᶠ (x : X) in nhdsSet C, P₁ x ↑f) → ∃ (F : ℝ → X → Y), (∀ (t : ℝ) (x : X), P₀ x ↑(F t)) ∧ (∀ᶠ (x : X) in nhdsSet (C ∪ K₀), P₁ x ↑(F 1)) ∧ (∀ (p : ℝ × X), P₂ p ↑↿F) ∧ (∀ (t : ℝ), ∀ x ∉ K₁, F t x = f x) ∧ (∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), F t = f) ∧ ∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), F t = F 1) : ∃ (F : ℝ → X → Y), F 0 = f₀ ∧ (∀ (t : ℝ) (x : X), P₀ x ↑(F t)) ∧ (∀ (x : X), P₁ x ↑(F 1)) ∧ ∀ (p : ℝ × X), P₂ p ↑↿F