|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Praneeth Kolichala. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Praneeth Kolichala |
| 5 | +-/ |
| 6 | + |
| 7 | +import category_theory.groupoid |
| 8 | +import algebraic_topology.fundamental_groupoid.basic |
| 9 | +import topology.category.Top.limits |
| 10 | +import topology.homotopy.product |
| 11 | +import category_theory.limits.preserves.shapes.products |
| 12 | + |
| 13 | +/-! |
| 14 | +# Fundamental groupoid preserves products |
| 15 | +In this file, we give the following definitions/theorems: |
| 16 | +
|
| 17 | + - `fundamental_groupoid_functor.pi_iso` An isomorphism between Π i, (π Xᵢ) and π (Πi, Xᵢ), whose |
| 18 | + inverse is precisely the product of the maps π (Π i, Xᵢ) → π (Xᵢ), each induced by |
| 19 | + the projection in `Top` Π i, Xᵢ → Xᵢ. |
| 20 | +
|
| 21 | + - `fundamental_groupoid_functor.prod_iso` An isomorphism between πX × πY and π (X × Y), whose |
| 22 | + inverse is precisely the product of the maps π (X × Y) → πX and π (X × Y) → Y, each induced by |
| 23 | + the projections X × Y → X and X × Y → Y |
| 24 | +
|
| 25 | + - `fundamental_groupoid_functor.preserves_product` A proof that the fundamental groupoid functor |
| 26 | + preserves all products. |
| 27 | +-/ |
| 28 | + |
| 29 | +noncomputable theory |
| 30 | + |
| 31 | +namespace fundamental_groupoid_functor |
| 32 | + |
| 33 | +open_locale fundamental_groupoid |
| 34 | + |
| 35 | +universes u |
| 36 | + |
| 37 | +section pi |
| 38 | + |
| 39 | +variables {I : Type u} (X : I → Top.{u}) |
| 40 | + |
| 41 | +/-- |
| 42 | +The projection map Π i, X i → X i induces a map π(Π i, X i) ⟶ π(X i). |
| 43 | +-/ |
| 44 | +def proj (i : I) : πₓ (Top.of (Π i, X i)) ⥤ πₓ (X i) := πₘ ⟨_, continuous_apply i⟩ |
| 45 | + |
| 46 | +/-- The projection map is precisely path.homotopic.proj interpreted as a functor -/ |
| 47 | +@[simp] lemma proj_map (i : I) (x₀ x₁ : πₓ (Top.of (Π i, X i))) (p : x₀ ⟶ x₁) : |
| 48 | + (proj X i).map p = (@path.homotopic.proj _ _ _ _ _ i p) := rfl |
| 49 | + |
| 50 | +/-- |
| 51 | +The map taking the pi product of a family of fundamental groupoids to the fundamental |
| 52 | +groupoid of the pi product. This is actually an isomorphism (see `pi_iso`) |
| 53 | +-/ |
| 54 | +@[simps] |
| 55 | +def pi_to_pi_Top : (Π i, πₓ (X i)) ⥤ πₓ (Top.of (Π i, X i)) := |
| 56 | +{ obj := λ g, g, |
| 57 | + map := λ v₁ v₂ p, path.homotopic.pi p, |
| 58 | + map_id' := |
| 59 | + begin |
| 60 | + intro x, |
| 61 | + change path.homotopic.pi (λ i, 𝟙 (x i)) = _, |
| 62 | + simp only [fundamental_groupoid.id_eq_path_refl, path.homotopic.pi_lift], |
| 63 | + refl, |
| 64 | + end, |
| 65 | + map_comp' := λ x y z f g, (path.homotopic.comp_pi_eq_pi_comp f g).symm, } |
| 66 | + |
| 67 | +/-- |
| 68 | +Shows `pi_to_pi_Top` is an isomorphism, whose inverse is precisely the pi product |
| 69 | +of the induced projections. This shows that `fundamental_groupoid_functor` preserves products. |
| 70 | +-/ |
| 71 | +@[simps] |
| 72 | +def pi_iso : category_theory.Groupoid.of (Π i : I, πₓ (X i)) ≅ πₓ (Top.of (Π i, X i)) := |
| 73 | +{ hom := pi_to_pi_Top X, |
| 74 | + inv := category_theory.functor.pi' (proj X), |
| 75 | + hom_inv_id' := |
| 76 | + begin |
| 77 | + change pi_to_pi_Top X ⋙ (category_theory.functor.pi' (proj X)) = 𝟭 _, |
| 78 | + apply category_theory.functor.ext; intros, |
| 79 | + { ext, simp, }, { refl, }, |
| 80 | + end, |
| 81 | + inv_hom_id' := |
| 82 | + begin |
| 83 | + change (category_theory.functor.pi' (proj X)) ⋙ pi_to_pi_Top X = 𝟭 _, |
| 84 | + apply category_theory.functor.ext; intros, |
| 85 | + { suffices : path.homotopic.pi ((category_theory.functor.pi' (proj X)).map f) = f, { simpa, }, |
| 86 | + change (category_theory.functor.pi' (proj X)).map f |
| 87 | + with λ i, (category_theory.functor.pi' (proj X)).map f i, |
| 88 | + simp, }, { refl, } |
| 89 | + end } |
| 90 | + |
| 91 | +section preserves |
| 92 | +open category_theory |
| 93 | + |
| 94 | +/-- Equivalence between the categories of cones over the objects `π Xᵢ` written in two ways -/ |
| 95 | +def cone_discrete_comp : limits.cone (discrete.functor X ⋙ π) ≌ |
| 96 | + limits.cone (discrete.functor (λ i, πₓ (X i))) := |
| 97 | +limits.cones.postcompose_equivalence (discrete.comp_nat_iso_discrete X π) |
| 98 | + |
| 99 | +lemma cone_discrete_comp_obj_map_cone : |
| 100 | + (cone_discrete_comp X).functor.obj ((π).map_cone (Top.pi_fan X)) |
| 101 | + = limits.fan.mk (πₓ (Top.of (Π i, X i))) (proj X) := rfl |
| 102 | + |
| 103 | +/-- This is `pi_iso.inv` as a cone morphism (in fact, isomorphism) -/ |
| 104 | +def pi_Top_to_pi_cone : (limits.fan.mk (πₓ (Top.of (Π i, X i))) (proj X)) ⟶ |
| 105 | + Groupoid.pi_limit_fan (λ i : I, (πₓ (X i))) := { hom := category_theory.functor.pi' (proj X) } |
| 106 | + |
| 107 | +instance : is_iso (pi_Top_to_pi_cone X) := |
| 108 | +begin |
| 109 | + haveI : is_iso (pi_Top_to_pi_cone X).hom := (infer_instance : is_iso (pi_iso X).inv), |
| 110 | + exact limits.cones.cone_iso_of_hom_iso (pi_Top_to_pi_cone X), |
| 111 | +end |
| 112 | + |
| 113 | +/-- The fundamental groupoid functor preserves products -/ |
| 114 | +def preserves_product : limits.preserves_limit (discrete.functor X) π := |
| 115 | +begin |
| 116 | + apply limits.preserves_limit_of_preserves_limit_cone (Top.pi_fan_is_limit X), |
| 117 | + apply (limits.is_limit.of_cone_equiv (cone_discrete_comp X)).to_fun, |
| 118 | + simp only [cone_discrete_comp_obj_map_cone], |
| 119 | + apply limits.is_limit.of_iso_limit _ (as_iso (pi_Top_to_pi_cone X)).symm, |
| 120 | + exact (Groupoid.pi_limit_cone _).is_limit, |
| 121 | +end |
| 122 | + |
| 123 | +end preserves |
| 124 | + |
| 125 | +end pi |
| 126 | + |
| 127 | +section prod |
| 128 | + |
| 129 | +variables (A B : Top.{u}) |
| 130 | + |
| 131 | +/-- The induced map of the left projection map X × Y → X -/ |
| 132 | +def proj_left : πₓ (Top.of (A × B)) ⥤ πₓ A := πₘ ⟨_, continuous_fst⟩ |
| 133 | + |
| 134 | +/-- The induced map of the right projection map X × Y → Y -/ |
| 135 | +def proj_right : πₓ (Top.of (A × B)) ⥤ πₓ B := πₘ ⟨_, continuous_snd⟩ |
| 136 | + |
| 137 | +@[simp] lemma proj_left_map (x₀ x₁ : πₓ (Top.of (A × B))) (p : x₀ ⟶ x₁) : |
| 138 | + (proj_left A B).map p = path.homotopic.proj_left p := rfl |
| 139 | + |
| 140 | +@[simp] lemma proj_right_map (x₀ x₁ : πₓ (Top.of (A × B))) (p : x₀ ⟶ x₁) : |
| 141 | + (proj_right A B).map p = path.homotopic.proj_right p := rfl |
| 142 | + |
| 143 | + |
| 144 | +/-- |
| 145 | +The map taking the product of two fundamental groupoids to the fundamental groupoid of the product |
| 146 | +of the two topological spaces. This is in fact an isomorphism (see `prod_iso`). |
| 147 | +-/ |
| 148 | +@[simps obj] |
| 149 | +def prod_to_prod_Top : (πₓ A) × (πₓ B) ⥤ πₓ (Top.of (A × B)) := |
| 150 | +{ obj := λ g, g, |
| 151 | + map := λ x y p, match x, y, p with |
| 152 | + | (x₀, x₁), (y₀, y₁), (p₀, p₁) := path.homotopic.prod p₀ p₁ |
| 153 | + end, |
| 154 | + map_id' := |
| 155 | + begin |
| 156 | + rintro ⟨x₀, x₁⟩, |
| 157 | + simp only [category_theory.prod_id, fundamental_groupoid.id_eq_path_refl], |
| 158 | + unfold_aux, rw path.homotopic.prod_lift, refl, |
| 159 | + end, |
| 160 | + map_comp' := λ x y z f g, match x, y, z, f, g with |
| 161 | + | (x₀, x₁), (y₀, y₁), (z₀, z₁), (f₀, f₁), (g₀, g₁) := |
| 162 | + (path.homotopic.comp_prod_eq_prod_comp f₀ f₁ g₀ g₁).symm |
| 163 | + end } |
| 164 | + |
| 165 | +lemma prod_to_prod_Top_map {x₀ x₁ : πₓ A} {y₀ y₁ : πₓ B} |
| 166 | + (p₀ : x₀ ⟶ x₁) (p₁ : y₀ ⟶ y₁) : |
| 167 | + @category_theory.functor.map _ _ _ _ |
| 168 | + (prod_to_prod_Top A B) (x₀, y₀) (x₁, y₁) (p₀, p₁) = path.homotopic.prod p₀ p₁ := rfl |
| 169 | + |
| 170 | +/-- |
| 171 | +Shows `prod_to_prod_Top` is an isomorphism, whose inverse is precisely the product |
| 172 | +of the induced left and right projections. |
| 173 | +-/ |
| 174 | +@[simps] |
| 175 | +def prod_iso : category_theory.Groupoid.of ((πₓ A) × (πₓ B)) ≅ (πₓ (Top.of (A × B))) := |
| 176 | +{ hom := prod_to_prod_Top A B, |
| 177 | + inv := (proj_left A B).prod' (proj_right A B), |
| 178 | + hom_inv_id' := |
| 179 | + begin |
| 180 | + change prod_to_prod_Top A B ⋙ ((proj_left A B).prod' (proj_right A B)) = 𝟭 _, |
| 181 | + apply category_theory.functor.hext, { intros, ext; simp; refl, }, |
| 182 | + rintros ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩, |
| 183 | + have := and.intro (path.homotopic.proj_left_prod f₀ f₁) (path.homotopic.proj_right_prod f₀ f₁), |
| 184 | + simpa, |
| 185 | + end, |
| 186 | + inv_hom_id' := |
| 187 | + begin |
| 188 | + change ((proj_left A B).prod' (proj_right A B)) ⋙ prod_to_prod_Top A B = 𝟭 _, |
| 189 | + apply category_theory.functor.hext, { intros, ext; simp; refl, }, |
| 190 | + rintros ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f, |
| 191 | + have := path.homotopic.prod_proj_left_proj_right f, |
| 192 | + simpa, |
| 193 | + end } |
| 194 | + |
| 195 | +end prod |
| 196 | + |
| 197 | +end fundamental_groupoid_functor |
0 commit comments