# Homotopic maps induce naturally isomorphic functors #

## Main definitions #

• FundamentalGroupoidFunctor.homotopicMapsNatIso H The natural isomorphism between the induced functors f : π(X) ⥤ π(Y) and g : π(X) ⥤ π(Y), given a homotopy H : f ∼ g

• FundamentalGroupoidFunctor.equivOfHomotopyEquiv hequiv The equivalence of the categories π(X) and π(Y) given a homotopy equivalence hequiv : X ≃ₕ Y between them.

## Implementation notes #

• In order to be more universe polymorphic, we define ContinuousMap.Homotopy.uliftMap which lifts a homotopy from I × X → Y to (TopCat.of ((ULift I) × X)) → Y. This is because this construction uses FundamentalGroupoidFunctor.prodToProdTop to convert between pairs of paths in I and X and the corresponding path after passing through a homotopy H. But FundamentalGroupoidFunctor.prodToProdTop requires two spaces in the same universe.

The path 0 ⟶ 1 in I

Equations
Instances For
def unitInterval.upath01 :
Path { down := 0 } { down := 1 }

The path 0 ⟶ 1 in ULift I

Equations
Instances For

The homotopy path class of 0 → 1 in ULift I

Equations
Instances For
@[reducible, inline]
abbrev ContinuousMap.Homotopy.hcast {X : TopCat} {x₀ : X} {x₁ : X} (hx : x₀ = x₁) :

Abbreviation for eqToHom that accepts points in a topological space

Equations
Instances For
@[simp]
theorem ContinuousMap.Homotopy.hcast_def {X : TopCat} {x₀ : X} {x₁ : X} (hx₀ : x₀ = x₁) :
theorem ContinuousMap.Homotopy.heq_path_of_eq_image {X₁ : TopCat} {X₂ : TopCat} {Y : TopCat} {f : C(X₁, Y)} {g : C(X₂, Y)} {x₀ : X₁} {x₁ : X₁} {x₂ : X₂} {x₃ : X₂} {p : Path x₀ x₁} {q : Path x₂ x₃} (hfg : ∀ (t : ), f (p t) = g (q t)) :
HEq (.map p) (.map q)

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

theorem ContinuousMap.Homotopy.eq_path_of_eq_image {X₁ : TopCat} {X₂ : TopCat} {Y : TopCat} {f : C(X₁, Y)} {g : C(X₂, Y)} {x₀ : X₁} {x₁ : X₁} {x₂ : X₂} {x₃ : X₂} {p : Path x₀ x₁} {q : Path x₂ x₃} (hfg : ∀ (t : ), f (p t) = g (q t)) :
.map p =

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.

def ContinuousMap.Homotopy.uliftMap {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) :
C((TopCat.of ( × X)), Y)

Interpret a homotopy H : C(I × X, Y) as a map C(ULift I × X, Y)

Equations
• H.uliftMap = { toFun := fun (x : (TopCat.of ( × X))) => H (x.1.down, x.2), continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.Homotopy.ulift_apply {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) (i : ) (x : X) :
H.uliftMap (i, x) = H (i.down, x)
@[reducible, inline]
abbrev ContinuousMap.Homotopy.prodToProdTopI {X : TopCat} {a₁ : (TopCat.of )} {a₂ : (TopCat.of )} {b₁ : X} {b₂ : X} (p₁ : ) (p₂ : ) :
.obj ({ as := a₁ }, { as := b₁ }) .obj ({ as := a₂ }, { as := b₂ })

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
• = .map (p₁, p₂)
Instances For
def ContinuousMap.Homotopy.diagonalPath {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) {x₀ : X} {x₁ : X} :

The diagonal path d of a homotopy H on a path p

Equations
• H.diagonalPath p = ( H.uliftMap).map
Instances For
def ContinuousMap.Homotopy.diagonalPath' {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) {x₀ : X} {x₁ : X} :

The diagonal path, but starting from f x₀ and going to g x₁

Equations
• H.diagonalPath' p =
Instances For
theorem ContinuousMap.Homotopy.apply_zero_path {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) {x₀ : X} {x₁ : X} :

Proof that f(p) = H(0 ⟶ 0, p), with the appropriate casts

theorem ContinuousMap.Homotopy.apply_one_path {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) {x₀ : X} {x₁ : X} :

Proof that g(p) = H(1 ⟶ 1, p), with the appropriate casts

theorem ContinuousMap.Homotopy.evalAt_eq {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) (x : X) :

Proof that H.evalAt x = H(0 ⟶ 1, x ⟶ x), with the appropriate casts

theorem ContinuousMap.Homotopy.eq_diag_path {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) {x₀ : X} {x₁ : X} :
CategoryTheory.CategoryStruct.comp (.map p) H.evalAt x₁ = H.diagonalPath' p CategoryTheory.CategoryStruct.comp H.evalAt x₀ (.map p) = H.diagonalPath' p
def FundamentalGroupoidFunctor.homotopicMapsNatIso {X : TopCat} {Y : TopCat} {f : C(X, Y)} {g : C(X, Y)} (H : f.Homotopy g) :

Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced functors f and g

Equations
• = { app := fun (x : ) => H.evalAt x.as, naturality := }
Instances For
Equations
• =

Homotopy equivalent topological spaces have equivalent fundamental groupoids.

Equations
• One or more equations did not get rendered due to their size.
Instances For