LeanPool.DirectedTopologyLean4.DihomotopyCover

def DirectedMap.Dihomotopy.covered {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} (F : f.Dihomotopy g) (hX : X₀ ∪ X₁ = Set.univ) : Prop

A dihomotopy of directed maps is covered if its image lies entirely in X₀ or in X₁.

Equations

• F.covered hX = (Set.range ⇑F ⊆ X₀ ∨ Set.range ⇑F ⊆ X₁)

def DirectedMap.Dihomotopy.coveredPartwise {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) (F : f.Dihomotopy g) (n m : ℕ) : Prop

A dihomotopy of directed maps is covered partwise n m if it can be covered by rectangles (n+1 vertically, m+1 horizontally) such that each rectangle is covered by either X₀ or X₁

Equations

• DirectedMap.Dihomotopy.coveredPartwise hX F n m = ∀ (i j : ℕ) (hi : i < n.succ) (hj : j < m.succ), have x := hX; ⇑F '' UnitSubrectangle hi hj ⊆ X₀ ∨ ⇑F '' UnitSubrectangle hi hj ⊆ X₁

theorem DirectedMap.Dihomotopy.covered_of_coveredPartwise {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} {F : f.Dihomotopy g} {hX : X₀ ∪ X₁ = Set.univ} (hF : coveredPartwise hX F 0 0) : F.covered hX

A dihomotopy that can be covered partwise by 1 × 1 squares is covered.

theorem DirectedMap.Dihomotopy.left_path_image_interval_subset_of_dihomotopy_subset {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (n : ℕ) {i m : ℕ} (hi : i < m.succ) : ⇑(Dipath.ofDirectedMap f).extend '' Set.Icc (↑i / (↑m + 1)) ((↑i + 1) / (↑m + 1)) ⊆ ⇑F '' UnitSubrectangle ⋯ hi

If F : f ∼ g is a dihomotopy of directed maps, then the image of f restricted to [i/(m+1), (i+1)/(m+1)] is contained in the image of F restricted to [0, 1/(n+1)] × [i/(m+1), (i+1)/(m+1)].

theorem DirectedMap.Dihomotopy.path_covered_partiwse_of_dihomotopy_coveredPartwise_left {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} {F : f.Dihomotopy g} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F n m) : Dipath.coveredPartwise hX (Dipath.ofDirectedMap f) m

If F : f ∼ g is a dihomotopy of directed maps, and F is n × m-covered, then f is m-covered.

theorem DirectedMap.Dihomotopy.right_path_image_interval_subset_of_dihomotopy_subset {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (n : ℕ) {i m : ℕ} (hi : i < m.succ) : ⇑(Dipath.ofDirectedMap g).extend '' Set.Icc (↑i / (↑m + 1)) ((↑i + 1) / (↑m + 1)) ⊆ ⇑F '' UnitSubrectangle ⋯ hi

If F : f ∼ g is a dihomotopy of directed maps, then the image of g restricted to [i/(m+1), (i+1)/(m+1)] is contained in the image of F restricted to [n/(n+1), 1] × [i/(m+1), (i+1)/(m+1)].

theorem DirectedMap.Dihomotopy.path_covered_partiwse_of_dihomotopy_coveredPartwise_right {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} {F : f.Dihomotopy g} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F n m) : Dipath.coveredPartwise hX (Dipath.ofDirectedMap g) m

If F : f ∼ g is a dihomotopy of directed maps, and F is n × m-covered, then g is m-covered.

theorem DirectedMap.Dihomotopy.coveredPartwise_exists {X : dTopCat} {f g : D(↑unitInterval,↑X)} {X₀ X₁ : Set ↑X} (F : f.Dihomotopy g) (hX : X₀ ∪ X₁ = Set.univ) (X₀_open : IsOpen X₀) (X₁_open : IsOpen X₁) : ∃ (n : ℕ) (m : ℕ), coveredPartwise hX F n m

If F : f ∼ g is a dihomotopy of directed maps, there exist n m : ℕ such that F is n × m-covered.

theorem DirectedMap.Dihomotopy.fpv_subrectangle {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {n m j : ℕ} (hj : j < m.succ) : ⇑(SplitDihomotopy.FirstPartVerticallyDihomotopy F (Fraction.ofPos ⋯)).toDihomotopy '' UnitSubrectangle ⋯ hj ⊆ ⇑F '' UnitSubrectangle ⋯ hj

The image of a dihomotopy F of the subrectangles [0, 1/(n+2)] × [j/(m+1), (j+1)/(m+1)] contains the image of the first part of F, split at 1/(n+2), of [0, 1] × [j/(m+1), (j+1)/(m+1)].

theorem DirectedMap.Dihomotopy.coveredPartwise_first_vpart {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F.toDihomotopy n.succ m) : coveredPartwise hX (SplitDihomotopy.FirstPartVerticallyDihomotopy F (Fraction.ofPos ⋯)).toDihomotopy 0 m

If F is (n+1) × m-covered, then the first part of F, split at T = 1/(n+2) is 0 x m-covered.

theorem DirectedMap.Dihomotopy.spv_aux₁_coed {t : ℝ} {n i : ℕ} : i < n.succ → ∀ (ht : ↑i / ↑n.succ ≤ t), (↑i + 1) / (↑n + 2) ≤ (1 - 1 / (↑n + 1 + 1)) * t + 1 / (↑n + 1 + 1)

If i/(n+1) ≤ t, then (i+1)/(n+2) ≤ (σ q) * t + q, where q = 1/(n+2)

theorem DirectedMap.Dihomotopy.spv_aux₁ {t : ↑unitInterval} {n i : ℕ} (hi : i < n.succ) (ht : Fraction ⋯ ⋯ ≤ t) : Fraction ⋯ ⋯ ≤ ⟨↑(unitInterval.symm (Fraction ⋯ ⋯)) * ↑t + ↑(Fraction ⋯ ⋯), ⋯⟩

If i/(n+1) ≤ t, then (i+1)/(n+2) ≤ (σ q) * t + q, where q = 1/(n+2)

theorem DirectedMap.Dihomotopy.spv_aux₂_coed {t : ℝ} {n i : ℕ} : i < n.succ → 0 ≤ t → ∀ (ht : t ≤ ↑i.succ / ↑n.succ), (1 - 1 / (↑n + 1 + 1)) * t + 1 / (↑n + 1 + 1) ≤ (↑i + 2) / (↑n + 2)

If t ≤ (i+1)/(n+1), then (σ q) * t + q ≤ (i+2)/(n+2), where q = 1/(n+2)

theorem DirectedMap.Dihomotopy.spv_aux₂ {t : ↑unitInterval} {n i : ℕ} (hi : i < n.succ) (ht : t ≤ Fraction ⋯ ⋯) : ⟨↑(unitInterval.symm (Fraction ⋯ ⋯)) * ↑t + ↑(Fraction ⋯ ⋯), ⋯⟩ ≤ Fraction ⋯ ⋯

If t ≤ (i+1)/(n+1), then (σ q) * t + q ≤ (i+2)/(n+2), where q = 1/(n+2)

theorem DirectedMap.Dihomotopy.spv_subrectangle {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {n m i j : ℕ} (hi : i < n.succ) (hj : j < m.succ) : ⇑(SplitDihomotopy.SecondPartVerticallyDihomotopy F (Fraction.ofPos ⋯)).toDihomotopy '' UnitSubrectangle hi hj ⊆ ⇑F '' UnitSubrectangle ⋯ hj

The image of a dihomotopy F of the subrectangle [(i+1)/(n+2), (i+2)/(n+2)] × [j/(m+1), (j+1)/(m+1)] contains the image of the second part of F, split at 1/(n+2), of [i/(n+1), (i+1)/(n+1)] × [j/(m+1), (j+1)/(m+1)].

theorem DirectedMap.Dihomotopy.coveredPartwise_second_vpart {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F.toDihomotopy n.succ m) : coveredPartwise hX (SplitDihomotopy.SecondPartVerticallyDihomotopy F (Fraction.ofPos ⋯)).toDihomotopy n m

If F is (n + 1) × m-covered, then the second part of F, split at T = 1/(n+1) is n × m-covered.

theorem DirectedMap.Dihomotopy.fph_subrectangle {X : dTopCat} {f g : D(↑unitInterval,↑X)} {F : f.Dihomotopy g} {n m i : ℕ} (hi : i < n.succ) : ⇑(SplitDihomotopy.FirstPartHorizontallyDihomotopy F (Fraction.ofPos ⋯)) '' UnitSubrectangle hi ⋯ ⊆ ⇑F '' UnitSubrectangle hi ⋯

The image of a dihomotopy F of the rectangle [i/(n+1), (i+1)/(n+1)] × [0, 1/(m+2)] contains the image of the first part of F, split at 1/(m+2), of [i/(n+1), (i+1)/(n+1)] × [0, 1].

theorem DirectedMap.Dihomotopy.coveredPartwise_first_hpart {X : dTopCat} {X₀ X₁ : Set ↑X} {f g : D(↑unitInterval,↑X)} {F : f.Dihomotopy g} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F n m.succ) : coveredPartwise hX (SplitDihomotopy.FirstPartHorizontallyDihomotopy F (Fraction.ofPos ⋯)) n 0

If F is n × (m+1)-covered, then the first part of F, split at T = 1/(m+2), is n × 0-covered.

theorem DirectedMap.Dihomotopy.sph_subrectangle {X : dTopCat} {f g : D(↑unitInterval,↑X)} {F : f.Dihomotopy g} {n m i j : ℕ} (hi : i < n.succ) (hj : j < m.succ) : ⇑(SplitDihomotopy.SecondPartHorizontallyDihomotopy F (Fraction.ofPos ⋯)) '' UnitSubrectangle hi hj ⊆ ⇑F '' UnitSubrectangle hi ⋯

The image of a dihomotopy F of the rectangle [i/(n+1), (i+1)/(n+1)] × [(j+1)/(m+2), (j+2)/(m+2)] contains the image of the second part of F, split at 1/(m+2), of [i/(n+1), (i+1)/(n+1)] × [j/(m+1), (j+1)/(m+1)].

theorem DirectedMap.Dihomotopy.coveredPartwise_second_hpart {X : dTopCat} {X₀ X₁ : Set ↑X} {f g : D(↑unitInterval,↑X)} {F : f.Dihomotopy g} {hX : X₀ ∪ X₁ = Set.univ} {n m : ℕ} (hF : coveredPartwise hX F n m.succ) : coveredPartwise hX (SplitDihomotopy.SecondPartHorizontallyDihomotopy F (Fraction.ofPos ⋯)) n m

If F is n × (m+1)-covered, then the second part of F, split at at T = 1/(n+1) is n × m-covered.

theorem Dipath.Dihomotopy.range_left_subset {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) : Set.range ⇑γ₁ ⊆ Set.range ⇑F

theorem Dipath.Dihomotopy.range_right_subset {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) : Set.range ⇑γ₂ ⊆ Set.range ⇑F

def Dipath.Dihomotopy.covered {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (hX : X₀ ∪ X₁ = Set.univ) (F : γ₁.Dihomotopy γ₂) : Prop

A dihomotopy of directed paths is covered if its image lies entirely in X₀ or in X₁.

Equations

• Dipath.Dihomotopy.covered hX F = (Set.range ⇑F ⊆ X₀ ∨ Set.range ⇑F ⊆ X₁)

theorem Dipath.Dihomotopy.covered_left_of_covered {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {hX : X₀ ∪ X₁ = Set.univ} (hF : covered hX F) : Dipath.covered hX γ₁

If F : γ₁ ∼ γ₂ is a dihomotopy of directed paths, and F is covered, then γ₁ is covered.

theorem Dipath.Dihomotopy.covered_right_of_covered {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} {hX : X₀ ∪ X₁ = Set.univ} (hF : covered hX F) : Dipath.covered hX γ₂

If F : γ₁ ∼ γ₂ is a dihomotopy of directed paths, and F is covered, then γ₂ is covered.

def Dipath.Dihomotopy.dihomotopicCovered {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} (hX : X₀ ∪ X₁ = Set.univ) (γ₁ γ₂ : Dipath x y) (n m : ℕ) : Prop

Two paths are m × n-dihomotopic if there is a dihomotopy between them that can be covered by m × n rectangles.

Equations

• Dipath.Dihomotopy.dihomotopicCovered hX γ₁ γ₂ n m = ∃ (F : γ₁.Dihomotopy γ₂), DirectedMap.Dihomotopy.coveredPartwise hX F.toDihomotopy n m

theorem Dipath.Dihomotopy.dihomotopicCovered_split {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} {F : γ₁.Dihomotopy γ₂} (hX : X₀ ∪ X₁ = Set.univ) {n m : ℕ} (hF : DirectedMap.Dihomotopy.coveredPartwise hX F.toDihomotopy n.succ m) : dihomotopicCovered hX γ₁ (F.eval (Fraction.ofPos ⋯)) 0 m ∧ dihomotopicCovered hX (F.eval (Fraction.ofPos ⋯)) γ₂ n m

If γ₁ and γ₂ are two paths connected by a path-dihomotopy F that is covered by m × (n + 1) rectangles, then γ₁ and F.eval (1/(n+2)) are m × 0-dihomotopic and F.eval (1/(n+2)) and γ₂ are m × n-dihomotopic.

theorem Dipath.Dihomotopy.dihomotopicCovered_exists_of_preDihomotopic {X : dTopCat} {X₀ X₁ : Set ↑X} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (hX : X₀ ∪ X₁ = Set.univ) (h : γ₁.PreDihomotopic γ₂) (X₀_open : IsOpen X₀) (X₁_open : IsOpen X₁) : ∃ (n : ℕ) (m : ℕ), dihomotopicCovered hX γ₁ γ₂ n m

If γ₁ and γ₂ are two directed paths paths such that there is some dihomotopy between them, then there are n m : ℕ such that γ₁ and γ₂ are n × m-dihomotopicCovered.