# mathlib3documentation

algebraic_topology.fundamental_groupoid.induced_maps

# Homotopic maps induce naturally isomorphic functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

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

• fundamental_groupoid_functor.equiv_of_homotopy_equiv 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 continuous_map.homotopy.ulift_map which lifts a homotopy from I × X → Y to (Top.of ((ulift I) × X)) → Y. This is because this construction uses fundamental_groupoid_functor.prod_to_prod_Top to convert between pairs of paths in I and X and the corresponding path after passing through a homotopy H. But fundamental_groupoid_functor.prod_to_prod_Top requires two spaces in the same universe.

The path 0 ⟶ 1 in I

Equations
def unit_interval.upath01  :
path {down := 0} {down := 1}

The path 0 ⟶ 1 in ulift I

Equations

The homotopy path class of 0 → 1 in ulift I

Equations
@[reducible]
noncomputable def continuous_map.homotopy.hcast {X : Top} {x₀ x₁ : X} (hx : x₀ = x₁) :

Abbreviation for eq_to_hom that accepts points in a topological space

@[simp]
theorem continuous_map.homotopy.hcast_def {X : Top} {x₀ x₁ : X} (hx₀ : x₀ = x₁) :
theorem continuous_map.homotopy.heq_path_of_eq_image {X₁ X₂ Y : Top} {f : C(X₁, Y)} {g : C(X₂, Y)} {x₀ x₁ : X₁} {x₂ x₃ : X₂} {p : path x₀ x₁} {q : path x₂ x₃} (hfg : (t : unit_interval), f (p t) = g (q t)) :

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 continuous_map.homotopy.eq_path_of_eq_image {X₁ X₂ Y : Top} {f : C(X₁, Y)} {g : C(X₂, Y)} {x₀ x₁ : X₁} {x₂ x₃ : X₂} {p : path x₀ x₁} {q : path x₂ x₃} (hfg : (t : unit_interval), f (p t) = g (q t)) :

These definitions set up the following diagram, for each path p:

        f(p)
*--------*
| \      |
H₀  |   \ d  |  H₁
|     \  |
*--------*
g(p)


Here, H₀ = H.eval_at 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
@[simp]
theorem continuous_map.homotopy.ulift_apply {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) (i : ulift unit_interval) (x : X) :
(H.ulift_map) (i, x) = H (i.down, x)
@[reducible]
noncomputable def continuous_map.homotopy.prod_to_prod_Top_I {X : Top} {a₁ a₂ : } {b₁ b₂ : X}  :
(a₁, b₁) (a₂, b₂)

An abbreviation for prod_to_prod_Top, with some types already in place to help the typechecker. In particular, the first path should be on the ulifted unit interval.

noncomputable def continuous_map.homotopy.diagonal_path {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) {x₀ x₁ : X}  :

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

Equations
noncomputable def continuous_map.homotopy.diagonal_path' {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) {x₀ x₁ : X}  :

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

Equations
theorem continuous_map.homotopy.apply_zero_path {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) {x₀ x₁ : X}  :

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

theorem continuous_map.homotopy.apply_one_path {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) {x₀ x₁ : X}  :

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

theorem continuous_map.homotopy.eval_at_eq {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) (x : X) :

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

theorem continuous_map.homotopy.eq_diag_path {X Y : Top} {f g : C(X, Y)} (H : f.homotopy g) {x₀ x₁ : X}  :
noncomputable def fundamental_groupoid_functor.homotopic_maps_nat_iso {X Y : Top} {f 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
Instances for fundamental_groupoid_functor.homotopic_maps_nat_iso`
@[protected, instance]
noncomputable def fundamental_groupoid_functor.equiv_of_homotopy_equiv {X Y : Top} (hequiv : Y) :

Homotopy equivalent topological spaces have equivalent fundamental groupoids.

Equations