CW Complex

Stream: Is there code for X?

[Adam Dionne]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Reid Barton]

No, I didn't define CW complexes.

[Dean Young]

@Hannah Scholz
@Floris van Doorn
@Jiazhen Xia

Maybe CW-complexes could have a cool notation based on the concept of a higher inductive type (https://ncatlab.org/nlab/show/higher+inductive+type).

[Dean Young]

https://www.mathematics.uni-bonn.de/him/video-recordings/tp_2024_02_school_video/workshop-asymptotics-of-random-convex-sets-fluctuations-and-large-deviations/steve-awodey-what-is-hott

[Dean Young]

I wanted the == 's to provide the information of how a particular cell that gets glued in somehow

[Dean Young]

(like a formula for an attaching map)

[Jiazhen Xia]

@Dean Young Thanks for suggesting intuitive notations. We can work on this together. (The definition of CW-complexes will soon be merged into mathlib.)