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
The homotopy path class of 0 → 1 in ULift I
Equations
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.42, 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
- ContinuousMap.Homotopy.prodToProdTopI p₁ p₂ = (FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{?u.90, 0} ↑unitInterval)) X).map (p₁, p₂)
Instances For
The diagonal path d of a homotopy H on a path p
Equations
- H.diagonalPath p = (FundamentalGroupoid.fundamentalGroupoidFunctor.map H.uliftMap).map (ContinuousMap.Homotopy.prodToProdTopI unitInterval.uhpath01 p)
Instances For
The diagonal path, but starting from f x₀ and going to g x₁
Equations
- H.diagonalPath' p = CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯) (CategoryTheory.CategoryStruct.comp (H.diagonalPath p) (ContinuousMap.Homotopy.hcast ⋯))
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
Proof that H.evalAt 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
functors f and g
Equations
- FundamentalGroupoidFunctor.homotopicMapsNatIso H = { app := fun (x : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj 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.