Zulip Chat Archive

Stream: Is there code for X?

Topic: CW Complex


view this post on Zulip Adam Dionne (Jan 21 2021 at 19:11):

Has n-dimensional CW complex (https://en.wikipedia.org/wiki/CW_complex) been formalized in Lean? What about an infinite dimensional CW complex?

view this post on Zulip Johan Commelin (Jan 21 2021 at 19:25):

@Adam Dionne Nope, we don't have CW complexes yet.

view this post on Zulip Johan Commelin (Jan 21 2021 at 19:25):

I've done simplicial sets in branch#sset and I hope to add them to mathlib at some point in the future.

view this post on Zulip Johan Commelin (Jan 21 2021 at 19:26):

@Reid Barton Or maybe you did CW in your repo? I actually don't know.

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 08:18):

It's time we had these things, and also simplicial homology

view this post on Zulip Reid Barton (Jan 22 2021 at 11:43):

No, I didn't define CW complexes.


Last updated: May 16 2021 at 05:21 UTC