For every CW-complex X, this file constructs a relative CW-complex X.IProd homeomorphic to I × X, where I is the unit interval. The $(-1)$-skeleton of X.IProd is homeomorphic to {0, 1} × X.

@[reducible, inline]

noncomputable abbrev CWComplex.zeroOneProdInclIProd (X : CWComplex) : TopCat.of (↑unitInterval.zeroOne × ↑X.toTopCat) ⟶ TopCat.of (↑unitInterval × ↑X.toTopCat)

The inclusion map from {0, 1} × X to I × X

Equations

• X.zeroOneProdInclIProd = TopCat.ofHom (unitInterval.zeroOneIncl.prodMap (ContinuousMap.id ↑X.toTopCat))

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.l (X : CWComplex) (n : ℕ) : TopCat.of (↑unitInterval.zeroOne × ↑(X.sk n)) ⟶ TopCat.of (↑unitInterval.zeroOne × ↑X.toTopCat)

l

Equations

• CWComplex.IProd.l X n = TopCat.ofHom ((ContinuousMap.id ↑unitInterval.zeroOne).prodMap (TopCat.Hom.hom (X.skIncl n)))

@[reducible, inline]

abbrev CWComplex.IProd.r (X : CWComplex) (n : ℕ) : TopCat.of (↑unitInterval.zeroOne × ↑(X.sk n)) ⟶ TopCat.of (↑unitInterval × ↑(X.sk n))

r

Equations

• CWComplex.IProd.r X n = TopCat.ofHom (unitInterval.zeroOneIncl.prodMap (ContinuousMap.id ↑(X.sk n)))

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.xskl (X : CWComplex) (n : ℕ) : (∐ fun (b : (X.attachCells n).cells) => TopCat.diskBoundary n) ⟶ X.sk n

xskl

Equations

• CWComplex.IProd.xskl X n = CategoryTheory.Limits.Sigma.desc (X.attachCells n).attachMaps

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.xskr (X : CWComplex) (n : ℕ) : (∐ fun (x : (X.attachCells n).cells) => TopCat.diskBoundary n) ⟶ ∐ fun (x : (X.attachCells n).cells) => TopCat.disk n

xskr

Equations

• CWComplex.IProd.xskr X n = CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl n

noncomputable def CWComplex.IProd.sk (X : CWComplex) (n : ℕ) : TopCat

                    l X n
{0, 1} × (X.sk n) ------→ {0, 1} × X
       |                       |
r X n  |             pushout   |
       ↓                       ↓
     I × (X.sk n) ----→ X.IProd.sk (n + 1)

X.IProd.sk 0 = {0, 1} × X ≅ X.IProd.sk 1

Equations

• CWComplex.IProd.sk X 0 = TopCat.of (↑unitInterval.zeroOne × ↑X.toTopCat)
• CWComplex.IProd.sk X n_2.succ = CategoryTheory.Limits.pushout (CWComplex.IProd.l X n_2) (CWComplex.IProd.r X n_2)

noncomputable def CWComplex.IProd.skZeroIsoSkOne (X : CWComplex) : sk X 0 ≅ sk X 1

skZeroIsoSkOne

Equations

• CWComplex.IProd.skZeroIsoSkOne X = CategoryTheory.asIso (CategoryTheory.Limits.pushout.inl (CWComplex.IProd.l X 0) (CWComplex.IProd.r X 0))

noncomputable def CWComplex.cubeInclToSk (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) : TopCat.cube n ⟶ X.sk (n + 1)

cubeInclToSk

Equations

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

noncomputable def CWComplex.cubeIncl (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) : TopCat.cube n ⟶ X.toTopCat

cubeIncl

Equations

• X.cubeIncl α = CategoryTheory.CategoryStruct.comp (X.cubeInclToSk α) (X.skIncl (n + 1))

noncomputable def CWComplex.cubeAtt (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) : TopCat.cubeBoundary n ⟶ X.sk n

cubeAtt

Equations

• X.cubeAtt α = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left (TopCat.diskPair.homeoCubePairULift n).inv) ((X.attachCells n).attachMaps α)

noncomputable def CWComplex.IProd.cubeAttBotOrTop (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) (t : ↑unitInterval.zeroOne) : TopCat.cube n ⟶ sk X (n + 1)

cubeAttBotOrTop

Equations

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

noncomputable def CWComplex.IProd.cubeAttSides (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) : TopCat.of (↑unitInterval × ↑(TopCat.cubeBoundary n)) ⟶ sk X (n + 1)

cubeAttSides

Equations

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

theorem CWComplex.IProd.cubeAtt_compatible (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) (t : ↑unitInterval.zeroOne) (y : ↑(TopCat.cubeBoundary n)) : (CategoryTheory.ConcreteCategory.hom (cubeAttBotOrTop X α t)) ((CategoryTheory.ConcreteCategory.hom (TopCat.cubeBoundaryIncl n)) y) = (CategoryTheory.ConcreteCategory.hom (cubeAttSides X α)) (unitInterval.zeroOneIncl t, y)

noncomputable def CWComplex.IProd.attachMaps (X : CWComplex) {n : ℕ} (α : (X.attachCells n).cells) : TopCat.diskBoundary (n + 1) ⟶ sk X (n + 1)

attachMaps

Equations

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

noncomputable def CWComplex.IProd.sigmaDisksInclToSk (X : CWComplex) (n : ℕ) : (∐ fun (x : (X.attachCells n).cells) => TopCat.disk (n + 1)) ⟶ sk X (n + 1 + 1)

Note: Each $n$-cell of X corresponds to an $(n + 1)$-cell of X.IProd. The latter cell is attached to IProd.sk X (n + 1), which is of dimension $n$. X.IProd has no 0-cells.

Equations

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

noncomputable def CWComplex.IProd.skInclSucc (X : CWComplex) (n : ℕ) : sk X (n + 1) ⟶ sk X (n + 1 + 1)

skInclSucc

Equations

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

theorem CWComplex.IProd.inl_skInclSucc (X : CWComplex) {n : ℕ} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (l X n) (r X n)) (skInclSucc X n) = CategoryTheory.Limits.pushout.inl (l X (n + 1)) (r X (n + 1))

theorem CWComplex.IProd.inl_skInclSucc_assoc (X : CWComplex) {n : ℕ} {Z : TopCat} (h : sk X (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (l X n) (r X n)) (CategoryTheory.CategoryStruct.comp (skInclSucc X n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (l X (n + 1)) (r X (n + 1))) h

theorem CWComplex.IProd.inr_skInclSucc (X : CWComplex) {n : ℕ} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (l X n) (r X n)) (skInclSucc X n) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom ((ContinuousMap.id ↑unitInterval).prodMap (TopCat.Hom.hom (X.skInclSucc n)))) (CategoryTheory.Limits.pushout.inr (l X (n + 1)) (r X (n + 1)))

theorem CWComplex.IProd.inr_skInclSucc_assoc (X : CWComplex) {n : ℕ} {Z : TopCat} (h : sk X (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (l X n) (r X n)) (CategoryTheory.CategoryStruct.comp (skInclSucc X n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TopCat.ofHom ((ContinuousMap.id ↑unitInterval).prodMap (TopCat.Hom.hom (X.skInclSucc n)))) (CategoryTheory.Limits.pushout.inr (l X (n + 1)) (r X (n + 1)))) h

theorem CWComplex.IProd.commSqSkSk (X : CWComplex) (n : ℕ) : CategoryTheory.CommSq (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1)) (skInclSucc X n) (sigmaDisksInclToSk X n)

∐ ∂𝔻 (n + 1) -----------→ IProd.sk X (n + 1)
    |                             |
    |                             |
    ↓                             ↓
∐ 𝔻 (n + 1) ------------→ IProd.sk X (n + 1 + 1)

Now verify that commSqSkSk is a pushout square.

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.l' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : X.sk n ⟶ TopCat.of C(↑unitInterval, ↑Z.pt)

l'

Equations

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

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.r' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : (∐ fun (x : (X.attachCells n).cells) => TopCat.disk n) ⟶ TopCat.of C(↑unitInterval, ↑Z.pt)

r'

Equations

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

theorem CWComplex.IProd.pushoutSkSk.w' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : CategoryTheory.CategoryStruct.comp (xskl X n) (l' X n Z) = CategoryTheory.CategoryStruct.comp (xskr X n) (r' X n Z)

The following square commutes.

  ∐ ∂𝔻 n --------→ X.sk n
     |     xskl       |
xskr |                | l'
     ↓      r'        ↓
  ∐ 𝔻 n ---------→ C(I, Z)

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.d' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : X.sk (n + 1) ⟶ TopCat.of C(↑unitInterval, ↑Z.pt)

d'

Equations

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

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.l'' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : TopCat.of (↑unitInterval.zeroOne × ↑X.toTopCat) ⟶ Z.pt

l''

Equations

• CWComplex.IProd.pushoutSkSk.l'' X n Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CWComplex.IProd.l X n) (CWComplex.IProd.r X n)) Z.inl

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.r'' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : TopCat.of (↑unitInterval × ↑(X.sk (n + 1))) ⟶ Z.pt

r''

Equations

• CWComplex.IProd.pushoutSkSk.r'' X n Z = TopCat.ofHom (ContinuousMap.argSwap (TopCat.Hom.hom (CWComplex.IProd.pushoutSkSk.d' X n Z)).uncurry)

theorem CWComplex.IProd.pushoutSkSk.w'' (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : CategoryTheory.CategoryStruct.comp (l X (n + 1)) (l'' X n Z) = CategoryTheory.CategoryStruct.comp (r X (n + 1)) (r'' X n Z)

The following square commutes.

                       l X (n+1)
{0, 1} × (X.sk (n + 1)) ------→ {0, 1} × X
           |                       |
r X (n+1)  |                       | l''
           ↓                r''    ↓
     I × (X.sk (n + 1)) ---------→ Z

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.pushoutSkSk.desc (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : sk X (n + 1 + 1) ⟶ Z.pt

Given a commutative square

∐ ∂𝔻 (n + 1) ------→ IProd.sk X (n + 1)
    |                     |
    |                     |
    ↓                     ↓
∐ 𝔻 (n + 1) ------------→ Z

return the descending map IProd.sk X (n + 1 + 1) ⟶ Z out of the pushout cocone.

Equations

• CWComplex.IProd.pushoutSkSk.desc X n Z = CategoryTheory.Limits.pushout.desc (CWComplex.IProd.pushoutSkSk.l'' X n Z) (CWComplex.IProd.pushoutSkSk.r'' X n Z) ⋯

noncomputable def CWComplex.IProd.pushoutSkSk.cocone (X : CWComplex) (n : ℕ) : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))

cocone

Equations

• CWComplex.IProd.pushoutSkSk.cocone X n = CategoryTheory.Limits.PushoutCocone.mk (CWComplex.IProd.skInclSucc X n) (CWComplex.IProd.sigmaDisksInclToSk X n) ⋯

theorem CWComplex.IProd.pushoutSkSk.coconeInl (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : CategoryTheory.CategoryStruct.comp (cocone X n).inl (desc X n Z) = Z.inl

theorem CWComplex.IProd.pushoutSkSk.coconeInr (X : CWComplex) (n : ℕ) (Z : CategoryTheory.Limits.PushoutCocone (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1))) : CategoryTheory.CategoryStruct.comp (cocone X n).inr (desc X n Z) = Z.inr

theorem CWComplex.IProd.pushoutSkSk (X : CWComplex) (n : ℕ) : CategoryTheory.IsPushout (CategoryTheory.Limits.Sigma.desc (attachMaps X)) (CategoryTheory.Limits.Sigma.map fun (x : (X.attachCells n).cells) => TopCat.diskBoundaryIncl (n + 1)) (skInclSucc X n) (sigmaDisksInclToSk X n)

pushoutSkSk

noncomputable def CWComplex.IProd (X : CWComplex) : RelCWComplex

IProd

Equations

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