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.
Implementation notes #
- In order to be more universe polymorphic, we define
ContinuousMap.Homotopy.uliftMapwhich lifts a homotopy fromI × X → Yto(TopCat.of ((ULift I) × X)) → Y. This is because this construction usesFundamentalGroupoidFunctor.prodToProdTopto convert between pairs of paths in I and X and the corresponding path after passing through a homotopyH. ButFundamentalGroupoidFunctor.prodToProdToprequires two spaces in the same universe.
The path 0 ⟶ 1 in I
Equations
- unitInterval.path01 = { toFun := id, continuous_toFun := unitInterval.path01.proof_1, source' := unitInterval.path01.proof_2, 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_1, source' := unitInterval.upath01.proof_2, 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 : ↑(TopCat.of (ULift.{?u.47, 0} ↑unitInterval × ↑X))) => 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
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
Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
functors f and g
Equations
- FundamentalGroupoidFunctor.homotopicMapsNatIso H = { app := fun (x : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ↑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.