LeanPool.WhiteheadTheorem.Compressible.CWComplex

This file proves that if a map is compressible with respect to TopCat.diskBoundaryIncl n : ∂𝔻 n ⟶ 𝔻 n (inclusion from the boundary of a disk to the disk), then it is compressible with respect to the inclusion map from the -1-skeleton of any relative CW-complex to the relative CW-complex. This is the theorem IsCompressible.relCWComplex_of_diskBoundaryIncl.

Some proofs are similar to the ones in Mathlib.CategoryTheory.LiftingProperties.Limits

source

theorem TopCat.IsCompressible.of_comp_iso_left {A B Z X Y : TopCat} {i1 : A ⟶ X} {i2 : X ⟶ Z} {j : B ⟶ Y} (hcom1 : IsCompressible i1 j) [CategoryTheory.IsIso i2] :

IsCompressible (CategoryTheory.CategoryStruct.comp i1 i2) j

Suppose j is compressible w.r.t. i1, and i2 is an isomorphism, then j is compressible w.r.t. i1 ≫ i2.

source

theorem TopCat.IsCompressible.of_iso_comp_left {A B Z X Y : TopCat} {i1 : A ⟶ X} {i2 : X ⟶ Z} {j : B ⟶ Y} [CategoryTheory.IsIso i1] (hcom2 : IsCompressible i2 j) :

IsCompressible (CategoryTheory.CategoryStruct.comp i1 i2) j

Suppose i1 is an isomorphism and j is compressible w.r.t. i2, then j is compressible w.r.t. i1 ≫ i2.

source

theorem TopCat.IsCompressible.of_arrow_iso_left {A X A' X' B Y : TopCat} {i : A ⟶ X} {i' : A' ⟶ X'} {j : B ⟶ Y} (e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i') (hcom : IsCompressible i j) :

IsCompressible i' j

Suppose j is compressible w.r.t. i, and i is isomorphic to i' in the arrow category, then j is compressible w.r.t. i'.

source

theorem TopCat.IsCompressible.coprod {A B X Y : TopCat} {i : A ⟶ X} {j : B ⟶ Y} (hcom : IsCompressible i j) (cells : Type u) :

IsCompressible (CategoryTheory.Limits.Sigma.map fun (x : cells) => i) j

If j is compressible w.r.t. i, then it is also compressible w.r.t. ∐ i.

∐ A -----f----→ B
 |              |
∐ i             j
 |              |
 ↓              ↓
∐ X -----F----→ Y

TODO: This lemma can be generalized to the case where each component function of ∐ A ⟶ ∐ X can be different.

source

theorem TopCat.IsCompressible.pushout {A' A B X' X Y : TopCat} {ι : A' ⟶ X'} {i : A ⟶ X} {j : B ⟶ Y} {φ : A' ⟶ A} {Φ : X' ⟶ X} (po : CategoryTheory.IsPushout φ ι i Φ) (com : IsCompressible ι j) :

IsCompressible i j

Suppose the left square in the diagram below is a pushout square. If j is compressible w.r.t. ι, then it is also compressible w.r.t. i.

A' -----φ----→ A -----f----→ B
 |             |             |
 ι             i             j
 |             |             |
 ↓             ↓             ↓
X' -----Φ----→ X -----F----→ Y

source

theorem TopCat.IsCompressible.relCWComplex_of_diskBoundaryIncl (X : RelCWComplex) {B Y : TopCat} (j : B ⟶ Y) (jcom : ∀ (n : ℕ), IsCompressible (diskBoundaryIncl n) j) :

IsCompressible (X.skIncl 0) j

Suppose X is a relative CW-complex and j : B ⟶ Y is a continuous map. If j is n-compressible for every natural number n, then it is compressible w.r.t. the inclusion map from the $(-1)$-skeleton of X to X, i.e., any map from the pair (X, X.sk 0) to (Y, B) is homotopic relative to X.sk 0 to a map into B.

X.sk 0 --- f₀ ---→ B
  |                |
  i                j
  |                |
  ↓                ↓
  X ----- F₀ ----→ Y