LeanPool.DirectedTopologyLean4.Dipath

structure Dipath {X : Type u} [DirectedSpace X] (x y : X) extends Path x y : Type u

A dipath is a path together with a proof that that path "is a dipath"

• toFun : ↑unitInterval → X
• continuous_toFun : Continuous self.toFun
• source' : self.toFun 0 = x
• target' : self.toFun 1 = y
• dipath_toPath : IsDipath self.toPath

@[implicit_reducible]

instance instCoeDipathPath {X : Type u} [DirectedSpace X] {x y : X} : Coe (Dipath x y) (Path x y)

Equations

• instCoeDipathPath = { coe := fun (γ : Dipath x y) => γ.toPath }

theorem Dipath.directed {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : DirectedMap.Directed γ.toContinuousMap

def Dipath.toDirectedMap {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : D(↑unitInterval,X)

Convert a dipath to its underlying directed map D(I, X).

Equations

• γ.toDirectedMap = { toContinuousMap := γ.toContinuousMap, directed_toFun := ⋯ }

@[implicit_reducible]

instance Dipath.instFunLike {X : Type u} [DirectedSpace X] {x y : X} : FunLike (Dipath x y) (↑unitInterval) X

Equations

• Dipath.instFunLike = { coe := fun (γ : Dipath x y) => γ.toFun, coe_injective := ⋯ }

instance Dipath.directedMapClass {X : Type u} [DirectedSpace X] {x y : X} : DirectedMapClass (Dipath x y) (↑unitInterval) X

theorem Dipath.ext {X : Type u} [DirectedSpace X] {x y : X} {γ₁ γ₂ : Dipath x y} : ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

theorem Dipath.ext_iff {X : Type u} [DirectedSpace X] {x y : X} {γ₁ γ₂ : Dipath x y} : γ₁ = γ₂ ↔ ⇑γ₁ = ⇑γ₂

def Dipath.ofIsDipath {X : Type u} [DirectedSpace X] {x y : X} {γ : Path x y} (hγ : IsDipath γ) : Dipath x y

Promote a path with a proof of directedness into a dipath.

Equations

• Dipath.ofIsDipath hγ = { toPath := γ, dipath_toPath := hγ }

def Dipath.ofDirectedMap {X : Type u} [DirectedSpace X] (f : D(↑unitInterval,X)) : Dipath (f 0) (f 1)

An directed map from I to a directed space can be turned into a dipath

Equations

• Dipath.ofDirectedMap f = { toFun := ⇑f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

@[simp]

theorem Dipath.coe_mk {X : Type u} [DirectedSpace X] {x y : X} (f : ↑unitInterval → X) (h₀ : Continuous f) (h₁ : { toFun := f, continuous_toFun := h₀ }.toFun 0 = x) (h₂ : { toFun := f, continuous_toFun := h₀ }.toFun 1 = y) (h₃ : IsDipath { toFun := f, continuous_toFun := h₀, source' := h₁, target' := h₂ }) : ⇑{ toFun := f, continuous_toFun := h₀, source' := h₁, target' := h₂, dipath_toPath := h₃ } = f

theorem Dipath.continuous {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : Continuous ⇑γ

@[simp]

theorem Dipath.source {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : γ 0 = x

@[simp]

theorem Dipath.target {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : γ 1 = y

def Dipath.simps.apply {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : ↑unitInterval → X

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

Equations

• Dipath.simps.apply γ = ⇑γ

theorem Dipath.coe_toContinuousMap {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : ⇑γ.toContinuousMap = ⇑γ

@[simp]

theorem Dipath.coe_toDirectedMap {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : ⇑γ.toDirectedMap = ⇑γ

@[implicit_reducible]

instance Dipath.hasUncurryDipath {X : Type u_1} {α : Type u_2} [DirectedSpace X] {x y : α → X} : Function.HasUncurry ((a : α) → Dipath (x a) (y a)) (α × ↑unitInterval) X

Any function φ : Π (a : α), Dipath (x a) (y a) can be seen as a function α × I → X.

Equations

• Dipath.hasUncurryDipath = { uncurry := fun (φ : (a : α) → Dipath (x a) (y a)) (p : α × ↑unitInterval) => (φ p.1) p.2 }

Properites about the range of dipaths

@[simp]

theorem Dipath.coe_range {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : Set.range ⇑γ = Set.range ⇑γ.toPath

theorem Dipath.range_eq_image {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : Set.range ⇑γ = ⇑γ.extend '' unitInterval

theorem Dipath.range_eq_image_I {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : Set.range ⇑γ = ⇑γ '' Set.Icc 0 1

theorem Dipath.image_extend_eq_image {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (a b : ↑unitInterval) : ⇑γ.extend '' Set.Icc ↑a ↑b = ⇑γ '' Set.Icc a b

Reflexive dipaths

def Dipath.refl {X : Type u} [DirectedSpace X] (x : X) : Dipath x x

The constant dipath from a point to itself

Equations

• Dipath.refl x = { toPath := Path.refl x, dipath_toPath := ⋯ }

@[simp]

theorem Dipath.refl_apply {X : Type u} [DirectedSpace X] (x : X) (x✝ : ↑unitInterval) : (refl x).toFun x✝ = x

@[simp]

theorem Dipath.refl_toFun {X : Type u} [DirectedSpace X] (x : X) (x✝ : ↑unitInterval) : (refl x) x✝ = x

theorem Dipath.refl_range {X : Type u} [DirectedSpace X] {a : X} : Set.range ⇑(refl a) = {a}

Concatenation of dipaths

noncomputable def Dipath.trans {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) : Dipath x z

Directed paths can be concatenated

Equations

• γ.trans γ' = { toPath := γ.trans γ'.toPath, dipath_toPath := ⋯ }

@[simp]

theorem Dipath.trans_to_path {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) : γ.trans γ'.toPath = (γ.trans γ').toPath

theorem Dipath.trans_apply {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) (t : ↑unitInterval) : (γ.trans γ') t = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩

theorem Dipath.trans_range {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) : Set.range ⇑(γ.trans γ') = Set.range ⇑γ ∪ Set.range ⇑γ'

theorem Dipath.trans_eval_at_half {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) : (γ.trans γ') (Fraction.ofPos ⋯) = y

Mapping dipaths

def Dipath.map {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {Y : Type u_1} [DirectedSpace Y] (f : D(X,Y)) : Dipath (f x) (f y)

Image of a dipath from x to y by a directed map

Equations

• γ.map f = { toPath := γ.map ⋯, dipath_toPath := ⋯ }

@[simp]

theorem Dipath.map_coe {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {Y : Type u_1} [DirectedSpace Y] (f : D(X,Y)) : ⇑(γ.map f) = ⇑f ∘ ⇑γ

@[simp]

theorem Dipath.map_trans {X : Type u} [DirectedSpace X] {x y z : X} (γ : Dipath x y) (γ' : Dipath y z) {Y : Type u_1} [DirectedSpace Y] (f : D(X,Y)) : (γ.trans γ').map f = (γ.map f).trans (γ'.map f)

@[simp]

theorem Dipath.map_id {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : γ.map (DirectedMap.id X) = γ

@[simp]

theorem Dipath.map_map {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {Y : Type u_1} [DirectedSpace Y] {Z : Type u_2} [DirectedSpace Z] (f : D(X,Y)) (g : D(Y,Z)) : (γ.map f).map g = γ.map (g.comp f)

Casting dipaths

def Dipath.cast {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : Dipath x' y'

Casting a dipath from x to y to a dipath from x' to y' when x' = x and y' = y

Equations

• γ.cast hx hy = { toFun := ⇑γ, continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

theorem Dipath.cast_apply {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {x' y' : X} (hx : x' = x) (hy : y' = y) (t : ↑unitInterval) : (γ.cast hx hy) t = γ t

@[simp]

theorem Dipath.trans_cast {X : Type u_1} [DirectedSpace X] {a₁ a₂ b₁ b₂ c₁ c₂ : X} (γ : Dipath a₂ b₂) (γ' : Dipath b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂) (hc : c₁ = c₂) : (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc

@[simp]

theorem Dipath.cast_coe {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : ⇑(γ.cast hx hy) = ⇑γ

theorem Dipath.cast_range {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : Set.range ⇑(γ.cast hx hy) = Set.range ⇑γ

theorem Dipath.cast_image {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {x' y' : X} (hx : x' = x) (hy : y' = y) (a b : ℝ) : ⇑(γ.cast hx hy).extend '' Set.Icc a b = ⇑γ.extend '' Set.Icc a b

theorem Dipath.dipath_of_directed_map_of_to_dimap {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : ofDirectedMap γ.toDirectedMap = γ.cast ⋯ ⋯

Reparametrising a path

def Dipath.subparam {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) : Dipath (γ (f 0)) (γ (f 1))

Reparametrize a dipath by precomposing it with a directed self-map of the unit interval.

Equations

• γ.subparam f = { toFun := ⇑γ ∘ ⇑f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

theorem Dipath.subparam_range {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) : Set.range ⇑(γ.subparam f) ⊆ Set.range ⇑γ

def Dipath.reparam {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Dipath x y

Given a dipath γ and a dimap f : I → I where f 0 = 0 and f 1 = 1, γ.reparam f is the dipath defined by γ ∘ f.

Equations

• γ.reparam f hf₀ hf₁ = (γ.subparam f).cast ⋯ ⋯

@[simp]

theorem Dipath.coe_to_fun {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ⇑(γ.reparam f hf₀ hf₁) = ⇑γ ∘ ⇑f

@[simp]

theorem Dipath.reparam_id {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) : γ.reparam (DirectedMap.id ↑unitInterval) ⋯ ⋯ = γ

theorem Dipath.range_reparam {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Set.range ⇑(γ.reparam f hf₀ hf₁) = Set.range ⇑γ

def Dipath.dipathProduct {X : Type u} [DirectedSpace X] {Y : Type u_1} [DirectedSpace Y] {x₀ x₁ : X} {y₀ y₁ : Y} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath y₀ y₁) : Dipath (x₀, y₀) (x₁, y₁)

Two dipaths together form a dipath in the product space

Equations

• γ₁.dipathProduct γ₂ = { toFun := fun (t : ↑unitInterval) => (γ₁ t, γ₂ t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

def Dipath.ofProductFst {X : Type u} [DirectedSpace X] {Y : Type u_1} [DirectedSpace Y] {x₀ x₁ : X} {y₀ y₁ : Y} (γ : Dipath (x₀, y₀) (x₁, y₁)) : Dipath x₀ x₁

Given a directed path in a product space, we can project it to its first coordinate to obtain a directed path

Equations

• γ.ofProductFst = { toPath := γ.map ⋯, dipath_toPath := ⋯ }

def Dipath.ofProductSnd {X : Type u} [DirectedSpace X] {Y : Type u_1} [DirectedSpace Y] {x₀ x₁ : X} {y₀ y₁ : Y} (γ : Dipath (x₀, y₀) (x₁, y₁)) : Dipath y₀ y₁

Given a directed path in a product space, we can project it to its second coordinate to obtain a directed path

Equations

• γ.ofProductSnd = { toPath := γ.map ⋯, dipath_toPath := ⋯ }