Fundamental groupoid of product spaces

Stream: general

[Praneeth Kolichala]

I was thinking of proving some basic properties of the fundamental groupoid functor, such as the fact that it preserves products and coproducts, or the fact that it maps homotopic maps to equivalent (i.e. naturally isomorphic) maps between groupoids.

To this end, I wrote a proof of the following fact: given an indexed family of topological spaces $X_i$ for $i\in \mathcal{I}$, we have

$\pi\left(\prod_{i\in\mathcal{I}} X_i\right) = \prod_{i\in\mathcal{I}} \pi X_i$

Here, $\pi$ is the fundamental groupoid functor.

The code so far is here: https://github.com/prakol16/lean-fundamental-groupoid/tree/master. I'd like to pull request this to mathlib sometime soon, although I'm not really sure how big changes are supposed to be before a pull request.

In the meantime, I'd appreciate any comments about the code/style. I'd also like to know what the usual procedure is for going from products indexed over a family $\mathcal{I}$ to binary products. I'd like to be able to just plug in $\mathcal{I} = \{0, 1\}$, but maybe it is actually easier to just redo all the lemmas for binary products as well, because I notice in mathlib, some theorems are done separately for binary product types and for pi types.

[Johan Commelin]

@Praneeth Kolichala Welcome! Thanks for working on this!

I'm not really sure how big changes are supposed to be before a pull request

We generally advise to start with something small, just to get acquainted with the process. So if you have some standalone piece of < 50 lines, that would make a great first PR. Even after that, most PRs try to stay < 300 lines.
More importantly, PRs should follow the "unix philosophy" of doing one thing, and doing it well. That makes them so much easier to review.

I'd appreciate any comments about the code/style.

A lot of the code looks pretty good style-wise. Although I noticed some things that don't follow the style guide (e.g., :` should be at the end of the line, not the beginning of the next line).

I'd also like to know what the usual procedure is for going from products indexed over a family $\mathcal{I}$ to binary products

It is true that mathlib duplicates the API for binary products. Hopefully, you can deduce it from your general API by plugging in I = bool or I = fin 2. But probably there will be some hiccups. Those hiccups are exactly the reason why we duplicate the API: you want to deal with them once, instead of at every place the results are used.

[Yury G. Kudryashov]

The main issue with going from indexed products to binary products is that X × Y allows X and Y to be in different universes while Π i : fin 2, Type* doesn't allow this.

[Yury G. Kudryashov]

Probably, we should add a version of docs#prod_equiv_pi_fin_two that inserts appropriate ulifts on the right.

[Yury G. Kudryashov]

But you need to go through an explicit equiv or homeomorph anyway.