homotopies and stuff

Stream: maths

[Jean Lo]

What is the state of algebraic topology in mathlib?

I was recently looking at some stuff about covering spaces for an undergrad project, and looked around mathlib to see what has been formalised & how it's been done. Surprisingly, I didn't find many things that I recognised.

A search for some relevant words on zulip and in the commit history turned up a few instances of conversations about doing things like the homotopy groups or simplicial complexes (such as here, but the branch it links to doesn't exist anymore,) and also this separate repository from @Reid Barton which contains a lot of cool stuff.

Is there any work currently being done on getting this stuff into mathlib? In particular, are there any things that an interested but relatively-new-to-all-of-this student like me could possibly start doing that might be helpful?

[Reid Barton]

I'm not aware of any formalization of covering space theory. I certainly haven't done it. I think it would make a great project.

[Reid Barton]

I actually meant to sit down at some point and sketch out a spec of what would be involved to check how feasible it is in the current state of mathlib.