Homotopic maps induce naturally isomorphic functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

• fundamental_groupoid_functor.homotopic_maps_nat_iso H The natural isomorphism between the induced functors f : π(X) ⥤ π(Y) and g : π(X) ⥤ π(Y), given a homotopy H : f ∼ g

• fundamental_groupoid_functor.equiv_of_homotopy_equiv hequiv The equivalence of the categories π(X) and π(Y) given a homotopy equivalence hequiv : X ≃ₕ Y between them.

Implementation notes #

• In order to be more universe polymorphic, we define continuous_map.homotopy.ulift_map which lifts a homotopy from I × X → Y to (Top.of ((ulift I) × X)) → Y. This is because this construction uses fundamental_groupoid_functor.prod_to_prod_Top to convert between pairs of paths in I and X and the corresponding path after passing through a homotopy H. But fundamental_groupoid_functor.prod_to_prod_Top requires two spaces in the same universe.

These definitions set up the following diagram, for each path p:

        f(p)
    *--------*
    | \      |
H₀  |   \ d  |  H₁
    |     \  |
    *--------*
        g(p)

Here, H₀ = H.eval_at x₀ is the path from f(x₀) to g(x₀), and similarly for H₁. Similarly, f(p) denotes the path in Y that the induced map f takes p, and similarly for g(p).

Finally, d, the diagonal path, is H(0 ⟶ 1, p), the result of the induced H on path.homotopic.prod (0 ⟶ 1) p, where (0 ⟶ 1) denotes the path from 0 to 1 in I.

It is clear that the diagram commutes (H₀ ≫ g(p) = d = f(p) ≫ H₁), but unfortunately, many of the paths do not have defeq starting/ending points, so we end up needing some casting.