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.
Equations
- FundamentalGroupoidFunctor.homotopicMapsNatIso H = { app := fun (x : FundamentalGroupoid X) => ⟦H.evalAt x.as⟧, naturality := ⋯ }
Instances For
Homotopy equivalent topological spaces have equivalent fundamental groupoids.
Equations
- One or more equations did not get rendered due to their size.
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 I
Equations
- unitInterval.path01 = { toFun := id, continuous_toFun := unitInterval.path01._proof_2, source' := unitInterval.path01._proof_1, target' := unitInterval.path01._proof_3 }
Instances For
The path 0 ⟶ 1 in ULift I
Equations
- unitInterval.upath01 = { toFun := ULift.up, continuous_toFun := unitInterval.upath01._proof_2, source' := unitInterval.upath01._proof_1, target' := unitInterval.upath01._proof_3 }
Instances For
Abbreviation for eqToHom that accepts points in a topological space
Equations
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.
Interpret a homotopy H : C(I × X, Y) as a map C(ULift I × X, Y)
Equations
- H.uliftMap = { toFun := fun (x : ↑{ carrier := ULift.{?u.32, 0} ↑unitInterval × ↑X, str := instTopologicalSpaceProd }) => H (x.1.down, x.2), continuous_toFun := ⋯ }
Instances For
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.
Equations
- ContinuousMap.Homotopy.prodToProdTopI p₁ p₂ = (FundamentalGroupoidFunctor.prodToProdTop { carrier := ULift.{?u.60, 0} ↑unitInterval, str := ULift.topologicalSpace } X).map (p₁, p₂)
Instances For
The diagonal path d of a homotopy H on a path p
Equations
Instances For
The diagonal path, but starting from f x₀ and going to g x₁
Equations
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