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
• The definition of CW-complexes follows David Wärn's suggestion on Zulip.

def RelativeCWComplex.sphereInclusion (n : ℤ) : TopCat.sphere n ⟶ TopCat.disk (n + 1)

The inclusion map from the n-sphere to the (n + 1)-disk. (For n = -1, this involves the empty space 𝕊 (-1). This is the reason why sphere takes n : ℤ as an input rather than n : ℕ.)

Equations

• RelativeCWComplex.sphereInclusion n = { toFun := fun (x : ↑(TopCat.sphere n)) => match x with | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }, continuous_toFun := ⋯ }

structure RelativeCWComplex.AttachGeneralizedCells {S : TopCat} {D : TopCat} (f : S ⟶ D) (X : TopCat) (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

• iso_pushout : 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.

def RelativeCWComplex.AttachCells (n : ℤ) (X : TopCat) (X' : TopCat) : Type (u_1 + 1)

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

Equations

• RelativeCWComplex.AttachCells n = RelativeCWComplex.AttachGeneralizedCells (RelativeCWComplex.sphereInclusion n)

structure RelativeCWComplex : 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 : ℕ) → RelativeCWComplex.AttachCells (↑n - 1) (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 RelativeCWComplex : Type (u + 1)

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

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

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

theorem CWComplex.isEmpty_sk_zero (self : CWComplex) : IsEmpty ↑(self.sk 0)

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

def RelativeCWComplex.AttachGeneralizedCells.inclusion {S : TopCat} {D : TopCat} {f : S ⟶ D} {X : TopCat} {X' : TopCat} (att : RelativeCWComplex.AttachGeneralizedCells f X X') : X ⟶ X'

The inclusion map from X to X', when X' is obtained from X by attaching generalized cells f : S ⟶ D.

Equations

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

def RelativeCWComplex.skInclusion (X : RelativeCWComplex) (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.skInclusion n = RelativeCWComplex.AttachGeneralizedCells.inclusion (X.attachCells n)

def RelativeCWComplex.toTopCat (X : RelativeCWComplex) : TopCat

The topology on a relative CW-complex

Equations

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

instance RelativeCWComplex.instCoeTopCat : Coe RelativeCWComplex TopCat

Equations

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