LeanPool.WhiteheadTheorem.Shapes.Cube

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.Cube.

def Cube.boundaryJar (n : ℕ) : Set (Fin n → ↑unitInterval)

Cube.boundaryJar (n + 1) = ∂Iⁿ × I ∪ Iⁿ × {0} ⊆ Iⁿ⁺¹

Equations

• Cube.boundaryJar 0 = ∅
• Cube.boundaryJar n_2.succ = {y : Fin (n_2 + 1) → ↑unitInterval | (∃ (i : Fin (n_2 + 1)), y i = 0 ∨ y i = 1) ∧ (y (Fin.last n_2) = 1 → ∃ i < Fin.last n_2, y i = 0 ∨ y i = 1)}

def Cube.boundaryLid (n : ℕ) : Set (Fin n → ↑unitInterval)

Cube.boundaryLid (n + 1) = Iⁿ × {1} ⊆ Iⁿ⁺¹

Equations

• Cube.boundaryLid 0 = ∅
• Cube.boundaryLid n_2.succ = {y : Fin (n_2 + 1) → ↑unitInterval | y (Fin.last n_2) = 1}

def Topology.Homotopy.«term∂I^_» : Lean.ParserDescr

«term∂I^_»

Equations

• Topology.Homotopy.«term∂I^_» = Lean.ParserDescr.node `Topology.Homotopy.«term∂I^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∂I^") (Lean.ParserDescr.cat `term 0))

def Topology.Homotopy.«term⊔I^_» : Lean.ParserDescr

«term⊔I^_»

Equations

• Topology.Homotopy.«term⊔I^_» = Lean.ParserDescr.node `Topology.Homotopy.«term⊔I^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊔I^") (Lean.ParserDescr.cat `term 0))

def Cube.boundaryIncl (n : ℕ) : C(↑(boundary (Fin n)), Fin n → ↑unitInterval)

boundaryIncl

Equations

• Cube.boundaryIncl n = { toFun := Subtype.val, continuous_toFun := ⋯ }

def Cube.boundaryJarIncl (n : ℕ) : C(↑(boundaryJar n), Fin n → ↑unitInterval)

boundaryJarIncl

Equations

• Cube.boundaryJarIncl n = { toFun := Subtype.val, continuous_toFun := ⋯ }

instance Cube.isEmpty_boundary_zero : IsEmpty ↑(boundary (Fin 0))

instance Cube.isEmpty_boundaryJar_zero : IsEmpty ↑(boundaryJar 0)

theorem Cube.boundaryJar_subset_boundary (n : ℕ) : boundaryJar n ⊆ boundary (Fin n)

def Cube.boundaryJarInclToBoundary (n : ℕ) : C(↑(boundaryJar n), ↑(boundary (Fin n)))

boundaryJarInclToBoundary

Equations

• Cube.boundaryJarInclToBoundary n = { toFun := fun (x : ↑(Cube.boundaryJar n)) => match x with | ⟨y, hy⟩ => ⟨y, ⋯⟩, continuous_toFun := ⋯ }

theorem Cube.mem_boundaryJar_of_lt_last {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) (hy : ∃ i < Fin.last n, y i = 0 ∨ y i = 1) : y ∈ boundaryJar (n + 1)

theorem Cube.mem_boundaryJar_of_exists_eq_zero {n : ℕ} (y : Fin n → ↑unitInterval) (hy : ∃ (i : Fin n), y i = 0) : y ∈ boundaryJar n

theorem Cube.mem_boundaryLid_or_mem_boundaryJar_of_mem_boundary {n : ℕ} (y : Fin n → ↑unitInterval) (hy : y ∈ boundary (Fin n)) : y ∈ boundaryLid n ∨ y ∈ boundaryJar n

@[implicit_reducible]

instance Cube.uniqueBoundaryJarOne : Unique ↑(boundaryJar 1)

⊔I^1 = {0} is a singleton

Equations

• Cube.uniqueBoundaryJarOne = { default := ⟨0, Cube.uniqueBoundaryJarOne._proof_1⟩, uniq := Cube.uniqueBoundaryJarOne._proof_2 }

def Cube.homeoNeqLast {n : ℕ} : (Fin n → ↑unitInterval) ≃ₜ ({ j : Fin (n + 1) // j ≠ Fin.last n } → ↑unitInterval)

homeoNeqLast

Equations

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

def Cube.splitAtLast {n : ℕ} : (Fin (n + 1) → ↑unitInterval) ≃ₜ ↑unitInterval × (Fin n → ↑unitInterval)

A homeomorphism that sends (y₀, y₁, …, yₙ₋₁, yₙ) to (yₙ, (y₀, y₁, …, yₙ₋₁))

Equations

• Cube.splitAtLast = (Cube.splitAt (Fin.last n)).trans ((Homeomorph.refl ↑unitInterval).prodCongr Cube.homeoNeqLast.symm)

def Cube.splitAtLastComm {n : ℕ} : (Fin (n + 1) → ↑unitInterval) ≃ₜ (Fin n → ↑unitInterval) × ↑unitInterval

A homeomorphism that sends (y₀, y₁, …, yₙ₋₁, yₙ) to ((y₀, y₁, …, yₙ₋₁), yₙ)

Equations

• Cube.splitAtLastComm = Cube.splitAtLast.trans (Homeomorph.prodComm (↑unitInterval) (Fin n → ↑unitInterval))

theorem Cube.splitAtLast_fst_eq {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) : (splitAtLast y).1 = y (Fin.last n)

theorem Cube.splitAtLastComm_snd_eq {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) : (splitAtLastComm y).2 = y (Fin.last n)

theorem Cube.splitAtLast_snd_eq {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) : (splitAtLast y).2 = (splitAtLastComm y).1

theorem Cube.splitAtLast_snd_apply_eq {n : ℕ} (y : Fin (n + 1) → ↑unitInterval) (i : Fin n) : (splitAtLast y).2 i = y i.castSucc

theorem Cube.splitAtLast_symm_apply_last {n : ℕ} (t : ↑unitInterval) (y : Fin n → ↑unitInterval) : splitAtLast.symm (t, y) (Fin.last n) = t

theorem Cube.splitAtLast_symm_apply_eq_of_neq_last {n : ℕ} (t : ↑unitInterval) (y : Fin n → ↑unitInterval) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : splitAtLast.symm (t, y) i = y ⟨↑i, ⋯⟩

theorem Cube.mem_boundaryJar_iff_splitAtLast {n : ℕ} {y : Fin (n + 1) → ↑unitInterval} : y ∈ boundaryJar (n + 1) ↔ (splitAtLast y).1 = 0 ∨ (splitAtLast y).2 ∈ boundary (Fin n)

y ∈ ⊔I^(n+1) if and only if either y is on the bottom face, or its first n coordinates constitute a point in ∂I^n. Note that (splitAtLast y).fst is the last (n-th) coordinate.

theorem Cube.splitAtLast_snd_mem_boundary_of_last_neq_zero {n : ℕ} {y : Fin (n + 1) → ↑unitInterval} (hy : y ∈ boundaryJar (n + 1)) (hyn : y (Fin.last n) ≠ 0) : (splitAtLast y).2 ∈ boundary (Fin n)

An easy corrolary of mem_boundaryJar_iff_splitAtLast

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

def Cube.inclToTop {n : ℕ} : C(Fin n → ↑unitInterval, Fin (n + 1) → ↑unitInterval)

The inclusion from the n-dimensional cube to the top face of the (n+1)-dimensional cube, mapping (y₀, y₁, …, yₙ₋₁) to (y₀, y₁, …, yₙ₋₁, 1). (Although 1 appears first in this definition, it is actually the last coordinate in (I^ Fin (n + 1)), due to Cube.insertAt).

Equations

• Cube.inclToTop = { toFun := fun (y : Fin n → ↑unitInterval) => Cube.splitAtLast.symm (1, y), continuous_toFun := ⋯ }

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

(y, 1) is in the boundary.

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

If y is in the boundary, then (y, 1) is in the boundaryJar.

theorem Cube.splitAtLast_inclToTop_eq {n : ℕ} {y : Fin n → ↑unitInterval} : splitAtLast (inclToTop y) = (1, y)

def Cube.discardLast {n : ℕ} : C(Fin (n + 1) → ↑unitInterval, Fin n → ↑unitInterval)

(y₀, y₁, …, yₙ₋₁, yₙ) ↦ (y₀, y₁, …, yₙ₋₁)

Equations

• Cube.discardLast = { toFun := fun (y : Fin (n + 1) → ↑unitInterval) (i : Fin n) => y ⟨↑i, ⋯⟩, continuous_toFun := ⋯ }

def Cube.inclToBot {n : ℕ} : C(Fin n → ↑unitInterval, Fin (n + 1) → ↑unitInterval)

(y₀, y₁, …, yₙ₋₁) ↦ (y₀, y₁, …, yₙ₋₁, 0)

Equations

• Cube.inclToBot = { toFun := fun (y : Fin n → ↑unitInterval) => (Cube.insertAt (Fin.last n)) (0, Cube.homeoNeqLast y), continuous_toFun := ⋯ }

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

(y, 0) is in the boundary.

theorem Cube.inclToBot.mem_boundaryJar {n : ℕ} (y : Fin n → ↑unitInterval) : inclToBot y ∈ boundaryJar (n + 1)

(y, 0) is in the boundaryJar.

def Cube.inclToBoundaryJarBot {n : ℕ} : C(Fin n → ↑unitInterval, ↑(boundaryJar (n + 1)))

The inclusion (y₀, y₁, …, yₙ₋₁) ↦ (y₀, y₁, …, yₙ₋₁, 0) to the bottom face of ⊔I^(n+1)

Equations

• Cube.inclToBoundaryJarBot = { toFun := fun (y : Fin n → ↑unitInterval) => ⟨Cube.inclToBot y, ⋯⟩, continuous_toFun := ⋯ }

def Cube.inclToBoundaryJarSides {n : ℕ} : C(↑(boundary (Fin n)) × ↑unitInterval, ↑(boundaryJar (n + 1)))

The inclusion (y, t) ↦ (y₀, y₁, …, yₙ₋₁, t) to the sides of ⊔I^(n+1), i.e., the closure of the complement of the top and bottom faces of ∂I^(n+1).

Equations

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

def Cube.inclToSides {n : ℕ} : C(↑(boundary (Fin n)) × ↑unitInterval, Fin (n + 1) → ↑unitInterval)

The inclusion (y, t) ↦ (y₀, y₁, …, yₙ₋₁, t) to the sides of the $(n+1)$-dimensional cube.

Equations

• Cube.inclToSides = { toFun := Subtype.val ∘ ⇑Cube.inclToBoundaryJarSides, continuous_toFun := ⋯ }

def TopCat.cube (n : ℕ) : TopCat

cube

Equations

• TopCat.cube n = TopCat.of (ULift.{?u.1, 0} (Fin n → ↑unitInterval))

def TopCat.cubeBoundary (n : ℕ) : TopCat

cubeBoundary

Equations

• TopCat.cubeBoundary n = TopCat.of (ULift.{?u.1, 0} ↑(Cube.boundary (Fin n)))

def TopCat.cubeBoundaryJar (n : ℕ) : TopCat

cubeBoundaryJar

Equations

• TopCat.cubeBoundaryJar n = TopCat.of (ULift.{?u.1, 0} ↑(Cube.boundaryJar n))

def TopCat.term𝕀_ : Lean.ParserDescr

𝕀 n denotes the n-cube (as an object in TopCat).

Equations

• TopCat.term𝕀_ = Lean.ParserDescr.node `TopCat.term𝕀_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝕀 ") (Lean.ParserDescr.cat `term 1023))

def TopCat.«term∂𝕀_» : Lean.ParserDescr

∂𝕀 n denotes the boundary of the n-cube (as an object in TopCat).

Equations

• TopCat.«term∂𝕀_» = Lean.ParserDescr.node `TopCat.«term∂𝕀_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∂𝕀 ") (Lean.ParserDescr.cat `term 1023))

def TopCat.«term⊔𝕀_» : Lean.ParserDescr

⊔𝕀 n denotes the "boundary jar" ($⊔Iⁿ⁺¹ = ∂Iⁿ × I ∪ Iⁿ × {0} ⊆ Iⁿ⁺¹$) of the n-cube (as an object in TopCat).

Equations

• TopCat.«term⊔𝕀_» = Lean.ParserDescr.node `TopCat.«term⊔𝕀_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊔𝕀 ") (Lean.ParserDescr.cat `term 1023))

def TopCat.cubeBoundaryIncl (n : ℕ) : cubeBoundary n ⟶ cube n

The inclusion ∂𝕀 n ⟶ 𝕀 n of the boundary of the n-cube.

Equations

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

def TopCat.cubeBoundaryJarInclToBoundary (n : ℕ) : cubeBoundaryJar n ⟶ cubeBoundary n

cubeBoundaryJarInclToBoundary

Equations

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

@[simp]

theorem TopCat.cubeBoundaryIncl_apply_down_eq {n : ℕ} (y : Fin n → ↑unitInterval) (hy : y ∈ Cube.boundary (Fin n)) : ((CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) { down := ⟨y, hy⟩ }).down = y

def TopCat.cubeSplitAtLast {n : ℕ} : cube (n + 1) ≅ of (↑unitInterval × ↑(cube n))

cubeSplitAtLast

Equations

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

@[simp]

theorem TopCat.cubeSplitAtLast_inv_down_eq {n : ℕ} (t : ↑unitInterval) (y : ↑(cube n)) : ((CategoryTheory.ConcreteCategory.hom cubeSplitAtLast.inv) (t, y)).down = Cube.splitAtLast.symm (t, y.down)

This lemma should be applied before expanding the match expression.

theorem TopCat.cubeSplitAtLast_inv_mem_boundary_of_mem_boundary {n : ℕ} (t : ↑unitInterval) (y : ↑(cubeBoundary n)) : ((CategoryTheory.ConcreteCategory.hom cubeSplitAtLast.inv) (t, (CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) y)).down ∈ Cube.boundary (Fin (n + 1))

def TopCat.cubeBoundary.cubeInclToBotOrTop {n : ℕ} (t : ↑unitInterval.zeroOne) : cube n ⟶ cubeBoundary (n + 1)

The inclusion from the n-dimensional cube to the top or bottom face of the boundary of the (n+1)-dimensional cube, mapping (y₀, y₁, …, yₙ₋₁) to (y₀, y₁, …, yₙ₋₁, t).

Equations

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

@[reducible, inline]

abbrev TopCat.cubeBoundary.botOrTop (n : ℕ) (t : ↑unitInterval.zeroOne) : Set ↑(cubeBoundary (n + 1))

botOrTop

Equations

• TopCat.cubeBoundary.botOrTop n t = {{ down := ⟨y, property⟩ } : ↑(TopCat.cubeBoundary (n + 1)) | y (Fin.last n) = unitInterval.zeroOneIncl t}

@[reducible, inline]

abbrev TopCat.cubeBoundary.sides (n : ℕ) : Set ↑(cubeBoundary (n + 1))

sides

Equations

• TopCat.cubeBoundary.sides n = {{ down := ⟨y, property⟩ } : ↑(TopCat.cubeBoundary (n + 1)) | ∃ i < Fin.last n, y i = 0 ∨ y i = 1}

theorem TopCat.cubeBoundary.cubeInclToBotOrTop_mem_botOrTop {n : ℕ} (t : ↑unitInterval.zeroOne) (y : ↑(cube n)) : (CategoryTheory.ConcreteCategory.hom (cubeInclToBotOrTop t)) y ∈ botOrTop n t

def TopCat.cubeBoundary.castSucc {n : ℕ} (t : ↑unitInterval) (y : ↑(cubeBoundary n)) : ↑(cubeBoundary (n + 1))

Given a point on the boundary of the n-dimensional cube, cast it as a point on the boundary of the (n + 1)-dimensional cube by specifying the height t : I.

Equations

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

theorem TopCat.cubeBoundary.castSucc_mem_sides {n : ℕ} (t : ↑unitInterval) (y : ↑(cubeBoundary n)) : castSucc t y ∈ sides n