LeanPool.WhiteheadTheorem.HEP.Retract #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.HEP.Retract.

source

structure StrongDeformRetr (X : Type u_1) [TopologicalSpace X] (A : Set X) :

Type u_1

A strong deformation retraction from X to its subset A

r : C(X, X)
The retraction map
r_range : Set.range ⇑self.r ⊆ A
r sends all of X into A
H : (ContinuousMap.id X).HomotopyRel self.r A
A homotopy H rel A, where H₀ is the identity map on X, and H₁ = r.

Instances For

source

theorem Cube.splitAtLastComm_inclToBot_eq {n : ℕ} :

⇑splitAtLastComm ∘ ⇑inclToBot = fun (x : Fin n → ↑unitInterval) => (x, 0)

source

theorem Cube.inclToBot_discardLast_mem_boundary {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) :

inclToBot (discardLast y) ∈ boundary (Fin (n + 1))

source

theorem Cube.inclToBot_discardLast_eq_of {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) (hz : y (Fin.last n) = 0) :

inclToBot (discardLast y) = y

(y₀, y₁, …, yₙ₋₁, yₙ) ↦ (y₀, y₁, …, yₙ₋₁) ↦ (y₀, y₁, …, yₙ₋₁, 0) does nothing if yₙ = 0.

source

theorem Cube.inclToBoundaryJarBot_discardLast_eq_of {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) (hz : y (Fin.last n) = 0) :

↑(inclToBoundaryJarBot (discardLast y)) = y

source

theorem Cube.splitAtLastComm_inclToSides_eq {n : ℕ} :

⇑splitAtLastComm ∘ ⇑inclToSides = Prod.map (⇑(boundaryIncl n)) id

source

noncomputable def Cube.projToBoundary {n : ℕ} :

(Fin (n + 1) → ↑unitInterval) → ↑(boundary (Fin (n + 1)))

Project the $(n+1)$-dimensional cube to its boundary ∂I^(n+1). This fixes every point on the boundary, and maps other points to the default value 0. This (non-continuous) function is convenient for diagram-chasing when applying the homotopy extension property in retrToBoundaryJar. This function is noncomputable due to Real.decidableEq.

Equations

Cube.projToBoundary y = if x : y ∈ Cube.boundary (Fin (n + 1)) then ⟨y, x⟩ else ⟨0, ⋯⟩

Instances For

source

theorem Cube.projToBoundary_eq_of_mem_boundary {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) (hy : y ∈ boundary (Fin (n + 1))) :

↑(projToBoundary y) = y

projToBoundary y does nothing if y is already in the boundary.

source

noncomputable def Cube.projToSides {n : ℕ} :

(Fin (n + 1 + 1) → ↑unitInterval) → ↑(boundary (Fin (n + 1))) × ↑unitInterval

Project the $(n+2)$-dimensional cube to its sides (∂I^(n+1)) × I (the closure of the complement of the top and bottom faces of the boundary). Since ∂I^0 = ∅, the cube shoule be at least 2-dimensional.

Equations

Cube.projToSides = Prod.map Cube.projToBoundary id ∘ ⇑Cube.splitAtLastComm

Instances For

source

theorem Cube.inclToSides_projToSides_eq_of {n : ℕ} (y : Fin (n + 1 + 1) → ↑unitInterval) (hs : (splitAtLast y).2 ∈ boundary (Fin (n + 1))) :

inclToSides (projToSides y) = y

source

theorem Cube.inclToBoundaryJarSides_projToSides_eq_of {n : ℕ} (y : Fin (n + 1 + 1) → ↑unitInterval) (hs : (splitAtLast y).2 ∈ boundary (Fin (n + 1))) :

↑(inclToBoundaryJarSides (projToSides y)) = y

source

noncomputable def Cube.retrToBoundaryJar (n : ℕ) :

{ r' : C(Fin (n + 1) → ↑unitInterval, ↑(boundaryJar (n + 1))) // ∀ y ∈ boundaryJar (n + 1), ↑(r' y) = y }

A retraction from I^n to ⊔I^n, for n ≥ 1.

Equations

Cube.retrToBoundaryJar n = ⟨(Classical.choose ⋯).comp ↑Cube.splitAtLastComm, ⋯⟩

Instances For

source

noncomputable def Cube.strongDeformRetrToBoundaryJar (n : ℕ) :

StrongDeformRetr (Fin (n + 1) → ↑unitInterval) (boundaryJar (n + 1))

A strong deformation retraction from I^n to ⊔I^n, for n ≥ 1. I'm writing down the formula for each coordinate because:

failed to synthesize ContinuousSMul (↑I) (Fin (n + 1) → ↑I)
Using Convex requires going to a subset of ℝ^(n+1) and back (although Convex ℝ I is very helpful)

Equations

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

Instances For

source

def Cube.deformRetrToBot {n : ℕ} :

C(↑unitInterval × (Fin (n + 1) → ↑unitInterval), Fin (n + 1) → ↑unitInterval)

Deformation retraction from the cube to its bottom face

Equations

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

Instances For

source

theorem Cube.deformRetrToBot_apply_bot {n : ℕ} (t : ↑unitInterval) {y : Fin (n + 1) → ↑unitInterval} (hy : y (Fin.last n) = 0) :

deformRetrToBot (t, y) (Fin.last n) = 0

If y is in the bottom face of the cube, then deformRetrToBot ⟨t, y⟩ is in the bottom face for all t.

source

theorem Cube.deformRetrToBot_apply_sides {n : ℕ} (t : ↑unitInterval) {y : Fin (n + 1) → ↑unitInterval} (hy : (splitAtLast y).2 ∈ boundary (Fin n)) :

(splitAtLast (deformRetrToBot (t, y))).2 ∈ boundary (Fin n)

If y is in the sides (the closure of the complement of the top and bottom faces of the boundary) of the cube, then deformRetrToBot ⟨t, y⟩ is in the sides for all t.

source

def Cube.boundaryJarDeformRetrToBot {n : ℕ} :