Algebraic topology

Stream: maths

[Mark Lavrentyev]

Is anyone working on developing some covering space stuff for mathlib? Wondering if there's an approach that works particularly nicely with fundamental groupoids (perhaps via covering groupoids, described in Ch 10 of Brown's Topology & Groupoids textbook)?

[Anatole Dedecker]

#16087 has been open for quite some time (cc @Thomas Browning)

[Rémi Bottinelli]

I'm not, but following Brown to develop some groupoid theory! Would welcome some collaboration/help! Since groupoid covering is on a path to plenty of combinatorial group theory results, I think there is a really good incentive to develop that.

[Filippo A. E. Nuccio]

This is something we discussed with @Thomas Browning and would be in our radar. I have developed H-spaces in #16029 hoping to develop Serre's thesis. But the project on covering spaces has been dormant for quite a while.

[Thomas Browning]

@Jordan Brown is working towards homotopy lifting. But we are also waiting on #16087.

[Mark Lavrentyev]

Got it - thanks for the context all!

[Rémi Bottinelli]

@Thomas Browning Can I ask for a ping when homotopy lifting is included? I'm trying to set up coverings of groupoids, and having the connection "covering of spaces" -> "covering of groupoids" would be nice. Thanks!

[Thomas Browning]

Sure!