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 HThe 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 hequivThe equivalence of the categories
π(Y)given a homotopy equivalence
hequiv : X ≃ₕ Ybetween them.
Implementation notes #
- In order to be more universe polymorphic, we define
continuous_map.homotopy.ulift_mapwhich lifts a homotopy from
I × X → Yto
(Top.of ((ulift I) × X)) → Y. This is because this construction uses
fundamental_groupoid_functor.prod_to_prod_Topto convert between pairs of paths in I and X and the corresponding path after passing through a homotopy
fundamental_groupoid_functor.prod_to_prod_Toprequires two spaces in the same universe.
The path 0 ⟶ 1 in ulift I
f(p(t) = g(q(t)) for two paths
q, then the induced path homotopy classes
g(p) are the same as well, despite having a priori different types
These definitions set up the following diagram, for each path
f(p) *--------* | \ | H₀ | \ d | H₁ | \ | *--------* g(p)
H₀ = H.eval_at x₀ is the path from
and similarly for
f(p) denotes the
path in Y that the induced map
p, and similarly for
d, the diagonal path, is H(0 ⟶ 1, p), the result of the induced
path.homotopic.prod (0 ⟶ 1) p, where
(0 ⟶ 1) denotes the path from
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.
Interpret a homotopy `H : C(I × X, Y) as a map C(ulift I × X, Y)
An abbreviation for
prod_to_prod_Top, with some types already in place to help the
typechecker. In particular, the first path should be on the ulifted unit interval.
The diagonal path
d of a homotopy
H on a path
The diagonal path, but starting from
f x₀ and going to
f(p) = H(0 ⟶ 0, p), with the appropriate casts
g(p) = H(1 ⟶ 1, p), with the appropriate casts
H.eval_at x = H(0 ⟶ 1, x ⟶ x), with the appropriate casts
Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
Homotopy equivalent topological spaces have equivalent fundamental groupoids.
- fundamental_groupoid_functor.equiv_of_homotopy_equiv hequiv = category_theory.equivalence.mk (fundamental_groupoid.fundamental_groupoid_functor.map hequiv.to_fun) (fundamental_groupoid.fundamental_groupoid_functor.map hequiv.inv_fun) (_.mpr (_.mpr (category_theory.as_iso (fundamental_groupoid_functor.homotopic_maps_nat_iso (nonempty.some _))).symm)) (_.mpr (_.mpr (category_theory.as_iso (fundamental_groupoid_functor.homotopic_maps_nat_iso (nonempty.some _)))))