LeanPool.WhiteheadTheorem.Shapes.CubeBoundaryMap

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

@[reducible, inline]

abbrev TopCat.cubeBoundary.botTopSidesCover (n : ℕ) : Fin 3 → Set ↑(cubeBoundary (n + 1))

botTopSidesCover

Equations

• TopCat.cubeBoundary.botTopSidesCover n = ![TopCat.cubeBoundary.botOrTop n 0, TopCat.cubeBoundary.botOrTop n 1, TopCat.cubeBoundary.sides n]

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

theorem TopCat.cubeBoundary.sides_eq_union_iUnion (n : ℕ) : sides 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}

theorem TopCat.cubeBoundary.botTopSidesCover_cover (n : ℕ) (y : ↑(cubeBoundary (n + 1))) : ∃ (k : Fin 3), y ∈ botTopSidesCover n k

theorem TopCat.cubeBoundary.botTopSidesCover_closed (n : ℕ) (k : Fin 3) : IsClosed (botTopSidesCover n k)

theorem TopCat.cubeBoundary.splitAtLast_snd_mem_boundary_of_mem_sides {n : ℕ} {y : ↑(cubeBoundary (n + 1))} (hy : y ∈ sides n) : (Cube.splitAtLast ↑y.down).2 ∈ Cube.boundary (Fin n)

def TopCat.cubeBoundary.mapVecOfBotTopSides {n : ℕ} {Z : TopCat} (f01 : ↑unitInterval.zeroOne → (cube n ⟶ Z)) (fs : of (↑unitInterval × ↑(cubeBoundary n)) ⟶ Z) (k : Fin 3) : C(↑(botTopSidesCover n k), ↑Z)

mapVecOfBotTopSides

Equations

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

theorem TopCat.cubeBoundary.mapVecOfBotTopSides_compatible_botOrTop {n : ℕ} {Z : TopCat} (f01 : ↑unitInterval.zeroOne → (cube n ⟶ Z)) (fs : of (↑unitInterval × ↑(cubeBoundary n)) ⟶ Z) (h : ∀ (t : ↑unitInterval.zeroOne) (y : ↑(cubeBoundary n)), (CategoryTheory.ConcreteCategory.hom (f01 t)) ((CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) y) = (CategoryTheory.ConcreteCategory.hom fs) (unitInterval.zeroOneIncl t, y)) : (∀ (y : ↑(cubeBoundary (n + 1))) (hy0 : y ∈ botTopSidesCover n 0) (hy2 : y ∈ botTopSidesCover n 2), (mapVecOfBotTopSides f01 fs 0) ⟨y, hy0⟩ = (mapVecOfBotTopSides f01 fs 2) ⟨y, hy2⟩) ∧ ∀ (y : ↑(cubeBoundary (n + 1))) (hy1 : y ∈ botTopSidesCover n 1) (hy2 : y ∈ botTopSidesCover n 2), (mapVecOfBotTopSides f01 fs 1) ⟨y, hy1⟩ = (mapVecOfBotTopSides f01 fs 2) ⟨y, hy2⟩

theorem TopCat.cubeBoundary.mapVecOfBotTopSides_compatible {n : ℕ} {Z : TopCat} (f01 : ↑unitInterval.zeroOne → (cube n ⟶ Z)) (fs : of (↑unitInterval × ↑(cubeBoundary n)) ⟶ Z) (h : ∀ (t : ↑unitInterval.zeroOne) (y : ↑(cubeBoundary n)), (CategoryTheory.ConcreteCategory.hom (f01 t)) ((CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) y) = (CategoryTheory.ConcreteCategory.hom fs) (unitInterval.zeroOneIncl t, y)) (j k : Fin 3) (y : ↑(cubeBoundary (n + 1))) (hyj : y ∈ botTopSidesCover n j) (hyk : y ∈ botTopSidesCover n k) : (mapVecOfBotTopSides f01 fs j) ⟨y, hyj⟩ = (mapVecOfBotTopSides f01 fs k) ⟨y, hyk⟩

noncomputable def TopCat.cubeBoundary.mapOfBotTopSides {n : ℕ} {Z : TopCat} (f01 : ↑unitInterval.zeroOne → (cube n ⟶ Z)) (fs : of (↑unitInterval × ↑(cubeBoundary n)) ⟶ Z) (h : ∀ (t : ↑unitInterval.zeroOne) (y : ↑(cubeBoundary n)), (CategoryTheory.ConcreteCategory.hom (f01 t)) ((CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) y) = (CategoryTheory.ConcreteCategory.hom fs) (unitInterval.zeroOneIncl t, y)) : cubeBoundary (n + 1) ⟶ Z

mapOfBotTopSides

Equations

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

theorem TopCat.cubeBoundary.cubeInclToBotOrTop_mapOfBotTopSides {n : ℕ} {Z : TopCat} (f01 : ↑unitInterval.zeroOne → (cube n ⟶ Z)) (fs : of (↑unitInterval × ↑(cubeBoundary n)) ⟶ Z) (h : ∀ (t : ↑unitInterval.zeroOne) (y : ↑(cubeBoundary n)), (CategoryTheory.ConcreteCategory.hom (f01 t)) ((CategoryTheory.ConcreteCategory.hom (cubeBoundaryIncl n)) y) = (CategoryTheory.ConcreteCategory.hom fs) (unitInterval.zeroOneIncl t, y)) (t : ↑unitInterval.zeroOne) : CategoryTheory.CategoryStruct.comp (cubeInclToBotOrTop t) (mapOfBotTopSides f01 fs h) = f01 t