hatcher cell complex

Stream: maths

[Tony]

I'm looking at https://leanprover-community.github.io/mathlib-overview.html and I don't see anything for simplicial complex or delta complex as seen in Hatcher's Algebraic Topology text.

I expect formalizing this could get tricky with complex -vs- geometric realization as a space. Has the community thought about this yet? (Someday it would be really cool to formalize some geometric group theory / cube complex / RAAG work)

[Yaël Dillies]

@Bhavik Mehta and I have been doing simplicial complexes for the combinatorial side of things (Sperner's lemma). Nothing on the algebraic side, really. All of our work is on the branch sperner-again of mathlib.

[Adam Topaz]

We have docs#category_theory.simplicial_object

[Adam Topaz]

Still no geometric realizations of simplicial sets, as far as I remember.

[Johan Commelin]

branch#sset had geometric realizations, but not yet the adjunction.

[Johan Commelin]

But I fear that it's not compatible with mathlibs current docs#category_theory.simplicial_object. Otoh, it shouldn't be too hard to port.

[Adam Topaz]

(I always forget that simplicial objects are in the category theory namespace...)

[Johan Commelin]

Well, we can't PR to your brain to fix that... so maybe we can change mathlib?

[Adam Topaz]

nah, I think it deserves to be in that namespace.

[Adam Topaz]

Maybe the simplicial_object files should move to the category_theory folder?

[Tony]

My guess is dealing with all the attaching maps could get rough. Here's some concrete results that would use the material: http://www.math.utah.edu/pcmi12/lecture_notes/sageev.pdf

Simplicial looks like the place to start thanks. I'd be happy with just a formalized defn of delta-complex or CW-complex.

[Johan Commelin]

There has been discussion about how to formalize CW-complexes on this zulip. You might want to search the history.

[Tony]

Maybe something more formal would be a reasonable goal:
Euclidean Neighborhood Retracts
Homotopy Extension Property
etc.

[Tony]

I was looking for cell, seems people have talked about it!

[Tony]

Something like this from Lee maybe:

Theorem 5.20 (CW Construction Theorem). Suppose X 0  X 1    X n1  X n   is a sequence of topological spaces satisfying the following conditions:

X0

(i) is a nonempty discrete space. Topological Properties of CW Complexes

139

(ii) For each n  1, X n is obtained from X n1 by attaching a (possibly empty) collection of n-cells.

S Then X D n X n has a unique topology coherent with the family fX n g, and a unique cell decomposition making it into a CW complex whose n-skeleton is Xn  for each n.