LeanPool.WhiteheadTheorem.CWComplex.Basic

Imported Lean Pool material for LeanPool.WhiteheadTheorem.CWComplex.Basic.

CW-complexes

This file defines (relative) CW-complexes.

Main definitions

• RelativeCWComplex: A relative CW-complex is the colimit of an expanding sequence of subspaces sk i (called the $(i-1)$-skeleton) for i ≥ 0, where sk 0 (i.e., the $(-1)$-skeleton) is an arbitrary topological space, and each sk (n + 1) (i.e., the $n$-skeleton) is obtained from sk n (i.e., the $(n-1)$-skeleton) by attaching n-disks.
• CWComplex: A CW-complex is a relative CW-complex whose sk 0 (i.e., $(-1)$-skeleton) is empty.

References

• [R. Fritsch and R. Piccinini, Cellular Structures in Topology][fritsch-piccinini1990]
• The definition of CW-complexes follows David Wärn's suggestion on Zulip.

structure RelCWComplex.AttachGeneralizedCells {S D : TopCat} (f : S ⟶ D) (X X' : TopCat) : Type (u + 1)

A type witnessing that X' is obtained from X by attaching generalized cells f : S ⟶ D

• cells : Type u

  The index type over the generalized cells

• attachMaps : self.cells → (S ⟶ X)

  An attaching map for each generalized cell

• isoPushout : X' ≅ CategoryTheory.Limits.pushout (CategoryTheory.Limits.Sigma.desc self.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : self.cells) => f)

  X' is the pushout of ∐ S ⟶ X and ∐ S ⟶ ∐ D.

@[reducible, inline]

abbrev RelCWComplex.AttachCells (n : ℕ) (X X' : TopCat) : Type (u + 1)

A type witnessing that X' is obtained from X by attaching (n + 1)-disks

Equations

• RelCWComplex.AttachCells n = RelCWComplex.AttachGeneralizedCells (TopCat.diskBoundaryIncl n)

structure RelCWComplex : Type (u + 1)

A relative CW-complex consists of an expanding sequence of subspaces sk i (called the $(i-1)$-skeleton) for i ≥ 0, where sk 0 (i.e., the $(-1)$-skeleton) is an arbitrary topological space, and each sk (n + 1) (i.e., the n-skeleton) is obtained from sk n (i.e., the $(n-1)$-skeleton) by attaching n-disks.

• sk : ℕ → TopCat

  The skeletons. Note: sk i is usually called the $(i-1)$-skeleton in the math literature.

• attachCells (n : ℕ) : AttachCells n (self.sk n) (self.sk (n + 1))

  Each sk (n + 1) (i.e., the $n$-skeleton) is obtained from sk n (i.e., the $(n-1)$-skeleton) by attaching n-disks.

structure CWComplexextends RelCWComplex : Type (u + 1)

A CW-complex is a relative CW-complex whose sk 0 (i.e., $(-1)$-skeleton) is empty.

• sk : ℕ → TopCat
• attachCells (n : ℕ) : AttachCells n (self.sk n) (self.sk (n + 1))
• isEmpty_sk_zero : IsEmpty ↑(self.sk 0)

  sk 0 (i.e., the $(-1)$-skeleton) is empty.

noncomputable def RelCWComplex.AttachCells.incl {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : X ⟶ X'

The inclusion map from X to X', given that X' is obtained from X by attaching (n + 1)-disks

Equations

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

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachCells.sigmaAttachMaps {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : (∐ fun (b : att.cells) => TopCat.diskBoundary n) ⟶ X

The top side of the pushout square

Equations

• att.sigmaAttachMaps = CategoryTheory.Limits.Sigma.desc att.attachMaps

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachCells.sigmaDiskBoundaryIncl {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : (∐ fun (x : att.cells) => TopCat.diskBoundary n) ⟶ ∐ fun (x : att.cells) => TopCat.disk n

The left side of the pushout square

Equations

• att.sigmaDiskBoundaryIncl = CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachCells.pushoutInl {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : X ⟶ CategoryTheory.Limits.pushout att.sigmaAttachMaps (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n)

The right side of the pushout square (TODO: after updating mathlib on 2025-03-08, using the abbreviation att.sigmaDiskBoundaryIncl results in type mismatch, which seems to be a universe level issue. So the abbreviation is temporarily replaced with the full definition.)

Equations

• att.pushoutInl = CategoryTheory.Limits.pushout.inl att.sigmaAttachMaps (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n)

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachCells.pushoutInr {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : (∐ fun (x : att.cells) => TopCat.disk n) ⟶ CategoryTheory.Limits.pushout att.sigmaAttachMaps (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n)

The bottom side of the pushout square

Equations

• att.pushoutInr = CategoryTheory.Limits.pushout.inr att.sigmaAttachMaps (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n)

theorem RelCWComplex.AttachCells.pushout_isPushout {n : ℕ} {X X' : TopCat} (att : AttachCells n X X') : CategoryTheory.IsPushout att.sigmaAttachMaps (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => TopCat.diskBoundaryIncl n) att.pushoutInl att.pushoutInr

The pushout square is a pushout.

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

The inclusion map from sk n (i.e., the $(n-1)$-skeleton) to sk (n + 1) (i.e., the $n$-skeleton) of a relative CW-complex

Equations

• X.skInclSucc n = (X.attachCells n).incl

noncomputable def RelCWComplex.skInclToSk (X : RelCWComplex) {n m : ℕ} (hnm : n ≤ m) : X.sk n ⟶ X.sk m

The inclusion map from sk n (i.e., the $(n-1)$-skeleton) to sk m (i.e., the $(m-1)$-skeleton) of a relative CW-complex

Equations

• X.skInclToSk hnm = (CategoryTheory.Functor.ofSequence X.skInclSucc).map (CategoryTheory.homOfLE hnm)

noncomputable def RelCWComplex.toTopCat (X : RelCWComplex) : TopCat

The topology on a relative CW-complex

Equations

• X.toTopCat = CategoryTheory.Limits.colimit (CategoryTheory.Functor.ofSequence X.skInclSucc)

@[implicit_reducible]

noncomputable instance RelCWComplex.instCoeTopCat : Coe RelCWComplex TopCat

Equations

• RelCWComplex.instCoeTopCat = { coe := fun (X : RelCWComplex) => X.toTopCat }

@[implicit_reducible]

noncomputable instance RelCWComplex.instCoeCWComplexTopCat : Coe CWComplex TopCat

Equations

• RelCWComplex.instCoeCWComplexTopCat = { coe := fun (X : CWComplex) => X.toTopCat }

noncomputable def RelCWComplex.skIncl (X : RelCWComplex) (n : ℕ) : X.sk n ⟶ X.toTopCat

The inclusion map from sk n (i.e., the $(n-1)$-skeleton of X) to X

Equations

• X.skIncl n = CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.ofSequence X.skInclSucc) n

@[simp]

theorem RelCWComplex.skInclSucc_skIncl_eq (X : RelCWComplex) (n : ℕ) : CategoryTheory.CategoryStruct.comp (X.skInclSucc n) (X.skIncl (n + 1)) = X.skIncl n

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachGeneralizedCells.pushoutInl {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') : X ⟶ CategoryTheory.Limits.pushout (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f)

pushoutInl

Equations

• att.pushoutInl = CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f)

@[reducible, inline]

noncomputable abbrev RelCWComplex.AttachGeneralizedCells.pushoutInr {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') : (∐ fun (x : att.cells) => D) ⟶ CategoryTheory.Limits.pushout (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f)

pushoutInr

Equations

• att.pushoutInr = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f)

theorem RelCWComplex.AttachGeneralizedCells.attachMaps_apply_eq_ι_desc {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) : att.attachMaps α = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => S) α) (CategoryTheory.Limits.Sigma.desc att.attachMaps)

theorem RelCWComplex.AttachGeneralizedCells.w_sigma_cells {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => S) α) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f)

S --> ∐ S
|      |
f      |
↓      ↓
D --> ∐ D

theorem RelCWComplex.AttachGeneralizedCells.w_sigma_cells_assoc {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) {Z : TopCat} (h : (∐ fun (x : att.cells) => D) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => S) α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f) h)

S --> ∐ S
|      |
f      |
↓      ↓
D --> ∐ D

theorem RelCWComplex.AttachGeneralizedCells.w_cell' {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) att.pushoutInr) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => S) α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc att.attachMaps) att.pushoutInl)

S --> ∐ S --> X
|      |      |
f      |      |
↓      ↓      ↓    ≅
D --> ∐ D --> ⬝ ------> X'

theorem RelCWComplex.AttachGeneralizedCells.w_cell'_assoc {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) {Z : TopCat} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) (CategoryTheory.CategoryStruct.comp att.pushoutInr h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => S) α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.CategoryStruct.comp att.pushoutInl h))

S --> ∐ S --> X
|      |      |
f      |      |
↓      ↓      ↓    ≅
D --> ∐ D --> ⬝ ------> X'

theorem RelCWComplex.AttachGeneralizedCells.w_cell {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) att.pushoutInr) = CategoryTheory.CategoryStruct.comp (att.attachMaps α) att.pushoutInl

S ----------> X
|             |
f             |
↓             ↓    ≅
D --> ∐ D --> ⬝ ------> X'

theorem RelCWComplex.AttachGeneralizedCells.w_cell_assoc {S D : TopCat} {f : S ⟶ D} {X X' : TopCat} (att : AttachGeneralizedCells f X X') (α : att.cells) {Z : TopCat} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.Sigma.desc att.attachMaps) (CategoryTheory.Limits.Sigma.map fun (x : att.cells) => f) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : att.cells) => D) α) (CategoryTheory.CategoryStruct.comp att.pushoutInr h)) = CategoryTheory.CategoryStruct.comp (att.attachMaps α) (CategoryTheory.CategoryStruct.comp att.pushoutInl h)

S ----------> X
|             |
f             |
↓             ↓    ≅
D --> ∐ D --> ⬝ ------> X'