Homotopy formalization

Stream: maths

[Roberto Alvarez]

Hello everyone,
I'm thinking about formalizing results from homotopy theory as part of a course on the Lean theorem prover.
I'd be happy to hear from the people that have contributed to the library about missing results that shouldn't be too complicated.
Here is a list of ideas I got from Prof. Bartholdi and @Yury G. Kudryashov
(1) fundamental group of pointed space
(2) more on pointed spaces
(3) pi_n(X), its group structure
(4) show pi_1(S^1) = Z
(5) universal covers
(6) show pi_1(X) is invariant under homotopy equivalence (for connected spaces?)
(7) short exact sequence of a fibration

[Johan Commelin]

Hi! Welcome! @Shing Tak Lam has been doing some homotopy stuff recently.

[Johan Commelin]

In particular, I think (1) is done.

[Filippo A. E. Nuccio]

Hi! I will be very happy to join forces, if possible: I will be teaching a graduate course next year on Lean and the proposal I wrote is precisely about developing the fundamental group. The idea was to let the students solve some sorry's in a pre-compiled file leading them to the definition, not in a mathlib style. For what students will your course be?

[Yury G. Kudryashov]

We have the fundamental groupoid but I'm not sure that we have lots of theory about the fundamental group.

[Yury G. Kudryashov]

@Filippo A. E. Nuccio Roberto is going to formalize something as a part of @Laurent Bartholdi 's course (fall 2021).

[Yury G. Kudryashov]

And the plan is to have some code merged to mathlib in a few weeks.

[Yury G. Kudryashov]

Let's wait for @Shing Tak Lam to avoid duplication of effort.

[Filippo A. E. Nuccio]

Oh nice! Well, this project was really teaching-oriented, for me: so it won't be a problem if by the moment my course starts (spring 2023...) everything will already be in mathlib. I should rather take inspiration from @Laurent Bartholdi 's course, if the material is available.

[Filippo A. E. Nuccio]

I will may be interested in formalizing results about $\pi_1$ for mathlib when the definition will land in it, but now I am busy with LTE so will certainly wait for @Shing Tak Lam.

[Yury G. Kudryashov]

In Laurent's course, students went through materials from @Kevin Buzzard 's course at https://github.com/ImperialCollegeLondon/formalising-mathematics, then each student chose a domain to formalize something new.

[Yury G. Kudryashov]

Roberto chose the fundamental group.

[Filippo A. E. Nuccio]

But that wasn't in Kevin's list, right?

[Yury G. Kudryashov]

No, we used the list to help students learn the syntax.

[Yury G. Kudryashov]

Now they formalize whatever they want (another student is going to formalize complex analysis once I get #10000 merged).

[Filippo A. E. Nuccio]

And how long did it take to make them familiarize with the syntax? My students will be M2 students at "Ecole Normale Superieure" in Lyon (France) which means that they will be (very) good at Math, but with little/no CS culture.

[Yury G. Kudryashov]

2 students covered most of the material in about a month, another two didn't come to today's meeting.

[Filippo A. E. Nuccio]

Thanks for the feedback!

[Shing Tak Lam]

(1) Can be stated as the automorphism group at a point, but there isn't much beyond the definitions atm.
(3) I've been slowly working on it in this branch (warning: code is a mess atm), right now it doesn't seem too hard, but it just seems like a lot of duplication of proofs I wrote for fundamental_groupoid, so I'm not too motivated to work on it at the moment :|
(4) and (5) I have been working on covering spaces in this branch (again, code is a mess). What I have there so far is the definitions, and a start on homotopy lifting. I can PR the definition of covering spaces with some API first, which would unblock (5).
(6) I have an open PR for defining homotopy equivalences, and with that it shouldn't be too hard to do.

For (2) and (7), I don't have anything about it atm. I think someone mentioned they were interested in (2) at some point, but I don't think I've seen anything.

[Yury G. Kudryashov]

About (1): I think that we should define def fundamental_group (x : X) to be the group of endomorphisms of x as an element of fundamental_groupoid X.

[Yury G. Kudryashov]

Then we should split fundamental_groupoid_functor into path.homotopic.quotient.map and a few lemmas about it.

[Yury G. Kudryashov]

In particular, prove that a continuous map f : C(X, Y) between topological spaces (possibly, in different universes) defines a homomorphism π₁ x →* π₁ (f x)

[Yury G. Kudryashov]

Then relate these homomorphisms for two homotopic maps f g : C(X, Y).

[Yury G. Kudryashov]

Then relate homotopy groups of spaces related by homotopy_equiv.

[Yury G. Kudryashov]

Note that mathematicians can say "π₁ x is isomorphic to π₁ y, so we don't care which x do we choose (at least, if we're in a path connected space)" but we can't easily do this in Lean.

[Yury G. Kudryashov]

We need to carry those isomorphisms around.

[Kevin Buzzard]

You could also try pi_n(X) abelian for n>=2. I should think that a lot of this is very do-able even for beginners, if you're not asking for mathlib-ready code (and of course you shouldn't ask the generic maths student to write mathlib-ready code, I tend not to even fuss about non-terminal simps if a project is just a one-off thing and mathlib will likely never be bumped by the student).

[Adam Topaz]

Another formalization target is to develop the theory of covering spaces, and (eventually) obtain the Galois correspondence (with $\pi_1$)

[Filippo A. E. Nuccio]

Sure, I won't ask for mathlib-ready code. If they will want to join, they will eventually learn how to prepare nice code. Yours seems a very nice suggestion, thanks! This will take place in a year or so, so I still have time to prepare; covering spaces were the other option.

[Eric Rodriguez]

eckmann-hilton is already in mathlib, btw

[Laurent Bartholdi]

@Kevin Buzzard yes, I forgot it on the list -- $\pi_n x$ abelian for all $n\ge2$ is definitely among the things I would like to see. In fact, one should aim at much more: $\bigoplus_{n\ge2}\pi_n$ is a Lie algebra over the integers, and a $\pi_1$-module. All of this is pretty explicit, constructing maps and homotopies, so should be doable.

Another one I like a lot, and which is probably not too difficult, is $\Omega\Sigma X\sim F(X)$, in words the loop space of the suspension of $X$ is homotopy equivalent to the free group on $X$ (with the obvious topology coming from words over $X\cup X^{-1}$).

[Kevin Buzzard]

In 2018 Luca Gerolla formalised pi_1 in Lean as a summer project and the thing he had real trouble with was just "obvious" stuff like "if f:[0,1/2]->R and g:[1/2,1]->R are continuous and agree at 1/2, then gluing them together is continuous". But I think the issue was that the API for this sort of thing just didn't exist at the time.

[Junyan Xu]

I think we will have homotopy groups in mathlib very soon (the underlying type is defined in #14724, and the group structure and commutativity when n > 1 seems within reach). But how should we denote the operation? I can think of the following two options:

• Define the group structure only on π_{n+2} and use the + notation (because of commutativity, this seems to be the usual choice), and the only choice if we want the Lie algebra structure; then we could define the group structure on π_1 separately using the * notation (which will lead to a bit of code duplication, but the add_comm_group instance will be available only on π_{n+2} anyway) and show it's isomorphic to docs#fundamental_group (which is multiplicative).

• Define the group structure on all π_{n+1} and use the + notation. Then to talk about the π_1-module structure or isomorphism with fundamental group we'd have to use multiplicative π_1.

Which one do people prefer?

[Kevin Buzzard]

What a fascinating question! Forgive my ignorance -- what extra structure is there on $\pi_2(X)$ other than that of an abelian group? You mentioned lie algebras -- is it a Lie module over something?

[Kevin Buzzard]

We're running into this sort of thing in number theory as well: I want to look at group cohomology of Galois groups Gal(L/K) (with law * but it's really function.comp) acting on abelian groups like $L^\times$ with group law also multiplication.

[Kevin Buzzard]

The group law is not even defined for n=0. For n=1 you have a group structure and for n=2 it's abelian. What does pi_3(X) have that \pi_2(X) doesn't?

Can type class inference handle this sort of situation? You might end up having to define an addition on pi_0 (send everything to x?) and then try and convince type class inference that it's only a group for n>=1 and only an abelian group for n>=2, and it's not going to be looking at local hypotheses to find these assumptions...

[Patrick Massot]

Option 1 seems better to me.

[Kevin Buzzard]

Do you want the fundamental object to be higher_pi_succ_succ (n : nat) (x : X)?

[Oliver Nash]

I also prefer option 1. I think one day we’ll have to have a way to uncouple our algebraic classes from their notation.

[Kevin Buzzard]

This is why I'm asking what pi_3 has that pi_2 doesn't: I'm wondering whether the set of pi's for n>=3 also needs to be "special cased" later

[Oliver Nash]

@Kevin Buzzard I think the “Lie algebra” mentioned is the Whitehead product. It’s a generalisation of the action of the fundamental group on the higher groups.

[Oliver Nash]

My reading is that is the pi_2 and above that will be special-cased.

[Oliver Nash]

(Or equivalently, that pi_0 and pi_1 will be special-cased.)

[Kevin Buzzard]

So is this all just some special case of some well known categorical abstraction which tells me exactly what the structure really is and has consequences such as pi n X is a pointed type for n>=0, a group for n>=1 and an abelian group for n>= 2?

[Kevin Buzzard]

My only worry is what about when someone comes along who is an expert in whatever pi_3 is that pi_2 isn't and says it's inconvenient to do what they want to do because of it not working for stupid pi_2. But I think that this is a bit of a hypothetical worry at this point :-)

[Kevin Buzzard]

We seem to manage with fin n not having a point (a zero) for n=0 and not having a 1 for n=0,1. I guess it's a bit like that

[Reid Barton]

There's no new property or structure on $\pi_3$ and so on, at least not considered in isolation.

[Reid Barton]

Kevin Buzzard said:

So is this all just some special case of some well known categorical abstraction which tells me exactly what the structure really is and has consequences such as pi n X is a pointed type for n>=0, a group for n>=1 and an abelian group for n>= 2?

It's a pointed set with n compatible group structures, which (by a theorem/computation) reduces to what you wrote.

[Reid Barton]

Basically just the Eckmann-Hilton argument: two compatible group structures have to be equal (and abelian), so then by "all horses are the same color" it doesn't matter if we add a third compatible group structure.

[Reid Barton]

https://en.wikipedia.org/wiki/Whitehead_product for the Lie algebra structure Junyan mentioned

[Reid Barton]

I think we will probably want some way to refer to the group structure on pi n uniformly for n = 1 and for n >= 2. For example if $F \to E \to B$ is a fiber sequence then there's a connecting homomorphism $\pi_{n+1} B \to \pi_n F$ and it is still a group homomorphism for $n = 1$.

[Reid Barton]

How strange would it be to give pi 1 both + and * group structures with the same definition?

[Kevin Buzzard]

The only reason this might be a bad idea (other than the obvious reason that it's weird) would be that if later on someone wants to use * on higher pi_n for something else. This was why I was asking about other structures on higher pi.

[Reid Barton]

Alternatively, define * on all pi n (n >= 1) and then define + to be the same as * for n >= 2

[Kevin Buzzard]

Then will you be able to get add_comm_group to fire or will it get stuck looking for the proof that 2<=n?

[Reid Barton]

In the Agda libraries they define the group structure on $\pi_n$ by doing something like your higher_pi_succ_succ. I guess the Lean equivalent might be

instance : group (pi (n + 1) X) := ...
instance : add_comm_group (pi (n + 2) X) := ...

[Reid Barton]

Maybe some [fact (n >= 2)] approach is okay too

[Reid Barton]

I guess a minimal test case for this stuff would be to define an isomorphism $\pi_{n}(\Omega X) \cong \pi_{n+1}(X)$ (of groups for $n \ge 1$, or possibly of abelian groups for $n \ge 2$).

[Reid Barton]

From the PR it sounds like maybe the strategy is to build this as an isomorphism of sets, and then transfer the group structure from left to right?

[Junyan Xu]

Reid Barton said:

https://en.wikipedia.org/wiki/Whitehead_product for the Lie algebra structure Junyan mentioned

I actually didn't know about what the Lie algebra structure was, but it's mentioned two posts above my post.

Reid Barton said:

Maybe some [fact (n >= 2)] approach is okay too

The main problem I see is that the definition of pi n depends on fin n → I (i.e. the cube I^n), and to define the group structure you then need to resort to the non-defeq type equality fin n.pred.succ = fin n when n > 0, which may bite you, so it's best to write pi (n+1) X. That's probably why in Agda they did it that way, and we should probably follow suite. The add_comm_group instance could take a [fact (n > 1)] though, because commutativity is prop not data.

instance : group (pi (n + 1) X) := ...
instance : add_comm_group (pi (n + 2) X) := ...

Does this mean they have + and * meaning the same thing for n > 1? Then we could certainly follow, as you suggested.

Reid Barton said:

From the PR it sounds like maybe the strategy is to build this as an isomorphism of sets, and then transfer the group structure from left to right?

What we want to utilize is rather the bijections $\pi_1(\Omega^n X)\cong \pi_{n+1}(X)$ (one for each element of fin (n+1), and we'd use two to show commutativity). The underlying type of the homotopy group is defined in the usual way, as maps $I^n\to X$ sending $\partial I^n$ to x (named gen_loop n x, which is essentially $\Omega^n X$) up to homotopy relative to $\partial I^n$, and the plan is indeed to transfer the group structure from left to right; however it's easy to see the transferred group operation agree with the usual definition, i.e. $(f+g)(t_0,t_1,\dots,t_n)=f(2t_0,t_1,\dots,t_n)\text{ for }t_0 \leq 1/2\text{ and }g(2t_0-1,t_1,\dots,t_n)\text{ for }t_0 \geq 1/2$ (I suspect this will hold even definitionally when using the zeroth bijection between $\pi_1(\Omega^n X)$ and $\pi_{n+1}(X)$).

I also want to hear about opinions about the notation for the underlying type. Currently $\pi_n(X,x)$ denoted π n x, with the space X implicit. Should we make it explicit? And can we make the notation prettier? I seem to remember that notations like π_n(X,x) doesn't work, and you have to add brackets, something like π_[n](X,x)? And should we make it a localized notation or global? Currently π n x is just a local notation and making the single letter π global is obviously bad, but a complicated notation like π_[n](X,x) could probably be made global, as in the case of C(X, Y) for docs#continuous_map.

[Damiano Testa]

In my experience, the base point for the fundamental group is rarely moved around. Maybe it makes sense to use inhabited X as an instance and only mention the space, using default as the basepoint? This is closer to the standard abuse of notation in maths.

[Kevin Buzzard]

I think there might be some subtleties here.

[Adam Topaz]

In my experience, the base point plays a crucial role! For example the torsor of paths $\pi_1(X,x,y)$ is a fairly important object in anabelian geometry. We do have some tricks that let us ignore the base-point, essentially by considering the fundamental group not as a group but as an object in the category of groups (or profinite groups in the etale case) with "outer" morphisms, i.e. where $Hom^{Out}(G,H) = Hom(G,H)/Inn(H)$.

[Adam Topaz]

Personally I would be fine with π_ n X x as notation for $\pi_n(X,x)$

[Damiano Testa]

Ok, I'm convinced on including the basepoint explicitly and in the notation!

[Reid Barton]

We could use a bundled "pointed space" type and write π_ n ⟨X, x⟩--too bad we can't use (X, x)

[Kyle Miller]

I wonder if there's some trick where π_ n X could mean π_ n ⟨X, default⟩? I'm not sure you can write a coercion that depends on a typeclass like that (inhabited in this case).

[Yaël Dillies]

This, maybe?

def π_ n (X : Type*) (n : ℕ) (x : X := by exact default) : Type* := sorry

[Kyle Miller]

That suggests a potential solution:

import tactic
--import category_theory.category.Pointed

universes u

meta def tactic.default := `[exact default]

structure Pointed : Type (u + 1) :=
(X : Type u)
(point : X . tactic.default)

#check (⟨ℕ⟩ : Pointed)
#check (⟨ℕ, 37⟩ : Pointed)

This means you can write π_ n ⟨X⟩ for π_ n ⟨X, default⟩.

(Note that by exact default doesn't work in Lean 3 since that tactic will be resolved immediately. I think it works in Lean 4.)

[Yaël Dillies]

Nifty use of docs#Pointed!

[Roberto Alvarez]

Kyle Miller said:

This means you can write π_ n ⟨X⟩ for π_ n ⟨X, default⟩.

I don't know how to actually implement this notation, am I supposed to duplicate the Pointed structure so that it includes the tactic?