feat(topology/homotopy): Homotopic maps induce naturally isomorphic functors between fundamental groupoid (#11595)

Co-authored-by: prakol16 <prakol16@users.noreply.github.com>

Author: prakol16

src/category_theory/category/Groupoid.lean

@@ -74,6 +74,9 @@ instance forget_to_Cat_faithful : faithful forget_to_Cat := { }
 which sometimes helps in applying simp lemmas -/
 lemma hom_to_functor {C D E : Groupoid.{v u}} (f : C ⟶ D) (g : D ⟶ E) : f ≫ g = f ⋙ g := rfl
 
+/-- Converts identity in the category of groupoids to the functor identity -/
+lemma id_to_functor {C : Groupoid.{v u}} : 𝟭 C = 𝟙 C := rfl
+
 section products
 
 /-- The cone for the product of a family of groupoids indexed by J is a limit cone -/

src/topology/homotopy/fundamental_groupoid.lean

@@ -330,6 +330,9 @@ localized "notation `πₓ` := fundamental_groupoid.fundamental_groupoid_functor
 localized "notation `πₘ` := fundamental_groupoid.fundamental_groupoid_functor.map"
   in fundamental_groupoid
 
+lemma map_eq {X Y : Top} {x₀ x₁ : X} (f : C(X, Y)) (p : path.homotopic.quotient x₀ x₁) :
+  (πₘ f).map p = p.map_fn f := rfl
+
 /-- Help the typechecker by converting a point in a groupoid back to a point in
 the underlying topological space. -/
 @[reducible]

src/topology/homotopy/induced_maps.lean

@@ -0,0 +1,213 @@
+/-
+Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Praneeth Kolichala
+-/
+import topology.homotopy.product
+import topology.homotopy.equiv
+import category_theory.equivalence
+
+/-!
+# Homotopic maps induce naturally isomorphic functors
+
+## 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.
+-/
+
+noncomputable theory
+
+universe u
+
+open fundamental_groupoid
+open category_theory
+open fundamental_groupoid_functor
+
+open_locale fundamental_groupoid
+open_locale unit_interval
+
+namespace unit_interval
+
+/-- The path 0 ⟶ 1 in I -/
+def path01 : path (0 : I) 1 := { to_fun := id, source' := rfl, target' := rfl }
+
+/-- The path 0 ⟶ 1 in ulift I -/
+def upath01 : path (ulift.up 0 : ulift.{u} I) (ulift.up 1) :=
+{ to_fun := ulift.up, source' := rfl, target' := rfl }
+
+local attribute [instance] path.homotopic.setoid
+/-- The homotopy path class of 0 → 1 in `ulift I` -/
+def uhpath01 : @from_top (Top.of $ ulift.{u} I) (ulift.up (0 : I)) ⟶ from_top (ulift.up 1) :=
+⟦upath01⟧
+
+end unit_interval
+
+namespace continuous_map.homotopy
+open unit_interval (uhpath01)
+
+local attribute [instance] path.homotopic.setoid
+
+section casts
+
+/-- Abbreviation for `eq_to_hom` that accepts points in a topological space -/
+abbreviation hcast {X : Top} {x₀ x₁ : X} (hx : x₀ = x₁) : from_top x₀ ⟶ from_top x₁ := eq_to_hom hx
+
+@[simp] lemma hcast_def {X : Top} {x₀ x₁ : X} (hx₀ : x₀ = x₁) : hcast hx₀ = eq_to_hom hx₀ := rfl
+
+variables {X₁ X₂ Y : Top.{u}} {f : C(X₁, Y)} {g : C(X₂, Y)}
+  {x₀ x₁ : X₁} {x₂ x₃ : X₂} {p : path x₀ x₁} {q : path x₂ x₃} (hfg : ∀ t, f (p t) = g (q t))
+
+include hfg
+
+/-- 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 -/
+lemma heq_path_of_eq_image : (πₘ f).map ⟦p⟧ == (πₘ g).map ⟦q⟧ :=
+by { simp only [map_eq, ← path.homotopic.map_lift], apply path.homotopic.hpath_hext, exact hfg, }
+
+private lemma start_path : f x₀ = g x₂ := by { convert hfg 0; simp only [path.source], }
+private lemma end_path : f x₁ = g x₃ := by { convert hfg 1; simp only [path.target], }
+
+lemma eq_path_of_eq_image :
+  (πₘ f).map ⟦p⟧ = hcast (start_path hfg) ≫ (πₘ g).map ⟦q⟧ ≫ hcast (end_path hfg).symm :=
+by { rw functor.conj_eq_to_hom_iff_heq, exact heq_path_of_eq_image hfg }
+
+end casts
+
+/- We let `X` and `Y` be spaces, and `f` and `g` be homotopic maps between them -/
+variables {X Y : Top.{u}} {f g : C(X, Y)} (H : continuous_map.homotopy f g)
+  {x₀ x₁ : X} (p : from_top x₀ ⟶ from_top x₁)
+
+/-!
+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) -/
+def ulift_map : C(Top.of (ulift.{u} I × X), Y) :=
+⟨λ x, H (x.1.down, x.2),
+  H.continuous.comp ((continuous_induced_dom.comp continuous_fst).prod_mk continuous_snd)⟩
+
+@[simp] lemma ulift_apply (i : ulift.{u} I) (x : X) : H.ulift_map (i, x) = H (i.down, x) := rfl
+
+/-- 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. -/
+abbreviation prod_to_prod_Top_I {a₁ a₂ : Top.of (ulift I)} {b₁ b₂ : X}
+  (p₁ : from_top a₁ ⟶ from_top a₂) (p₂ : from_top b₁ ⟶ from_top b₂) :=
+@category_theory.functor.map _ _ _ _ (prod_to_prod_Top (Top.of $ ulift I) X)
+  (a₁, b₁) (a₂, b₂) (p₁, p₂)
+
+/-- The diagonal path `d` of a homotopy `H` on a path `p` -/
+def diagonal_path : from_top (H (0, x₀)) ⟶ from_top (H (1, x₁)) :=
+(πₘ H.ulift_map).map (prod_to_prod_Top_I uhpath01 p)
+
+/-- The diagonal path, but starting from `f x₀` and going to `g x₁` -/
+def diagonal_path' : from_top (f x₀) ⟶ from_top (g x₁) :=
+hcast (H.apply_zero x₀).symm ≫ (H.diagonal_path p) ≫ hcast (H.apply_one x₁)
+
+/-- Proof that `f(p) = H(0 ⟶ 0, p)`, with the appropriate casts -/
+lemma apply_zero_path : (πₘ f).map p = hcast (H.apply_zero x₀).symm ≫
+(πₘ H.ulift_map).map (prod_to_prod_Top_I (𝟙 (ulift.up 0)) p) ≫
+hcast (H.apply_zero x₁) :=
+begin
+  apply quotient.induction_on p,
+  intro p',
+  apply @eq_path_of_eq_image _ _ _ _ H.ulift_map _ _ _ _ _ ((path.refl (ulift.up _)).prod p'),
+  simp,
+end
+
+/-- Proof that `g(p) = H(1 ⟶ 1, p)`, with the appropriate casts -/
+lemma apply_one_path : (πₘ g).map p = hcast (H.apply_one x₀).symm ≫
+((πₘ H.ulift_map).map (prod_to_prod_Top_I (𝟙 (ulift.up 1)) p)) ≫
+hcast (H.apply_one x₁) :=
+begin
+  apply quotient.induction_on p,
+  intro p',
+  apply @eq_path_of_eq_image _ _ _ _ H.ulift_map _ _ _ _ _ ((path.refl (ulift.up _)).prod p'),
+  simp,
+end
+
+/-- Proof that `H.eval_at x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts -/
+lemma eval_at_eq (x : X) : ⟦H.eval_at x⟧ =
+  hcast (H.apply_zero x).symm ≫
+(πₘ H.ulift_map).map (prod_to_prod_Top_I uhpath01 (𝟙 x)) ≫
+hcast (H.apply_one x).symm.symm :=
+begin
+  dunfold prod_to_prod_Top_I uhpath01 hcast,
+  refine (@functor.conj_eq_to_hom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _ _).mpr _,
+  simp only [id_eq_path_refl, prod_to_prod_Top_map, path.homotopic.prod_lift, map_eq,
+    ← path.homotopic.map_lift],
+  apply path.homotopic.hpath_hext, intro, refl,
+end
+
+/- Finally, we show `d = f(p) ≫ H₁ = H₀ ≫ g(p)` -/
+lemma eq_diag_path :
+  (πₘ f).map p ≫ ⟦H.eval_at x₁⟧ = H.diagonal_path' p ∧
+  (⟦H.eval_at x₀⟧ ≫ (πₘ g).map p : from_top (f x₀) ⟶ from_top (g x₁)) = H.diagonal_path' p :=
+begin
+  rw [H.apply_zero_path, H.apply_one_path, H.eval_at_eq, H.eval_at_eq],
+  dunfold prod_to_prod_Top_I,
+  split; { slice_lhs 2 5 { simp [← category_theory.functor.map_comp], }, refl, },
+end
+
+end continuous_map.homotopy
+
+namespace fundamental_groupoid_functor
+open category_theory
+open_locale fundamental_groupoid
+local attribute [instance] path.homotopic.setoid
+
+variables {X Y : Top.{u}} {f g : C(X, Y)} (H : continuous_map.homotopy f g)
+
+/-- Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
+functors `f` and `g` -/
+def homotopic_maps_nat_iso : πₘ f ⟶ πₘ g :=
+{ app := λ x, ⟦H.eval_at x⟧,
+  naturality' := λ x y p, by rw [(H.eq_diag_path p).1, (H.eq_diag_path p).2] }
+
+instance : is_iso (homotopic_maps_nat_iso H) := by apply nat_iso.is_iso_of_is_iso_app
+
+open_locale continuous_map
+
+/-- Homotopy equivalent topological spaces have equivalent fundamental groupoids. -/
+def equiv_of_homotopy_equiv (hequiv : X ≃ₕ Y) : πₓ X ≌ πₓ Y :=
+begin
+  apply equivalence.mk
+    (πₘ hequiv.to_fun : πₓ X ⥤ πₓ Y)
+    (πₘ hequiv.inv_fun : πₓ Y ⥤ πₓ X);
+  simp only [Groupoid.hom_to_functor, Groupoid.id_to_functor],
+  { convert (as_iso (homotopic_maps_nat_iso hequiv.left_inv.some)).symm,
+    exacts [((π).map_id X).symm, ((π).map_comp _ _).symm] },
+  { convert as_iso (homotopic_maps_nat_iso hequiv.right_inv.some),
+    exacts [((π).map_comp _ _).symm, ((π).map_id Y).symm] },
+end
+
+end fundamental_groupoid_functor

src/topology/homotopy/path.lean

@@ -33,7 +33,7 @@ In this file, we define a `homotopy` between two `path`s. In addition, we define
 universes u v
 
 variables {X : Type u} {Y : Type v} [topological_space X] [topological_space Y]
-variables {x₀ x₁ x₂ : X}
+variables {x₀ x₁ x₂ x₃ : X}
 
 noncomputable theory
 
@@ -309,6 +309,29 @@ quotient.map (λ (q : path x₀ x₁), q.map f.continuous) (λ p₀ p₁ h, path
 lemma map_lift (P₀ : path x₀ x₁) (f : C(X, Y)) :
   ⟦P₀.map f.continuous⟧ = quotient.map_fn ⟦P₀⟧ f := rfl
 
+lemma hpath_hext {p₁ : path x₀ x₁} {p₂ : path x₂ x₃} (hp : ∀ t, p₁ t = p₂ t) : ⟦p₁⟧ == ⟦p₂⟧ :=
+begin
+  have : x₀ = x₂ := by { convert hp 0; simp, }, subst this,
+  have : x₁ = x₃ := by { convert hp 1; simp, }, subst this,
+  rw heq_iff_eq, congr, ext t, exact hp t,
+end
+
+
 end homotopic
 
 end path
+
+
+namespace continuous_map.homotopy
+
+/--
+Given a homotopy H: f ∼ g, get the path traced by the point `x` as it moves from
+`f x` to `g x`
+-/
+def eval_at {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] {f g : C(X, Y)}
+  (H : continuous_map.homotopy f g) (x : X) : path (f x) (g x) :=
+{ to_fun := λ t, H (t, x),
+  source' := H.apply_zero x,
+  target' := H.apply_one x, }
+
+end continuous_map.homotopy

src/topology/homotopy/product.lean

@@ -387,7 +387,7 @@ def proj_right : πₓ (Top.of (A × B)) ⥤ πₓ B := πₘ ⟨_, continuous_s
 The map taking the product of two fundamental groupoids to the fundamental groupoid of the product
 of the two topological spaces. This is in fact an isomorphism (see `prod_iso`).
 -/
-@[simps]
+@[simps obj]
 def prod_to_prod_Top : (πₓ A) × (πₓ B) ⥤ πₓ (Top.of (A × B)) :=
 { obj := λ g, g,
   map := λ x y p, match x, y, p with
@@ -404,6 +404,11 @@ def prod_to_prod_Top : (πₓ A) × (πₓ B) ⥤ πₓ (Top.of (A × B)) :=
     (path.homotopic.comp_prod_eq_prod_comp f₀ f₁ g₀ g₁).symm
   end }
 
+lemma prod_to_prod_Top_map {x₀ x₁ : πₓ A} {y₀ y₁ : πₓ B}
+  (p₀ : x₀ ⟶ x₁) (p₁ : y₀ ⟶ y₁) :
+  @category_theory.functor.map _ _ _ _
+  (prod_to_prod_Top A B) (x₀, y₀) (x₁, y₁) (p₀, p₁) = path.homotopic.prod p₀ p₁ := rfl
+
 /--
 Shows `prod_to_prod_Top` is an isomorphism, whose inverse is precisely the product
 of the induced left and right projections.