6.6 Cell complexes

In classical topologyMathworldPlanetmathPlanetmath, a cell complex is a space obtained by successively attaching discs along their boundaries. It is called a CW complex if the boundary of an n-dimensional disc is constrained to lie in the discs of dimensionMathworldPlanetmath strictly less than n (the (n-1)-skeleton).

Any finite CW complex can be presented as a higher inductive type, by turning n-dimensional discs into n-dimensional paths and partitioning the image of the attaching map into a source and a target, with each written as a composite of lower dimensional paths. Our explicit definitions of π•Š1 and π•Š2 in Β§6.4 (http://planetmath.org/64circlesandspheres) had this form.

Another example is the torus T2, which is generated by:

  • β€’

    a point b:T2,

  • β€’

    a path p:b=b,

  • β€’

    another path q:b=b, and

  • β€’

    a 2-path t:p⁒\centerdot⁒q=q⁒\centerdot⁒p.

Perhaps the easiest way to see that this is a torus is to start with a rectangle, having four corners a,b,c,d, four edges p,q,r,s, and an interior which is manifestly a 2-path t from p⁒\centerdot⁒q to r⁒\centerdot⁒s:



Now identify the edge r with q and the edge s with p, resulting in also identifying all four corners. Topologically, this identification can be seen to produce a torus.

The inductionMathworldPlanetmath principle for the torus is the trickiest of any we’ve written out so far. Given P:T2→𝒰, for a sectionPlanetmathPlanetmathPlanetmath ∏(x:T2)P⁒(x) we require

  • β€’

    a point bβ€²:P⁒(b),

  • β€’

    a path pβ€²:bβ€²=pPbβ€²,

  • β€’

    a path qβ€²:bβ€²=qPbβ€², and

  • β€’

    a 2-path tβ€² between the β€œcomposites” p′⁒\centerdot⁒qβ€² and q′⁒\centerdot⁒pβ€², lying over t.

In order to make sense of this last datum, we need a composition operation for dependent paths, but this is not hard to define. Then the induction principle gives a function f:∏(x:T2)P⁒(x) such that f⁒(b)≑bβ€² and 𝖺𝗉𝖽f(p)=pβ€² and 𝖺𝗉𝖽f(q)=qβ€² and something like β€œπ–Ίπ—‰π–½f2(t)=t′”. However, this is not well-typed as it stands, firstly because the equalities 𝖺𝗉𝖽f(p)=pβ€² and 𝖺𝗉𝖽f(q)=qβ€² are not judgmental, and secondly because 𝖺𝗉𝖽f only preserves path concatenation up to homotopy. We leave the details to the reader (see http://planetmath.org/node/87797Exercise 6.1).

Of course, another definition of the torus is T2:β‰‘π•Š1Γ—π•Š1 (in http://planetmath.org/node/87800Exercise 6.3 we ask the reader to verify the equivalence of the two). The cell-complex definition, however, generalizes easily to other spaces without such descriptions, such as the Klein bottle, the projective planeMathworldPlanetmath, etc. But it does get increasingly difficult to write down the induction principles, requiring us to define notions of dependent n-paths and of 𝖺𝗉𝖽 acting on n-paths. Fortunately, once we have the spheres in hand, there is a way around this.

Title 6.6 Cell complexes