This file proves that the pair (∂𝕀 n, ⊔𝕀 n) has the homotopy extension property for n ≥ 1.

@[reducible, inline]

abbrev TopCat.cubeBoundaryJar.bot (n : ℕ) : Set ↑(cubeBoundaryJar (n + 1))

bot

Equations

• TopCat.cubeBoundaryJar.bot n = {{ down := ⟨y, property⟩ } : ↑(TopCat.cubeBoundaryJar (n + 1)) | y (Fin.last n) = 0}

@[reducible, inline]

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

sides

Equations

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

@[reducible, inline]

abbrev TopCat.cubeBoundaryJar.botSidesCover (n : ℕ) : Fin 2 → Set ↑(cubeBoundaryJar (n + 1))

botSidesCover

Equations

• TopCat.cubeBoundaryJar.botSidesCover n = ![TopCat.cubeBoundaryJar.bot n, TopCat.cubeBoundaryJar.sides n]

theorem TopCat.cubeBoundaryJar.botSidesCover_cover (n : ℕ) (y : ↑(cubeBoundaryJar (n + 1))) : ∃ (k : Fin 2), y ∈ botSidesCover n k

theorem TopCat.cubeBoundaryJar.sides_eq_union (n : ℕ) : sides n = (⋃ (i : Fin n), {{ down := ⟨y, property⟩ } : ↑(cubeBoundaryJar (n + 1)) | y i.castSucc = 0}) ∪ ⋃ (i : Fin n), {{ down := ⟨y, property⟩ } : ↑(cubeBoundaryJar (n + 1)) | y i.castSucc = 1}

theorem TopCat.cubeBoundaryJar.isClosed_bot (n : ℕ) : IsClosed (bot n)

theorem TopCat.cubeBoundaryJar.isClosed_sides (n : ℕ) : IsClosed (sides n)

theorem TopCat.cubeBoundaryJar.botSidesCover_closed (n : ℕ) (k : Fin 2) : IsClosed (botSidesCover n k)

@[reducible, inline]

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

Cube.boundaryJar as a subset of Cube.boundary

Equations

• TopCat.cubeBoundary.jar n = {y : ↑(TopCat.cubeBoundary (n + 1)) | ↑y.down ∈ Cube.boundaryJar (n + 1)}

theorem TopCat.cubeBoundary.jar_eq_union (n : ℕ) : jar n = ((⋃ (i : Fin n), {{ down := ⟨y, property⟩ } : ↑(cubeBoundary (n + 1)) | y i.castSucc = 0}) ∪ ⋃ (i : Fin n), {{ down := ⟨y, property⟩ } : ↑(cubeBoundary (n + 1)) | y i.castSucc = 1}) ∪ {{ down := ⟨y, property⟩ } : ↑(cubeBoundary (n + 1)) | y (Fin.last n) = 0}

jar n can be written as the union of 2 * n + 1 surfaces of the (n + 1)-cube.

theorem TopCat.cubeBoundary.isClosed_jar (n : ℕ) : IsClosed (jar n)

@[reducible, inline]

abbrev TopCat.cubeBoundaryProdI.back (n : ℕ) : Set (↑(cubeBoundary (n + 1)) × ↑unitInterval)

The back surface of ∂𝕀 (n + 1) × I

Equations

• TopCat.cubeBoundaryProdI.back n = {pt : ↑(TopCat.cubeBoundary (n + 1)) × ↑unitInterval | ↑pt.1.down ∈ Cube.boundaryLid (n + 1)}

@[reducible, inline]

abbrev TopCat.cubeBoundaryProdI.flr (n : ℕ) : Set (↑(cubeBoundary (n + 1)) × ↑unitInterval)

The front, left, and right surfaces of ∂𝕀 (n + 1) × I

Equations

• TopCat.cubeBoundaryProdI.flr n = {pt : ↑(TopCat.cubeBoundary (n + 1)) × ↑unitInterval | ↑pt.1.down ∈ Cube.boundaryJar (n + 1)}

@[reducible, inline]

abbrev TopCat.cubeBoundaryProdI.backFlrCover (n : ℕ) : Fin 2 → Set (↑(cubeBoundary (n + 1)) × ↑unitInterval)

backFlrCover

Equations

• TopCat.cubeBoundaryProdI.backFlrCover n = ![TopCat.cubeBoundaryProdI.back n, TopCat.cubeBoundaryProdI.flr n]

theorem TopCat.cubeBoundaryProdI.backFlrCover_cover (n : ℕ) (pt : ↑(cubeBoundary (n + 1)) × ↑unitInterval) : ∃ (k : Fin 2), pt ∈ backFlrCover n k

theorem TopCat.cubeBoundaryProdI.flr_eq_sprod (n : ℕ) : flr n = cubeBoundary.jar n ×ˢ Set.univ

theorem TopCat.cubeBoundaryProdI.isClosed_back (n : ℕ) : IsClosed (back n)

theorem TopCat.cubeBoundaryProdI.isClosed_flr (n : ℕ) : IsClosed (flr n)

theorem TopCat.cubeBoundaryProdI.backFlrCover_closed (n : ℕ) (k : Fin 2) : IsClosed (backFlrCover n k)

def TopCat.cubeBoundaryProdI.backIsoCube (n : ℕ) : ↑(back n) ≃ₜ (Fin (n + 1) → ↑unitInterval)

backIsoCube

Equations

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

def TopCat.cubeBoundaryProdI.jarBotMap {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) : C(↑(cubeBoundaryJar.bot n), Y)

jarBotMap

Equations

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

def TopCat.cubeBoundaryProdI.jarSidesMap {n : ℕ} {Y : Type u} [TopologicalSpace Y] (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) : C(↑(cubeBoundaryJar.sides n), Y)

jarSidesMap

Equations

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

def TopCat.cubeBoundaryProdI.botSidesCoverMapVec {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (k : Fin 2) : C(↑(cubeBoundaryJar.botSidesCover n k), Y)

botSidesCoverMapVec

Equations

• TopCat.cubeBoundaryProdI.botSidesCoverMapVec f h = Fin.cons (TopCat.cubeBoundaryProdI.jarBotMap f) (Fin.cons (TopCat.cubeBoundaryProdI.jarSidesMap h) finZeroElim)

theorem TopCat.cubeBoundaryProdI.botSidesCoverMapVec_compatible_01 {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) (y : ↑(cubeBoundaryJar (n + 1))) (hy0 : y ∈ cubeBoundaryJar.botSidesCover n 0) (hy1 : y ∈ cubeBoundaryJar.botSidesCover n 1) : (botSidesCoverMapVec f h 0) ⟨y, hy0⟩ = (botSidesCoverMapVec f h 1) ⟨y, hy1⟩

jarBotMap and jarSidesMap agree at the intersection of cubeBoundaryJar.bot and cubeBoundaryJar.sides.

|     |
|     |
*_____*

theorem TopCat.cubeBoundaryProdI.botSidesCoverMapVec_compatible {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) (j k : Fin 2) (y : ↑(cubeBoundaryJar (n + 1))) (hyj : y ∈ cubeBoundaryJar.botSidesCover n j) (hyk : y ∈ cubeBoundaryJar.botSidesCover n k) : (botSidesCoverMapVec f h j) ⟨y, hyj⟩ = (botSidesCoverMapVec f h k) ⟨y, hyk⟩

noncomputable def TopCat.cubeBoundaryProdI.jarMap {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) : C(↑(cubeBoundaryJar (n + 1)), Y)

jarMap

Equations

• TopCat.cubeBoundaryProdI.jarMap f h fh = ContinuousMap.liftCoverClosed (TopCat.cubeBoundaryJar.botSidesCover n) (TopCat.cubeBoundaryProdI.botSidesCoverMapVec f h) ⋯ ⋯ ⋯

noncomputable def TopCat.cubeBoundaryProdI.backMap {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) : C(↑(back n), Y)

backMap

Equations

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

def TopCat.cubeBoundaryProdI.flrMap {n : ℕ} {Y : Type u} [TopologicalSpace Y] (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) : C(↑(flr n), Y)

flrMap

Equations

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

noncomputable def TopCat.cubeBoundaryProdI.backFlrCoverMapVec {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) (k : Fin 2) : C(↑(backFlrCover n k), Y)

backFlrCoverMapVec

Equations

• TopCat.cubeBoundaryProdI.backFlrCoverMapVec f h fh = Fin.cons (TopCat.cubeBoundaryProdI.backMap f h fh) (Fin.cons (TopCat.cubeBoundaryProdI.flrMap h) finZeroElim)

theorem TopCat.cubeBoundaryProdI.backFlrCover_mapVec_compatible_01 {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) (y : ↑(cubeBoundary (n + 1)) × ↑unitInterval) (hy0 : y ∈ backFlrCover n 0) (hy1 : y ∈ backFlrCover n 1) : (backFlrCoverMapVec f h fh 0) ⟨y, hy0⟩ = (backFlrCoverMapVec f h fh 1) ⟨y, hy1⟩

backMap and flrMap agree on the edges of the back surface.

  __________
 /*        /*
/ *       / *
----------  *
| *      |  *
| *______|__*
| /      | /
|/_______|/

theorem TopCat.cubeBoundaryProdI.backFlrCover_mapVec_compatible {n : ℕ} {Y : Type u} [TopologicalSpace Y] (f : C(↑(cubeBoundary (n + 1)), Y)) (h : C(↑(cubeBoundaryJar (n + 1)) × ↑unitInterval, Y)) (fh : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (cubeBoundaryJarInclToBoundary (n + 1))) = ⇑h ∘ fun (x : ↑(cubeBoundaryJar (n + 1))) => (x, 0)) (j k : Fin 2) (y : ↑(cubeBoundary (n + 1)) × ↑unitInterval) (hyj : y ∈ backFlrCover n j) (hyk : y ∈ backFlrCover n k) : (backFlrCoverMapVec f h fh j) ⟨y, hyj⟩ = (backFlrCoverMapVec f h fh k) ⟨y, hyk⟩

theorem TopCat.cubeBoundaryJarInclToBoundary_hasHEP (n : ℕ) (Y : Type u) [TopologicalSpace Y] : HasHomotopyExtensionProperty (Hom.hom (cubeBoundaryJarInclToBoundary (n + 1))) Y