LeanPool.DirectedTopologyLean4.DipathSubtype

theorem DiSubtype.subtypeHom_eq_coe {X : dTopCat} {X₀ : Set ↑X} (x : ↑X₀) : (CategoryTheory.ConcreteCategory.hom (dTopCat.DirectedSubtypeHom X₀)) x = ↑x

theorem DiSubtype.range_dipath_map_inclusion {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X₀} (γ : Dipath x y) : Set.range ⇑(γ.map (DirectedSubtypeInclusion X₀)) ⊆ X₀

theorem DiSubtype.subtype_path_class_eq_map {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X₀} (γ : Dipath x y) : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₀)).map ⟦γ⟧ = ⟦γ.map (DirectedSubtypeInclusion X₀)⟧

theorem DiSubtype.source_elt_of_image_subset {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) : x ∈ X₀

theorem DiSubtype.target_elt_of_image_subset {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) : y ∈ X₀

def DiSubtype.SubtypePath {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) : Path ⟨x, ⋯⟩ ⟨y, ⋯⟩

Lift a path whose range lies inside X₀ to a path in the subtype X₀.

Equations

• DiSubtype.SubtypePath hγ = { toFun := fun (t : ↑unitInterval) => ⟨γ t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

def DiSubtype.SubtypeDipath {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} (γ : Dipath x y) (hγ : Set.range ⇑γ ⊆ X₀) : Dipath ⟨x, ⋯⟩ ⟨y, ⋯⟩

Lift a dipath whose range lies inside X₀ to a dipath in the subtype X₀.

Equations

• DiSubtype.SubtypeDipath γ hγ = { toPath := DiSubtype.SubtypePath hγ, dipath_toPath := ⋯ }

theorem DiSubtype.map_subtypeDipath_eq {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} (γ : Dipath x y) (hγ : Set.range ⇑γ ⊆ X₀) : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₀)).map ⟦SubtypeDipath γ hγ⟧ = ⟦γ⟧

theorem DiSubtype.subtypeDipath_of_included_dipath_eq {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X₀} (γ : Dipath x y) : SubtypeDipath (γ.map (DirectedSubtypeInclusion X₀)) ⋯ = γ.cast ⋯ ⋯

theorem DiSubtype.range_refl_subset_of_mem {X : dTopCat} {X₀ : Set ↑X} {x : ↑X} (hx : x ∈ X₀) : Set.range ⇑(Dipath.refl x) ⊆ X₀

theorem DiSubtype.subtype_refl {X : dTopCat} {X₀ : Set ↑X} {x : ↑X} (hx : x ∈ X₀) : SubtypeDipath (Dipath.refl x) ⋯ = Dipath.refl ⟨x, hx⟩

theorem DiSubtype.subsets_of_trans_subset {X : dTopCat} {X₀ : Set ↑X} {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Set.range ⇑(γ₁.trans γ₂) ⊆ X₀) : Set.range ⇑γ₁ ⊆ X₀ ∧ Set.range ⇑γ₂ ⊆ X₀

theorem DiSubtype.trans_subset_of_subsets {X : dTopCat} {X₀ : Set ↑X} {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ₁ : Set.range ⇑γ₁ ⊆ X₀) (hγ₂ : Set.range ⇑γ₂ ⊆ X₀) : Set.range ⇑(γ₁.trans γ₂) ⊆ X₀

theorem DiSubtype.subtype_trans {X : dTopCat} {X₀ : Set ↑X} {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Set.range ⇑(γ₁.trans γ₂) ⊆ X₀) : (SubtypeDipath γ₁ ⋯).trans (SubtypeDipath γ₂ ⋯) = SubtypeDipath (γ₁.trans γ₂) hγ

theorem DiSubtype.subtype_reparam {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : SubtypeDipath (γ.reparam f hf₀ hf₁) ⋯ = (SubtypeDipath γ hγ).reparam f hf₀ hf₁

theorem DiSubtype.reparam_subset_of_subset {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Set.range ⇑(γ.reparam f hf₀ hf₁) ⊆ X₀

def DiSubtype.DihomotopyOfSubtype {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ γ' : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) (hγ' : Set.range ⇑γ' ⊆ X₀) {F : γ.Dihomotopy γ'} (hF : Set.range ⇑F ⊆ X₀) : (SubtypeDipath γ hγ).Dihomotopy (SubtypeDipath γ' hγ')

Lift a dihomotopy whose range lies inside X₀ to a dihomotopy of subtype dipaths.

Equations

• One or more equations did not get rendered due to their size.

theorem DiSubtype.dihomSubtype_of_dihom_range_subset {X : dTopCat} {X₀ : Set ↑X} {x y : ↑X} {γ γ' : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₀) (hγ' : Set.range ⇑γ' ⊆ X₀) {F : γ.Dihomotopy γ'} (hF : Set.range ⇑F ⊆ X₀) : ⟦SubtypeDipath γ hγ⟧ = ⟦SubtypeDipath γ' hγ'⟧