This file verifies that the pair (X.IProd.sk 0, X.IProd) is homeomorphic to ({0, 1} × X, I × X), where X.IProd is the relative CW-complex constructed in CWComplex/IProd/Def.lean, X.IProd.sk 0 is its $(-1)$-skeleton, and I is the unit interval.

theorem CWComplex.IProd.inl_l_r_eq_relCWComplex_skInclSucc_zero (X : CWComplex) : CategoryTheory.Limits.pushout.inl (l X 0) (r X 0) = X.IProd.skInclSucc 0

theorem CWComplex.IProd.skInclSucc_eq_relCWComplex_skInclSucc (X : CWComplex) (n : ℕ) : skInclSucc X n = X.IProd.skInclSucc (n + 1)

theorem CWComplex.IProd.skInclSucc_map_zero_le (X : CWComplex) (n : ℕ) : (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc).map (CategoryTheory.homOfLE ⋯) = CategoryTheory.Limits.pushout.inl (l X n) (r X n)

Two maps from X.IProd.sk 0 = TopCat.of (zeroOne × X.toTopCat) to X.IProd.sk (n + 1) are equal.

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.colimitCocone.r' (X : CWComplex) (n : ℕ) : TopCat.of (↑unitInterval × ↑(X.sk n)) ⟶ TopCat.of (↑unitInterval × ↑X.toTopCat)

r'

Equations

• CWComplex.IProd.colimitCocone.r' X n = TopCat.ofHom ((ContinuousMap.id ↑unitInterval).prodMap (TopCat.Hom.hom (X.skIncl n)))

theorem CWComplex.IProd.colimitCocone.w' (X : CWComplex) (n : ℕ) : CategoryTheory.CategoryStruct.comp (l X n) X.zeroOneProdInclIProd = CategoryTheory.CategoryStruct.comp (r X n) (r' X n)

noncomputable def CWComplex.IProd.colimitCocone.incl (X : CWComplex) (n : ℕ) : X.IProd.sk n ⟶ TopCat.of (↑unitInterval × ↑X.toTopCat)

incl

Equations

• CWComplex.IProd.colimitCocone.incl X 0 = X.zeroOneProdInclIProd
• CWComplex.IProd.colimitCocone.incl X n_2.succ = CategoryTheory.Limits.pushout.desc X.zeroOneProdInclIProd (CWComplex.IProd.colimitCocone.r' X n_2) ⋯

theorem CWComplex.IProd.colimitCocone.naturality (X : CWComplex) (n : ℕ) : CategoryTheory.CategoryStruct.comp (X.IProd.skInclSucc n) (incl X (n + 1)) = incl X n

noncomputable def CWComplex.IProd.colimitCocone.cocone (X : CWComplex) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)

The cocone with X.IProd.sk 0 ⟶ X.IProd.sk 1 ⟶ ⋯ as base and TopCat.of (I × X.toTopCat) as vertex. This is actually a colimit cocone (see CWComplex.IProd.colimitCocone).

Equations

• CWComplex.IProd.colimitCocone.cocone X = { pt := TopCat.of (↑unitInterval × ↑X.toTopCat), ι := CategoryTheory.NatTrans.ofSequence (CWComplex.IProd.colimitCocone.incl X) ⋯ }

noncomputable def CWComplex.IProd.colimitCocone.IXZ (X : CWComplex) (Z : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)) : CategoryTheory.Limits.Cocone ((CategoryTheory.Functor.ofSequence X.skInclSucc).comp (TopCat.topBinProdLeft' ↑unitInterval))

The cocone with I × X.sk 0 ⟶ I × X.sk 1 ⟶ ⋯ as base and Z.pt as vertex

Equations

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

@[reducible, inline]

noncomputable abbrev CWComplex.IProd.colimitCocone.IF (X : CWComplex) : CategoryTheory.Functor ℕ TopCat

Functor constructed from the sequence of morphisms I × X.sk 0 ⟶ I × X.sk 1 ⟶ ⋯

Equations

• CWComplex.IProd.colimitCocone.IF X = (CategoryTheory.Functor.ofSequence X.skInclSucc).comp (TopCat.topBinProdLeft' ↑unitInterval)

noncomputable def CWComplex.IProd.colimitCocone.IXCocone (X : CWComplex) : CategoryTheory.Limits.Cocone (IF X)

The cocone with I × X.sk 0 ⟶ I × X.sk 1 ⟶ ⋯ as base and TopCat.of (I × X.toTopCat) as vertex. This is actually a colimit cocone (see IX).

Equations

• CWComplex.IProd.colimitCocone.IXCocone X = (TopCat.topBinProdLeft' ↑unitInterval).mapCocone (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Functor.ofSequence X.skInclSucc))

theorem CWComplex.IProd.colimitCocone.isColim_IXCocone (X : CWComplex) : Nonempty (CategoryTheory.Limits.IsColimit (IXCocone X))

I × X is the colimit of I × X.sk 0 ⟶ I × X.sk 1 ⟶ ⋯, because the left adjoint functor I × · preserves colimtis.

noncomputable def CWComplex.IProd.colimitCocone.IX (X : CWComplex) : CategoryTheory.Limits.ColimitCocone (IF X)

IXCocone is a colimit cocone.

Equations

• CWComplex.IProd.colimitCocone.IX X = { cocone := CWComplex.IProd.colimitCocone.IXCocone X, isColimit := ⋯.some }

noncomputable def CWComplex.IProd.colimitCocone.desc (X : CWComplex) (Z : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)) : (cocone X).pt ⟶ Z.pt

Note: The type is definitionally equal to (IXCocone X).pt ⟶ Z.pt.

Equations

• CWComplex.IProd.colimitCocone.desc X Z = (CWComplex.IProd.colimitCocone.IX X).isColimit.desc (CWComplex.IProd.colimitCocone.IXZ X Z)

theorem CWComplex.IProd.colimitCocone.zeroOneProdInclIProd_desc (X : CWComplex) (Z : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)) : CategoryTheory.CategoryStruct.comp X.zeroOneProdInclIProd (desc X Z) = Z.ι.app 0

theorem CWComplex.IProd.colimitCocone.fac (X : CWComplex) (Z : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (incl X n) (desc X Z) = Z.ι.app n

theorem CWComplex.IProd.colimitCocone.uniq (X : CWComplex) (Z : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)) (d : (cocone X).pt ⟶ Z.pt) (d_fac : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp ((cocone X).ι.app n) d = Z.ι.app n) : d = desc X Z

noncomputable def CWComplex.IProd.colimitCocone (X : CWComplex) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Functor.ofSequence X.IProd.skInclSucc)

The cocone CWComplex.IProd.colimitCocone.cocone X is actually a colimit cocone.

Equations

• CWComplex.IProd.colimitCocone X = { cocone := CWComplex.IProd.colimitCocone.cocone X, isColimit := { desc := CWComplex.IProd.colimitCocone.desc X, fac := ⋯, uniq := ⋯ } }

noncomputable def CWComplex.IProd.iso (X : CWComplex) : X.IProd.toTopCat ≅ TopCat.of (↑unitInterval × ↑X.toTopCat)

iso

Equations

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

noncomputable def CWComplex.IProd.arrowIso (X : CWComplex) : CategoryTheory.Arrow.mk (X.IProd.skIncl 0) ≅ CategoryTheory.Arrow.mk X.zeroOneProdInclIProd

The arrow X.IProd.sk 0 ⟶ X.IProd.toTopCat is isomorphic to {0, 1} × X ⟶ I × X.

Equations

• CWComplex.IProd.arrowIso X = CategoryTheory.Arrow.isoMk (CategoryTheory.Iso.refl (CategoryTheory.Arrow.mk (X.IProd.skIncl 0)).left) (CWComplex.IProd.iso X) ⋯