Homotopic maps induce naturally isomorphic functors #
Main definitions #
FundamentalGroupoidFunctor.homotopicMapsNatIso HThe natural isomorphism between the induced functorsf : π(X) ⥤ π(Y)andg : π(X) ⥤ π(Y), given a homotopyH : f ∼ gFundamentalGroupoidFunctor.equivOfHomotopyEquiv hequivThe equivalence of the categoriesπ(X)andπ(Y)given a homotopy equivalencehequiv : X ≃ₕ Ybetween them.
Let F be a homotopy between two continuous maps f g : C(X, Y).
Given a path p : Path x₁ x₂ in the domain, consider the following two paths in the codomain.
One path goes along the image of p under f, then along the trajectory of x₂ under F.
The other path goes along the trajectory of x₁ under F, then along the image of p under g.
These two paths are homotopic.
Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
functors map f and map g on fundamental groupoids.
Instances For
Homotopy equivalent topological spaces have equivalent fundamental groupoids.
Instances For
Old proof #
The rest of the file contains definitions and theorems required to write the same proof in a slightly different manner.
The proof was rewritten in 2025 for two reasons:
- the new proof is much more straightforward;
- the new proof is fully universe polymorphic.
TODO: review which of these definitions and theorems are useful for other reasons, then deprecate the rest of them.
The path 0 ⟶ 1 in ULift I
Instances For
Abbreviation for eqToHom that accepts points in a topological space
Instances For
If f(p(t) = g(q(t)) for two paths p and q, then the induced path homotopy classes
f(p) and g(p) are the same as well, despite having a priori different types
These definitions set up the following diagram, for each path p:
f(p)
*--------*
| \ |
H₀ | \ d | H₁
| \ |
*--------*
g(p)
Here, H₀ = H.evalAt 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.
An abbreviation for prodToProdTop, with some types already in place to help the
typechecker. In particular, the first path should be on the ulifted unit interval.
Instances For
The diagonal path d of a homotopy H on a path p
Instances For
The diagonal path, but starting from f x₀ and going to g x₁
Instances For
Proof that f(p) = H(0 ⟶ 0, p), with the appropriate casts
Proof that g(p) = H(1 ⟶ 1, p), with the appropriate casts