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.

source

def unitInterval.path01 :

Path 0 1

The path 0 ⟶ 1 in I

Equations

unitInterval.path01 = { toContinuousMap := ContinuousMap.mk id, source' := unitInterval.path01.proof_2, target' := unitInterval.path01.proof_3 }

Instances For

source

def unitInterval.upath01 :

Path { down := 0 } { down := 1 }

The path 0 ⟶ 1 in ULift I

Equations

unitInterval.upath01 = { toContinuousMap := ContinuousMap.mk ULift.up, source' := unitInterval.upath01.proof_2, target' := unitInterval.upath01.proof_3 }

Instances For

source

def unitInterval.uhpath01 :

FundamentalGroupoid.fromTop { down := 0 } ⟶ FundamentalGroupoid.fromTop { down := 1 }

The homotopy path class of 0 → 1 in ULift I

Equations

unitInterval.uhpath01 = ⟦unitInterval.upath01⟧

Instances For

source

@[inline, reducible]

abbrev ContinuousMap.Homotopy.hcast {X : TopCat} {x₀ : ↑X} {x₁ : ↑X} (hx : x₀ = x₁) :

FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁

Abbreviation for eqToHom that accepts points in a topological space

Equations

ContinuousMap.Homotopy.hcast hx = CategoryTheory.eqToHom (_ : FundamentalGroupoid.fromTop x₀ = FundamentalGroupoid.fromTop x₁)

Instances For

source

@[simp]

theorem ContinuousMap.Homotopy.hcast_def {X : TopCat} {x₀ : ↑X} {x₁ : ↑X} (hx₀ : x₀ = x₁) :

ContinuousMap.Homotopy.hcast hx₀ = CategoryTheory.eqToHom (_ : { as := x₀ } = { as := x₁ })

source

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 : ↑unitInterval), f (p t) = g (q t)) :

HEq ((FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.map f).toPrefunctor.map ⟦p⟧) ((FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.map g).toPrefunctor.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

source

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 : ↑unitInterval), f (p t) = g (q t)) :

(FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.map f).toPrefunctor.map ⟦p⟧ = CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast (_ : f x₀ = g x₂)) (CategoryTheory.CategoryStruct.comp ((FundamentalGroupoid.fundamentalGroupoidFunctor.toPrefunctor.map g).toPrefunctor.map ⟦q⟧) (ContinuousMap.Homotopy.hcast (_ : g x₃ = f x₁)))

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.

source

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

C(↑(TopCat.of (ULift.{u, 0} ↑unitInterval × ↑X)), ↑Y)

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

Equations

ContinuousMap.Homotopy.uliftMap H = ContinuousMap.mk fun (x : ↑(TopCat.of (ULift.{u, 0} ↑unitInterval × ↑X))) => H (x.1.down, x.2)

Instances For

source

@[simp]

theorem ContinuousMap.Homotopy.ulift_apply {X : TopCat} {Y : TopCat} {f : C(↑X, ↑Y)} {g : C(↑X, ↑Y)} (H : ContinuousMap.Homotopy f g) (i : ULift.{u, 0} ↑unitInterval) (x : ↑X) :

(ContinuousMap.Homotopy.uliftMap H) (i, x) = H (i.down, x)

source

@[inline, reducible]

abbrev ContinuousMap.Homotopy.prodToProdTopI {X : TopCat} {a₁ : ↑(TopCat.of (ULift.{u, 0} ↑unitInterval))} {a₂ : ↑(TopCat.of (ULift.{u, 0} ↑unitInterval))} {b₁ : ↑X} {b₂ : ↑X} (p₁ : FundamentalGroupoid.fromTop a₁ ⟶ FundamentalGroupoid.fromTop a₂) (p₂ : FundamentalGroupoid.fromTop b₁ ⟶ FundamentalGroupoid.fromTop b₂) :

(FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).toPrefunctor.obj ({ as := a₁ }, { as := b₁ }) ⟶ (FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).toPrefunctor.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