LeanPool.DirectedTopologyLean4.DirectedHomotopy

structure DirectedMap.Dihomotopy {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f₀ f₁ : D(X,Y)) extends D(↑unitInterval × X,Y) : Type (max u v)

DirectedMap.Dihomotopy f₀ f₁ is the type of directed homotopies from f₀ to f₁.

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous self.toFun
• directed_toFun : Directed self.toContinuousMap
• map_zero_left (x : X) : self.toFun (0, x) = f₀.toFun x
• map_one_left (x : X) : self.toFun (1, x) = f₁.toFun x

class DirectedMap.DihomotopyLike {X : outParam (Type u_1)} {Y : outParam (Type u_2)} [DirectedSpace X] [DirectedSpace Y] (F : Type u_3) (f₀ f₁ : outParam D(X,Y)) [FunLike F (↑unitInterval × X) Y] extends DirectedMapClass F (↑unitInterval × X) Y : Prop

DirectedMap.DihomotopyLike F f₀ f₁ states that F is a type of homotopies between f₀ and f₁

• map_continuous (f : F) : Continuous ⇑f
• map_directed (f : F) : DirectedMap.Directed ↑f
• map_zero_left (f : F) (x : X) : f (0, x) = f₀ x
• map_one_left (f : F) (x : X) : f (1, x) = f₁ x

@[implicit_reducible]

instance DirectedMap.Dihomotopy.instFunLike {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} : FunLike (f₀.Dihomotopy f₁) (↑unitInterval × X) Y

Equations

• DirectedMap.Dihomotopy.instFunLike = { coe := fun (f : f₀.Dihomotopy f₁) => f.toFun, coe_injective := ⋯ }

instance DirectedMap.Dihomotopy.instDihomotopyLike {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} : DihomotopyLike (f₀.Dihomotopy f₁) f₀ f₁

theorem DirectedMap.Dihomotopy.ext {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {f g : f₀.Dihomotopy f₁} (h : ∀ (x : ↑unitInterval × X), f x = g x) : f = g

theorem DirectedMap.Dihomotopy.ext_iff {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {f g : f₀.Dihomotopy f₁} : f = g ↔ ∀ (x : ↑unitInterval × X), f x = g x

def DirectedMap.Dihomotopy.Simps.apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : ↑unitInterval × X → Y

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• DirectedMap.Dihomotopy.Simps.apply F = ⇑F

@[simp]

theorem DirectedMap.Dihomotopy.apply_zero {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (a : X) : F (0, a) = f₀ a

@[simp]

theorem DirectedMap.Dihomotopy.apply_one {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (a : X) : F (1, a) = f₁ a

@[simp]

theorem DirectedMap.Dihomotopy.coe_to_continuous_map {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : ⇑F.toContinuousMap = ⇑F

@[simp]

theorem DirectedMap.Dihomotopy.coe_to_directed_map {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : ⇑F.toDirectedMap = ⇑F

def DirectedMap.Dihomotopy.curry {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : ↑unitInterval → D(X,Y)

Currying a dihomotopy to a map fron I to D(X,Y).

Equations

• F.curry t = (↑F).prodConstFst t

@[simp]

theorem DirectedMap.Dihomotopy.curry_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (t : ↑unitInterval) (x : X) : (F.curry t) x = F (t, x)

def DirectedMap.Dihomotopy.currySnd {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : X → D(↑unitInterval,Y)

Currying a dihomotopy to a map fron X to D(I,Y).

Equations

• F.currySnd x = (↑F).prodConstSnd x

@[simp]

theorem DirectedMap.Dihomotopy.curry_snd_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (x : X) (t : ↑unitInterval) : (F.currySnd x) t = F (t, x)

def DirectedMap.Dihomotopy.homToDihom {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : (↑f₀).Homotopy ↑f₁) (HF : Directed ↑F) : f₀.Dihomotopy f₁

Promote a continuous-map homotopy together with a proof of directedness to a dihomotopy.

Equations

• DirectedMap.Dihomotopy.homToDihom F HF = { toContinuousMap := F.toContinuousMap, directed_toFun := HF, map_zero_left := ⋯, map_one_left := ⋯ }

def DirectedMap.Dihomotopy.dihomToHom {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) : (↑f₀).Homotopy ↑f₁

Forget the directedness of a dihomotopy to obtain the underlying continuous-map homotopy.

Equations

• F.dihomToHom = { toContinuousMap := F.toContinuousMap, map_zero_left := ⋯, map_one_left := ⋯ }

@[implicit_reducible]

instance DirectedMap.Dihomotopy.coeDihomToHom {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} : Coe (f₀.Dihomotopy f₁) ((↑f₀).Homotopy ↑f₁)

Equations

• DirectedMap.Dihomotopy.coeDihomToHom = { coe := fun (F : f₀.Dihomotopy f₁) => F.dihomToHom }

Evaluating dihomotopies at intermidiate points

def DirectedMap.Dihomotopy.evalAtLeft {X : Type u} [DirectedSpace X] {f g : D(↑unitInterval,X)} (F : f.Dihomotopy g) (t : ↑unitInterval) : Dipath (F (t, 0)) (F (t, 1))

Evaluating a dipath homotopy at an intermediate point in the left coordinate, giving us a dipath.

Equations

• F.evalAtLeft t = { toFun := ⇑(F.curry t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

def DirectedMap.Dihomotopy.evalAtRight {X : Type u_1} {Y : Type u_2} [DirectedSpace X] [DirectedSpace Y] {f g : D(X,Y)} (H : f.Dihomotopy g) (x : X) : Dipath (f x) (g x)

Given a dihomotopy H: f ∼ g, get the dipath traced by the point x as it moves from f x to g x

Equations

• H.evalAtRight x = { toFun := fun (t : ↑unitInterval) => H (t, x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

theorem DirectedMap.Dihomotopy.directed_refl {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) : Directed ↑(ContinuousMap.Homotopy.refl ↑f)

Given a directed map f, we can define a Dihomotopy f f by F (t, x) = f x

def DirectedMap.Dihomotopy.refl {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) : f.Dihomotopy f

The trivial reflexive dihomotopy F (t, x) = f x.

Equations

• DirectedMap.Dihomotopy.refl f = DirectedMap.Dihomotopy.homToDihom (ContinuousMap.Homotopy.refl ↑f) ⋯

theorem DirectedMap.Dihomotopy.refl_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (x : ↑unitInterval × X) : (refl f) x = f x.2

theorem DirectedMap.Dihomotopy.refl_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (x : ↑unitInterval × X) : (refl f) x = f x.2

@[implicit_reducible]

instance DirectedMap.Dihomotopy.instInhabitedId {X : Type u} [DirectedSpace X] : Inhabited ((DirectedMap.id X).Dihomotopy (DirectedMap.id X))

Equations

• DirectedMap.Dihomotopy.instInhabitedId = { default := DirectedMap.Dihomotopy.refl (DirectedMap.id X) }

def DirectedMap.Dihomotopy.FirstPartStretch {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) {T : ↑unitInterval} (hT : γ T = unitIAux.halfI) (ht₀ : ↑t₀ ≤ 2⁻¹) : Dipath ⟨2 * ↑t₀, ⋯⟩ 1

The first half of a split dipath, stretched to the interval [2 t₀, 1].

Equations

• DirectedMap.Dihomotopy.FirstPartStretch γ hT ht₀ = { toFun := ⇑((SplitDipath.FirstPart γ T).stretchUp ⋯), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

def DirectedMap.Dihomotopy.SecondPartStretch {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) {T : ↑unitInterval} (hT : γ T = unitIAux.halfI) (ht₁ : 2⁻¹ ≤ ↑t₁) : Dipath 0 ⟨2 * ↑t₁ - 1, ⋯⟩

The second half of a split dipath, stretched to the interval [0, 2 t₁ - 1].

Equations

• DirectedMap.Dihomotopy.SecondPartStretch γ hT ht₁ = { toFun := ⇑((SplitDipath.SecondPart γ T).stretchDown ⋯), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

theorem DirectedMap.Dihomotopy.trans_apply_half_left {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) (t : ↑unitInterval) (x : X) (ht : t = unitIAux.halfI) : (F.dihomToHom.trans G.dihomToHom) (t, x) = F (1, x)

theorem DirectedMap.Dihomotopy.trans_apply_half_right {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) (t : ↑unitInterval) (x : X) (ht : t = unitIAux.halfI) : (F.dihomToHom.trans G.dihomToHom) (t, x) = G (0, x)

theorem DirectedMap.Dihomotopy.trans_apply_left {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) (t : ↑unitInterval) (x : X) (ht : ↑t ≤ 2⁻¹) : (F.dihomToHom.trans G.dihomToHom) (t, x) = F (⟨2 * ↑t, ⋯⟩, x)

theorem DirectedMap.Dihomotopy.trans_apply_right {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) (t : ↑unitInterval) (x : X) (ht : 2⁻¹ ≤ ↑t) : (F.dihomToHom.trans G.dihomToHom) (t, x) = G (⟨2 * ↑t - 1, ⋯⟩, x)

theorem DirectedMap.Dihomotopy.trans_first_case {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) {a₀ a₁ : ↑unitInterval × X} {γ : Path a₀ a₁} (γ_dipath : IsDipath γ) (ht₁ : ↑a₁.1 ≤ 2⁻¹) : IsDipath (γ.map ⋯)

theorem DirectedMap.Dihomotopy.trans_second_case {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) {a₀ a₁ : ↑unitInterval × X} {γ : Path a₀ a₁} (γ_dipath : IsDipath γ) (ht₀ : 2⁻¹ ≤ ↑a₀.1) : IsDipath (γ.map ⋯)

noncomputable def DirectedMap.Dihomotopy.trans {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) : f₀.Dihomotopy f₂

Given Dihomotopy f₀ f₁ and Dihomotopy f₁ f₂, we can define a Dihomotopy f₀ f₂ by putting the first dihomotopy on [0, 1/2] and the second on [1/2, 1].

Equations

• F.trans G = DirectedMap.Dihomotopy.homToDihom (F.dihomToHom.trans G.dihomToHom) ⋯

theorem DirectedMap.Dihomotopy.trans_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} (F : f₀.Dihomotopy f₁) (G : f₁.Dihomotopy f₂) (x : ↑unitInterval × X) : (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

def DirectedMap.Dihomotopy.cast {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : g₀.Dihomotopy g₁

Casting a Dihomotopy f₀ f₁ to a Dihomotopy g₀ g₁ where f₀ = g₀ and f₁ = g₁.

Equations

• F.cast h₀ h₁ = { toFun := ⇑F, continuous_toFun := ⋯, directed_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

theorem DirectedMap.Dihomotopy.cast_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

theorem DirectedMap.Dihomotopy.cast_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.Dihomotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

def DirectedMap.Dihomotopy.hcomp {X : Type u} {Y : Type v} {Z : Type w} [DirectedSpace X] [DirectedSpace Y] [DirectedSpace Z] {f₀ f₁ : D(X,Y)} {g₀ g₁ : D(Y,Z)} (F : f₀.Dihomotopy f₁) (G : g₀.Dihomotopy g₁) : (g₀.comp f₀).Dihomotopy (g₁.comp f₁)

If we have a Dihomotopy f₀ f₁ and a Dihomotopy g₀ g₁, then we can compose them and get a Dihomotopy (g₀.comp f₀) (g₁.comp f₁).

Equations

• F.hcomp G = DirectedMap.Dihomotopy.homToDihom (DirectedMap.Dihomotopy.Homotopy.hcomp'✝ F.dihomToHom G.dihomToHom) ⋯

theorem DirectedMap.Dihomotopy.hcomp_apply {X : Type u} {Y : Type v} {Z : Type w} [DirectedSpace X] [DirectedSpace Y] [DirectedSpace Z] {f₀ f₁ : D(X,Y)} {g₀ g₁ : D(Y,Z)} (F : f₀.Dihomotopy f₁) (G : g₀.Dihomotopy g₁) (p : ↑unitInterval × X) : (F.hcomp G) p = G.dihomToHom (p.1, F.dihomToHom p)

theorem DirectedMap.Dihomotopy.hcomp_toFun {X : Type u} {Y : Type v} {Z : Type w} [DirectedSpace X] [DirectedSpace Y] [DirectedSpace Z] {f₀ f₁ : D(X,Y)} {g₀ g₁ : D(Y,Z)} (F : f₀.Dihomotopy f₁) (G : g₀.Dihomotopy g₁) (p : ↑unitInterval × X) : (F.hcomp G) p = G.dihomToHom (p.1, F.dihomToHom p)

def DirectedMap.PreDihomotopic {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f₀ f₁ : D(X,Y)) : Prop

Given directed maps f₀ and f₁, we say f₀ and f₁ are PreDihomotopic if there exists a Dihomotopy f₀ f₁.

Equations

• f₀.PreDihomotopic f₁ = Nonempty (f₀.Dihomotopy f₁)

def DirectedMap.Dihomotopic {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f₀ f₁ : D(X,Y)) : Prop

Given directed maps f₀ and f₁, we say f₀ and f₁ are Dihomotopic if there is a chain of PreDihomotopic maps leading from f₀ to f₁. In other words, Dihomotopic is the equivalence relation generated by PreDihomotopic.

Equations

• f₀.Dihomotopic f₁ = Relation.EqvGen DirectedMap.PreDihomotopic f₀ f₁

theorem DirectedMap.Dihomotopic.equivalence {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] : Equivalence Dihomotopic

structure DirectedMap.DihomotopyWith {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f₀ f₁ : D(X,Y)) (P : D(X,Y) → Prop) extends f₀.Dihomotopy f₁ : Type (max u v)

The type of dihomotopies between f₀ f₁ : D(X,Y), where the intermediate maps satisfy the predicate P : D(X,Y) → Prop

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous self.toFun
• directed_toFun : Directed self.toContinuousMap
• map_zero_left (x : X) : self.toFun (0, x) = f₀.toFun x
• map_one_left (x : X) : self.toFun (1, x) = f₁.toFun x
• prop' (t : ↑unitInterval) : P (self.prodConstFst t)

@[implicit_reducible]

instance DirectedMap.DihomotopyWith.instFunLike {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} : FunLike (f₀.DihomotopyWith f₁ P) (↑unitInterval × X) Y

Equations

• DirectedMap.DihomotopyWith.instFunLike = { coe := fun (F : f₀.DihomotopyWith f₁ P) => ⇑F.toDihomotopy, coe_injective := ⋯ }

instance DirectedMap.DihomotopyWith.instDihomotopyLike {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} : DihomotopyLike (f₀.DihomotopyWith f₁ P) f₀ f₁

theorem DirectedMap.DihomotopyWith.coeFn_injective {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} : Function.Injective DFunLike.coe

theorem DirectedMap.DihomotopyWith.ext {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} {F G : f₀.DihomotopyWith f₁ P} (h : ∀ (x : ↑unitInterval × X), F x = G x) : F = G

theorem DirectedMap.DihomotopyWith.ext_iff {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} {F G : f₀.DihomotopyWith f₁ P} : F = G ↔ ∀ (x : ↑unitInterval × X), F x = G x

def DirectedMap.DihomotopyWith.Simps.apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) : ↑unitInterval × X → Y

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• DirectedMap.DihomotopyWith.Simps.apply F = ⇑F

theorem DirectedMap.DihomotopyWith.continuous {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) : Continuous ⇑F

@[simp]

theorem DirectedMap.DihomotopyWith.apply_zero {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) (x : X) : F (0, x) = f₀ x

@[simp]

theorem DirectedMap.DihomotopyWith.apply_one {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) (x : X) : F (1, x) = f₁ x

@[simp]

theorem DirectedMap.DihomotopyWith.coe_to_continuous_map {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) : ⇑F.toContinuousMap = ⇑F

@[simp]

theorem DirectedMap.DihomotopyWith.coe_to_dihomotopy {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) : ⇑F.toDihomotopy = ⇑F

theorem DirectedMap.DihomotopyWith.prop {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {P : D(X,Y) → Prop} (F : f₀.DihomotopyWith f₁ P) (t : ↑unitInterval) : P (F.curry t)

def DirectedMap.DihomotopyWith.refl {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} (f : D(X,Y)) (hf : P f) : f.DihomotopyWith f P

Given a directed map f, and a proof h : P f, we can define a DihomotopyWith f f P by F (t, x) = f x

Equations

• DirectedMap.DihomotopyWith.refl f hf = { toDihomotopy := DirectedMap.Dihomotopy.refl f, prop' := ⋯ }

theorem DirectedMap.DihomotopyWith.refl_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} (f : D(X,Y)) (hf : P f) (x : ↑unitInterval × X) : (refl f hf) x = f x.2

theorem DirectedMap.DihomotopyWith.refl_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} (f : D(X,Y)) (hf : P f) (x : ↑unitInterval × X) : (refl f hf) x = f x.2

@[implicit_reducible]

instance DirectedMap.DihomotopyWith.instInhabitedIdTrue {X : Type u} [DirectedSpace X] : Inhabited ((DirectedMap.id X).DihomotopyWith (DirectedMap.id X) fun (x : D(X,X)) => True)

Equations

• DirectedMap.DihomotopyWith.instInhabitedIdTrue = { default := DirectedMap.DihomotopyWith.refl (DirectedMap.id X) trivial }

noncomputable def DirectedMap.DihomotopyWith.trans {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} {f₀ f₁ f₂ : D(X,Y)} (F : f₀.DihomotopyWith f₁ P) (G : f₁.DihomotopyWith f₂ P) : f₀.DihomotopyWith f₂ P

Given DihomotopyWith f₀ f₁ P and DihomotopyWith f₁ f₂ P, we can define a DihomotopyWith f₀ f₂ P by putting the first dihomotopy on [0, 1/2] and the second on [1/2, 1].

Equations

• F.trans G = { toDihomotopy := F.trans G.toDihomotopy, prop' := ⋯ }

theorem DirectedMap.DihomotopyWith.trans_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} {f₀ f₁ f₂ : D(X,Y)} (F : f₀.DihomotopyWith f₁ P) (G : f₁.DihomotopyWith f₂ P) (x : ↑unitInterval × X) : (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

def DirectedMap.DihomotopyWith.cast {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : g₀.DihomotopyWith g₁ P

Casting a DihomotopyWith f₀ f₁ P to a DihomotopyWith g₀ g₁ P where f₀ = g₀ and f₁ = g₁.

Equations

• F.cast h₀ h₁ = { toDihomotopy := F.cast h₀ h₁, prop' := ⋯ }

theorem DirectedMap.DihomotopyWith.cast_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

theorem DirectedMap.DihomotopyWith.cast_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {P : D(X,Y) → Prop} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

def DirectedMap.PreDihomotopicWith {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (P : D(X,Y) → Prop) (f₀ f₁ : D(X,Y)) : Prop

Given directed maps f₀ and f₁, we say f₀ and f₁ are pre_dihomotopic with respect to the predicate P if there exists a DihomotopyWith f₀ f₁ P.

Equations

• DirectedMap.PreDihomotopicWith P f₀ f₁ = Nonempty (f₀.DihomotopyWith f₁ P)

def DirectedMap.DihomotopicWith {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (P : D(X,Y) → Prop) (f₀ f₁ : D(X,Y)) : Prop

DihomotopicWith is the equivalence relation generated by PreDihomotopicWith.

Equations

• DirectedMap.DihomotopicWith P f₀ f₁ = Relation.EqvGen (DirectedMap.PreDihomotopicWith P) f₀ f₁

@[reducible, inline]

abbrev DirectedMap.DihomotopyRel {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f₀ f₁ : D(X,Y)) (S : Set X) : Type (max u v)

A DihomotopyRel f₀ f₁ S is a dihomotopy between f₀ and f₁ which is fixed on the points in S.

Equations

• f₀.DihomotopyRel f₁ S = f₀.DihomotopyWith f₁ fun (f : D(X,Y)) => ∀ x ∈ S, f x = f₀ x

theorem DirectedMap.DihomotopyRel.eq_fst {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {S : Set X} (F : f₀.DihomotopyRel f₁ S) (t : ↑unitInterval) {x : X} (hx : x ∈ S) : F (t, x) = f₀ x

theorem DirectedMap.DihomotopyRel.eq_snd {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {S : Set X} (F : f₀.DihomotopyRel f₁ S) (t : ↑unitInterval) {x : X} (hx : x ∈ S) : F (t, x) = f₁ x

theorem DirectedMap.DihomotopyRel.fst_eq_snd {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ : D(X,Y)} {S : Set X} (F : f₀.DihomotopyRel f₁ S) {x : X} (hx : x ∈ S) : f₀ x = f₁ x

def DirectedMap.DihomotopyRel.refl {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (S : Set X) : f.DihomotopyRel f S

Given a map f : D(X,Y) and a set S, we can define a DihomotopyRel f f S by setting F (t, x) = f x for all t. This is defined using DihomotopyWith.refl, but with the proof filled in.

Equations

• DirectedMap.DihomotopyRel.refl f S = DirectedMap.DihomotopyWith.refl f ⋯

theorem DirectedMap.DihomotopyRel.refl_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (S : Set X) (x : ↑unitInterval × X) : (refl f S) x = f x.2

theorem DirectedMap.DihomotopyRel.refl_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (S : Set X) (x : ↑unitInterval × X) : (refl f S) x = f x.2

noncomputable def DirectedMap.DihomotopyRel.trans {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} {S : Set X} (F : f₀.DihomotopyRel f₁ S) (G : f₁.DihomotopyRel f₂ S) : f₀.DihomotopyRel f₂ S

Given DihomotopyRel f₀ f₁ S and DihomotopyRel f₁ f₂ S, we can define a DihomotopyRel f₀ f₂ S by putting the first dihomotopy on [0, 1/2] and the second on [1/2, 1].

Equations

• F.trans G = { toDihomotopy := F.trans G.toDihomotopy, prop' := ⋯ }

theorem DirectedMap.DihomotopyRel.trans_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {f₀ f₁ f₂ : D(X,Y)} {S : Set X} (F : f₀.DihomotopyRel f₁ S) (G : f₁.DihomotopyRel f₂ S) (x : ↑unitInterval × X) : (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

def DirectedMap.DihomotopyRel.cast {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {S : Set X} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : g₀.DihomotopyRel g₁ S

Casting a DihomotopyRel f₀ f₁ S to a DihomotopyRel g₀ g₁ S where f₀ = g₀ and f₁ = g₁.

Equations

• F.cast h₀ h₁ = { toDihomotopy := F.cast h₀ h₁, prop' := ⋯ }

theorem DirectedMap.DihomotopyRel.cast_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {S : Set X} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

theorem DirectedMap.DihomotopyRel.cast_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {S : Set X} {f₀ f₁ g₀ g₁ : D(X,Y)} (F : f₀.DihomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (F.cast h₀ h₁) a = F a

def DirectedMap.PreDihomotopicRel {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (S : Set X) (f₀ f₁ : D(X,Y)) : Prop

Given directed maps f₀ and f₁, we say f₀ and f₁ are PreDihomotopic relative to a set S if there exists a DihomotopyRel f₀ f₁ S.

Equations

• DirectedMap.PreDihomotopicRel S f₀ f₁ = Nonempty (f₀.DihomotopyRel f₁ S)

def DirectedMap.DihomotopicRel {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] (S : Set X) (f₀ f₁ : D(X,Y)) : Prop

DihomotopicRel is the equivalence relation generated by PreDihomotopicRel.

Equations

• DirectedMap.DihomotopicRel S f₀ f₁ = Relation.EqvGen (DirectedMap.PreDihomotopicRel S) f₀ f₁

theorem DirectedMap.DihomotopicRel.equivalence {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {S : Set X} : Equivalence fun (f g : D(X,Y)) => DihomotopicRel S f g