Zulip Chat Archive

Stream: Is there code for X?

Topic: Do we have CW complexes?

Roman Bars (Mar 24 2021 at 07:48):

Say how far are we from writing down the term corresponding to https://en.wikipedia.org/wiki/Whitehead_theorem?

Kevin Buzzard (Mar 24 2021 at 07:49):

We don't have homotopy groups

Kevin Buzzard (Mar 24 2021 at 07:52):

But to be quite frank this should all be accessible nowadays. I know a student at Imperial made pi1 in 2018 but never PRed it.

Roman Bars (Mar 24 2021 at 07:55):

But with pi1 you can work in terms coverings which seems like it might be easier. If they proved the equivalence between coverings and loops that's more convincing.

Kevin Buzzard (Mar 24 2021 at 07:55):

They did the loop definition

Scott Morrison (Mar 24 2021 at 12:19):

Even defining a CW complex is pretty hairy. :-) Someone really should do it!

Scott Morrison (Mar 24 2021 at 12:20):

There's a non-trivial mutual recursion to describe k-skeletons and k-dimensional attaching maps.

Yaël Dillies (Mar 24 2021 at 18:54):

Bhavik and I are setting up the basics of simplicial complexes. This is still quite far off CW complexes though.

Kevin Buzzard (Mar 24 2021 at 19:10):

@Scott Morrison will simplicial complexes be as hairy?

Adam Topaz (Mar 24 2021 at 19:34):

This definition is trivial to write down:
https://en.wikipedia.org/wiki/Abstract_simplicial_complex

Adam Topaz (Mar 24 2021 at 19:34):

Of course, relating it to topology is a different story

Bhavik Mehta (Mar 24 2021 at 23:18):

Adam Topaz said:

Of course, relating it to topology is a different story

Yup, we're working on the topological aspect more anyway - they're much easier to work with than CW complexes in any case

David Wärn (Mar 24 2021 at 23:48):

Do CW complexes form a coinductive type? Writing CW A n for a CW-complex relative a base space A only having cells in dimensions n and above, an element of CW A n should give you (1) some index type I for the n-cells together with an I-index family of maps to A, and (2) an element of CW A' (n+1), where A' depends on the data in (1) ...

Scott Morrison (Mar 24 2021 at 23:51):

Wah... I like my CW complexes built from the bottom up, but maybe this is naive.

David Wärn (Mar 24 2021 at 23:58):

I think they're built from the bottom up in the same way that an infinite list is built from the empty list by appending lots of elements

Adam Topaz (Mar 25 2021 at 00:00):

I think the usual approach is to write an infinite dimensional cw complex as a limit of its finite dimensional skeleta, right?

Adam Topaz (Mar 25 2021 at 00:01):

And the finite dimensional ones are colimits of some sort, so seem more inductive IMO

Adam Topaz (Mar 25 2021 at 00:02):

Of course the limit can be seen as a coinductive construction

Adam Topaz (Mar 25 2021 at 00:03):

But the reason cw complexes are good is because you can do inductive proofs with them, so a top down approach doesn't make sense

David Wärn (Mar 25 2021 at 00:39):

What I was trying to do was describe the "type of all CW complexes", where by CW complex I mean the data "for every n, a collection I_n of n-cells together with attaching maps...". Indeed you get a topological space from such a gadget by taking the colimit of its skeleta.

This data presenting a CW complex is a bit complicated because the codomains of the attaching maps depend on previous data. Probably what you'll have to do in Lean is instead define what it means for a given space to be (up to homeomorphism) a CW complex (it means that you have a sequence of subspaces, such that yadda yadda), rather than defining these concrete examples of CW complexes

Adam Topaz (Mar 25 2021 at 00:50):

Actually the definition from Wikipedia seems very doable https://en.m.wikipedia.org/wiki/CW_complex

See the section titled "formulation"

Yury G. Kudryashov (Mar 25 2021 at 00:51):

I think that like with topological fibrations we need both abstract CW-complexes and a way to say "this topological space is a CW-complex".

Adam Topaz (Mar 25 2021 at 00:56):

(sorry what I said above was nonsense, they are indeed colimits of the skeleta, so there is really no way I can see that a cw complex can be coinductive)

Yury G. Kudryashov (Mar 25 2021 at 01:00):

If you already have a topological space, then you can just say that a CW-complex structure is something like (untested)

structure CW_complex (X : Type u) [topological_space X] :=
(cells : nat → Type v) -- probably we can reuse the same universe here
(maps : Π (n : nat) (i : cells n), local_equiv (fin n → real) X) -- or euclidean space?
(source_eq : ∀ n i, (maps n i).source = ball 0 1)
(cont_on : ∀ n i, continuous_on (maps n i) (closed_ball 0 1))
(cont_inv : ∀ n i, continuous_on (maps n i).symm (maps n i).target)
(bd_subset : ∀ n i, maps_to (maps n i) (sphere 0 1) (⋃ (m < n) j, (maps m j) '' (closed_ball 0 1)))

Yury G. Kudryashov (Mar 25 2021 at 01:01):

API should turn maps into a collection of local_homeomorphs.

Yury G. Kudryashov (Mar 25 2021 at 01:01):

Probably we need better field names and possibly I've missed something in the definition.

Yury G. Kudryashov (Mar 25 2021 at 01:04):

Also, it's possible that a better solution is to define an abstract CW-complex, and use homeomorph (c : CW_complex) X with a custom constructor from what I wrote in the previous message.

David Wärn (Mar 25 2021 at 09:26):

Yes, we'll need abstract CW complexes since many constructions build the skeleta recursively, and then you only know the total space at the end of the recursion. Actually this is not too difficult to express in Lean, you can write something like this

-- A type witnessing that X' is obtained from X by attaching n-cells
structure CW_aux (X : Top) (X' : Top) (n : ℕ) :=
(inclusion : X ⟶ X')
(cells : Type)
-- should also have, for each i in cells a map ∂D^n ⟶ X, and
-- a homeomorphism between X' and the result of gluing these n-cells to X

structure CW_complex :=
(skeleta : ℕ → Top)
(foo : Π n, CW_aux (skeleta n) (skeleta (n+1)) n)

What's coinductive about this definition is that you have an infinite sequence of spaces. The trick I was confused about is that you first tell Lean "there is a sequence of spaces", and only after this do you say "these spaces are built from a gluing procedure"

Mario Carneiro (Mar 25 2021 at 11:10):

Definitions which have types changing in a recursion are generally a bad idea. I like Yury's last suggestion: We have a concrete (inductive?) type CW_complex which denotes (representations of) abstract CW_complexes, and a reification operation (which I suppose can be coe_sort) which converts this representation into a type with a topological space structure on it based on intervals and simplices, and finally the is_CW_complex X function can just be defined as ∃ cw : CW_complex, nonempty (cw ≃ₜ X).

Scott Morrison (Mar 25 2021 at 21:22):

Completely abstract CW complexes aren't really possible. You have to reify the (boundary of the) n-skeleton in order to describe the attaching maps for the (n+1)-cells, which are genuinely continuous maps with no possible "abstract" representation.

Scott Morrison (Mar 25 2021 at 21:40):

Hence my claim above that you need to define the abstract representation of an n-dimensional CW complex and its reification in a mutual recursion.

Mario Carneiro (Mar 25 2021 at 21:51):

I'm not sure I see the reason for a mutual recursion here. The definition of an abstract CW complex can be like in the wiki page: a downward closed collection $\Delta$ of finite sets, and one definition for the reification that I can see is the set of convex linear combinations of an element of $\Delta$ .

Mario Carneiro (Mar 25 2021 at 22:13):

easy peasy: (modulo a topological space structure on finsupp which seems surprisingly missing)

import data.finsupp.basic data.real.basic topology.instances.real

noncomputable theory

instance finsupp.topological_space (ι α) [topological_space α] [has_zero α] :
  topological_space (ι →₀ α) := sorry

universe u
structure CW_complex : Type (u+1) :=
(α : Type u)
(sets : set (finset α))
(down_closed : ∀ (S ∈ sets) (T ⊆ S), T ∈ sets)

instance : has_coe_to_sort CW_complex :=
⟨_, λ C, {f : C.α →₀ ℝ // f.support ∈ C.sets ∧ f.sum (λ _ x, x) = 1}⟩

instance CW_complex.topological_space (C : CW_complex) : topological_space C :=
subtype.topological_space

def is_CW_complex (X : Type*) [topological_space X] :=
∃ C : CW_complex, nonempty (C ≃ₜ X)

Adam Topaz (Mar 25 2021 at 22:14):

This is a simplicial complex, no?

Scott Morrison (Mar 26 2021 at 00:32):

CW complexes are not combinatorial objects.

Scott Morrison (Mar 26 2021 at 00:34):

That said, nearly every actual construction of one proceeds from essentially combinatorial data (e.g. the attaching maps are described by identifying a k-sphere inside the n-skeleton, which itself is built out of k-cells in an easy way, and then using the "obvious" submersion corresponding to a particular element of \pi_n(S^k)). But in principle the attaching maps can be nastier, and require writing down an "arbitrary" continuous map.

Scott Morrison (Mar 26 2021 at 00:34):

But that is just saying that we want a bunch of auxilliary constructors for CW complexes that start from more combinatorial data.

Damiano Testa (Mar 26 2021 at 05:47):

Up to homotopy, every CW-complex with finitely many cells is homotopy equivalent to a simplicial complex, though, right?

Even more, every CW-complex with finitely many cells is homotopy equivalent to a finite topological space! It is difficult to get more combinatorial than this!

Homotopies are weird.

Scott Morrison (Mar 26 2021 at 06:57):

Damiano Testa said:

Even more, every CW-complex with finitely many cells is homotopy equivalent to a finite topological space! It is difficult to get more combinatorial than this!

I think this is only weak homotopy equivalence: https://ncatlab.org/nlab/show/finite+topological+space. Still, :head_bandage:.

Damiano Testa (Mar 26 2021 at 09:58):

Ah yes, of course: Scott, thanks for the correction!

Jakob Scholbach (Mar 27 2021 at 14:46):

It might be worth pointing out that CW complexes are, up to homotopy equivalence, the cofibrant objects in the mixed model structure on topological spaces. https://ncatlab.org/nlab/show/model+structure+on+topological+spaces#mixed_model_structure Generally speaking, for a cofibrantly generated model structure (which, however, the mixed model structure is not) the cofibrant objects are indeed very combinatorial: retracts of transfinite compositions of pushouts of generating cofibrations.

I am currently trying to lean-ify §2 in Cisinski's book on higher homotopical structures (=definitions of model structure notions, small object argument https://ncatlab.org/nlab/show/small+object+argument, construction of model structures on presheaf categories). If someone is interested in joining in, I would be very happy! With these tools and enough general categorical properties of a (convenient) category of topological spaces (so that the small object argument applies), the Whitehead theorem will be a formal consequence, @Roman Bars .