two definitions of CW-complexes

Stream: mathlib4

[Floris van Doorn]

In #12502 the categorical definition of a CW-complex will be added: it's a sequence of pushout diagrams, where the n+1-skeleton is a pushout of the n-skeleton with some balls glued to it.

A student of mine, @Hannah Scholz has formalized a different definition of CW-complexes: a closed subset of a Hausdorff topological space is a CW-complex, if it is decomposable as a disjoint union of open balls, which are attached on their boundaries to balls of lower dimensions. To be precise, our definition is here:
https://github.com/scholzhannah/CWComplexes/blob/6943745f0ac8c4783acc9c8d1e2f0e1629d2d988/CWcomplexes/Definition.lean#L47

I think this second definition will be a lot nicer to work with in a lot of specific cases (e.g. taking unions of CW-complexes, adding an additional cell to an existing CW-complex). In the second definition, you can do all reasoning in a single topological space, and reason about subsets. Instead in the categorical definition you have an infinite sequence of spaces, and this will be more annoying to deal with when reasoning explicitly, I think. Though I am happy to concede that for more categorical arguments the categorical definition might be preferable.
As an example, Hannah has already formalized the product of CW-complexes for compactly generated spaces (which is surprisingly tricky!): https://github.com/scholzhannah/CWComplexes/blob/6943745f0ac8c4783acc9c8d1e2f0e1629d2d988/CWcomplexes/Product.lean#L83

I would like to propose that we add both definitions to Mathlib, referencing each other of course, and hopefully with an equivalence proof. The reason that I think it's good to have both, is that it's still unclear which definition is easier to work with. As an experiment, I would be interested to see the definition of [EDIT: the product of two] CW-complex[es] using the categorical definition (where does the requirement that the space is compactly generated come in?)

cc @Dean Young @Jiazhen Xia @Joël Riou @Patrick Massot @Oliver Nash (and anyone else)

[Joël Riou]

I would also think that we want both definitions in mathlib, and ways to go from a def to the other. (The result about products of CW-complexes is great, because without extra assumptions, it is wrong!)

[Oliver Nash]

I'm late replying but I'm definitely in favour of have both definitions (with glue between them).

[Dean Young]

Related to products is internal hom and exponentiablity. Evidently exponentiable is equivalent to locally compact in locales (see attached paper). Hannah's proof about products of CW-complexes being a CW-complex carries over to localic ones, I think.

A categorical proof of the equivalence of local compactness and exponentiability in locale theory (Christopher F. Townsend).pdf

[Dean Young]

The paper On spaces having the homotopy type of a CW-complex, Trans. Amer. Math. Soc. 90 (2) (1959), 272-280. shows that locally finite CW complexes are locally compact ones, which may carry over to the setting of locally compact locales.

[I,I] cannot be a CW-complex, so there is no result like that for spaces of continuous functions. It's too bad.

[Dean Young]

The benefit here seems related to condensed and pyknotic math as well, maybe with a site fashioned out of locally compact locales.

[Jiazhen Xia]

#12502 (categorical definition) has been merged. Thank you (E. Dean Young, Joël Riou, Yaël Dillies, Floris van Doorn, ...) for your help with the PR!

I also think we should have both definitions, and I'd be happy to help with the proof that they are equivalent.

Floris van Doorn said:

I would be interested to see the definition of CW-complex using the categorical definition (where does the requirement that the space is compactly generated come in?)

A proof that every CW-complex, defined categorically, is compactly generated can be found here (Proposition 3.3).

[Dean Young]

Can someone help me with the full view of the progress here in terms of imports?

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0AVCSdCAcwE8cBhAdUonHQFMAPAKAFp25UYYwBnAFwB6YUyQA7MFAgA3RlHYBjeiACuE4DAoktqNbmARhIFBmwAWAPoATCEv7DkaTFmEEipMsJp0GLHB4QdABiX3owJmYAEgAGIA

@Joël Riou @Hannah Scholz @Floris van Doorn

import Mathlib.Topology.CWComplex

#check RelativeCWComplex.sphereInclusion
#check RelativeCWComplex
#check RelativeCWComplex.toTopCat
#check CWComplex.isEmpty_sk_zero
#check RelativeCWComplex.AttachGeneralizedCells.inclusion
#check RelativeCWComplex.toTopCat
#check RelativeCWComplex.instCoeTopCat
-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/CWComplex.html#CWComplex$0

[Floris van Doorn]

I don't understand what you're asking.

[Floris van Doorn]

The second definition is not yet PR'd to Mathlib. Hannah is working on generalizing her formalization from CW-complexes to relative CW-complexes.

[Dean Young]

Ok thanks- that's all I wanted to know. You may also want to work on the "internal" universe:

TETRAVALENCE.png
(Nov 15th)

[Martin Dvořák]

E. Dean Young said:

Ok thanks- that's all I wanted to know. You may also want to work on the "internal" universe:

TETRAVALENCE.png
(Nov 15th)

I don't know what it is, but it looks beautiful.

Do you have similar illustrations for other areas, too?

[Dean Young]

@Martin Dvořák thanks so much Martin.

Well -- and since its the CW thread -- I spent a lot of time drawing the Jar filling lemma that Jiazhen is showed, and base change too.

HEP.png

proj.png

basechange.png

windowframe.png

But they're not as beautiful.

This one is the most beautiful:

StringDiagramGenerator.py

After I got it working I asked Kyle Miller about his work in knots and his program recognized K₄!

image-3.png

The cells provided in this generator (in python3) can model a cartesian closed category

P.S. emoji code:

inductive valenzzustand where
| tetravalenz
| univalenz
| zunehmendbivalenz
| abnehmendbivalenz

notation "🌞" => valenzzustand.tetravalenz
notation "🌩" => valenzzustand.univalenz
notation "🌓" => valenzzustand.zunehmendbivalenz
notation "🌗" => valenzzustand.abnehmendbivalenz

#check 🌞
#check 🌩
#check 🌓
#check 🌗

def valenz (zustand : valenzzustand) : Nat :=
  match zustand with
  | 🌩   => 1
  | 🌓   => 2
  | 🌗   => 2
  | 🌞   => 4

[Dean Young]

Here's one, a math joke:

Screenshot 2024-11-16 at 11.18.31 PM.png

[Kevin Buzzard]

I think posts like this would be more suited to Martin Dvorak's Lean Discord (which has a memes channel). On this Zulip we like to keep to the point.

[Dean Young]

Ok no problem