Simplicial Complex vs CW Complex for Topology?

Stream: mathlib4

[Mr Proof]

In terms of doing topology in Lean...

What sort of data structure might be best to catalogue a database of topological spaces?

I think CW complexes might be more efficient notationally, but simplicial complexes have an simple elegance to them also.

Some topological spaces might be defined in other ways for which no known CW-complex is yet known. But to me that is more like an implicit definition.

I imagine that by having a database of topological spaces as, say, CW-complexes, then the proofs of isomorphims etc would be simplified with a set of rules on the complexes.

(BTW, anyone know of any databases of topological spaces with an example CW-complex or simplicial complex for each one?)

I would like to start with a database of simple topological spaces (nothing too wild!)

A question is: Should the primary definition of a topological space be in terms of a CW-complex or should the CW-complex be derived by a proof. My opinion is that it would be nicer to do the first option - since then it encourages most topological spaces to be defined in a similar manner for compatibility.

There would have to be proofs e.g. that the topology given by $|x|=1$ in 3 dimensions is equivalent to a CW-complex of cells such as some tetrahedron arrangement. I guess this would be done by mapping different patches.

[Aaron Liu]

this only gives you topological spaces which can be represented as CW complexes (so no rational numbers or cantor set), which could be a good thing or a bad thing

[Mr Proof]

Aaron Liu said:

this only gives you topological spaces which can be represented as CW complexes (so no rational numbers or cantor set), which could be a good thing or a bad thing

Yes, I don't know if there is a name for "all non-pathological topologies that can be represented by finite CW complexes". But it would include all the simple finite dimensional smooth manifolds and such like. So I think it would be pretty useful.

I'm always surprised at how many things have been crammed into the label of topology, when I'm sure the original idea of Poincare was just to think about higher dimensional surfaces. That's the problem with axiomatizing your definitions, then you find out all these other weird things fit your definition I suppose!

I just saw Lean already has CW-complexes: https://florisvandoorn.com/theses/HannahScholz.pdf

Also I found this paper: https://florisvandoorn.com/theses/HannahScholz.pdf

Anyone know if there's any CAS software that allows you to do calculations on CW-complexes or topologies? This seems to be lacking. Perhaps it is just too impractical?

(I've always wanted some software which you can just type

O(5)/O(4)

for example and it returns

S^4

(Well Chat-GPT can do it. But that doesn't count!)

There is something called fKenzo but I don't know if it's being maintained.