|
| 1 | +/- |
| 2 | +Copyright (c) 2020 Scott Morrison. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Simon Hudon, Scott Morrison |
| 5 | +-/ |
| 6 | +import category_theory.natural_isomorphism |
| 7 | +import category_theory.eq_to_hom |
| 8 | + |
| 9 | +/-! |
| 10 | +# Categories of indexed families of objects. |
| 11 | +
|
| 12 | +We define the pointwise category structure on indexed families of objects in a category |
| 13 | +(and also the dependent generalization). |
| 14 | +
|
| 15 | +-/ |
| 16 | + |
| 17 | +namespace category_theory |
| 18 | + |
| 19 | +universes w₀ w₁ w₂ v₁ v₂ u₁ u₂ |
| 20 | + |
| 21 | +variables {I : Type w₀} (C : I → Type u₁) [∀ i, category.{v₁} (C i)] |
| 22 | + |
| 23 | +/-- |
| 24 | +`pi C` gives the cartesian product of an indexed family of categories. |
| 25 | +-/ |
| 26 | +instance pi : category.{max w₀ v₁} (Π i, C i) := |
| 27 | +{ hom := λ X Y, Π i, X i ⟶ Y i, |
| 28 | + id := λ X i, 𝟙 (X i), |
| 29 | + comp := λ X Y Z f g i, f i ≫ g i } |
| 30 | + |
| 31 | +namespace pi |
| 32 | + |
| 33 | +@[simp] lemma id_apply (X : Π i, C i) (i) : (𝟙 X : Π i, X i ⟶ X i) i = 𝟙 (X i) := rfl |
| 34 | +@[simp] lemma comp_apply {X Y Z : Π i, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (i) : |
| 35 | + (f ≫ g : Π i, X i ⟶ Z i) i = f i ≫ g i := rfl |
| 36 | + |
| 37 | +/-- |
| 38 | +The evaluation functor at `i : I`, sending an `I`-indexed family of objects to the object over `i`. |
| 39 | +-/ |
| 40 | +@[simps] |
| 41 | +def eval (i : I) : (Π i, C i) ⥤ C i := |
| 42 | +{ obj := λ f, f i, |
| 43 | + map := λ f g α, α i, } |
| 44 | + |
| 45 | +section |
| 46 | +variables {J : Type w₁} |
| 47 | + |
| 48 | +/-- |
| 49 | +Pull back an `I`-indexed family of objects to an `J`-indexed family, along a function `J → I`. |
| 50 | +-/ |
| 51 | +@[simps] |
| 52 | +def comap (h : J → I) : (Π i, C i) ⥤ (Π j, C (h j)) := |
| 53 | +{ obj := λ f i, f (h i), |
| 54 | + map := λ f g α i, α (h i), } |
| 55 | + |
| 56 | +variables (I) |
| 57 | +/-- |
| 58 | +The natural isomorphism between |
| 59 | +pulling back a grading along the identity function, |
| 60 | +and the identity functor. -/ |
| 61 | +@[simps] |
| 62 | +def comap_id : comap C (id : I → I) ≅ 𝟭 (Π i, C i) := |
| 63 | +{ hom := { app := λ X, 𝟙 X }, |
| 64 | + inv := { app := λ X, 𝟙 X } }. |
| 65 | + |
| 66 | +variables {I} |
| 67 | +variables {K : Type w₂} |
| 68 | + |
| 69 | +/-- |
| 70 | +The natural isomorphism comparing between |
| 71 | +pulling back along two successive functions, and |
| 72 | +pulling back along their composition |
| 73 | +-/ |
| 74 | +@[simps] |
| 75 | +def comap_comp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) := |
| 76 | +{ hom := { app := λ X b, 𝟙 (X (g (f b))) }, |
| 77 | + inv := { app := λ X b, 𝟙 (X (g (f b))) } } |
| 78 | + |
| 79 | +/-- The natural isomorphism between pulling back then evaluating, and just evaluating. -/ |
| 80 | +@[simps {rhs_md := semireducible}] |
| 81 | +def comap_eval_iso_eval (h : J → I) (j : J) : comap C h ⋙ eval (C ∘ h) j ≅ eval C (h j) := |
| 82 | +nat_iso.of_components (λ f, iso.refl _) (by tidy) |
| 83 | + |
| 84 | +end |
| 85 | + |
| 86 | +section |
| 87 | +variables {J : Type w₀} {D : J → Type u₁} [∀ j, category.{v₁} (D j)] |
| 88 | + |
| 89 | +instance sum_elim_category : Π (s : I ⊕ J), category.{v₁} (sum.elim C D s) |
| 90 | +| (sum.inl i) := by { dsimp, apply_instance, } |
| 91 | +| (sum.inr j) := by { dsimp, apply_instance, } |
| 92 | + |
| 93 | +/-- |
| 94 | +The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects |
| 95 | +to obtain an `I ⊕ J`-indexed family of objects. |
| 96 | +-/ |
| 97 | +@[simps] |
| 98 | +def sum : (Π i, C i) ⥤ (Π j, D j) ⥤ (Π s : I ⊕ J, sum.elim C D s) := |
| 99 | +{ obj := λ f, |
| 100 | + { obj := λ g s, sum.rec f g s, |
| 101 | + map := λ g g' α s, sum.rec (λ i, 𝟙 (f i)) α s }, |
| 102 | + map := λ f f' α, |
| 103 | + { app := λ g s, sum.rec α (λ j, 𝟙 (g j)) s, }} |
| 104 | + |
| 105 | +end |
| 106 | + |
| 107 | +end pi |
| 108 | + |
| 109 | +namespace functor |
| 110 | + |
| 111 | +variables {C} |
| 112 | +variables {D : I → Type u₁} [∀ i, category.{v₁} (D i)] |
| 113 | + |
| 114 | +/-- |
| 115 | +Assemble an `I`-indexed family of functors into a functor between the pi types. |
| 116 | +-/ |
| 117 | +@[simps] |
| 118 | +def pi (F : Π i, C i ⥤ D i) : (Π i, C i) ⥤ (Π i, D i) := |
| 119 | +{ obj := λ f i, (F i).obj (f i), |
| 120 | + map := λ f g α i, (F i).map (α i) } |
| 121 | + |
| 122 | +-- One could add some natural isomorphisms showing |
| 123 | +-- how `functor.pi` commutes with `pi.eval` and `pi.comap`. |
| 124 | + |
| 125 | +end functor |
| 126 | + |
| 127 | +namespace nat_trans |
| 128 | + |
| 129 | +variables {C} |
| 130 | +variables {D : I → Type u₁} [∀ i, category.{v₁} (D i)] |
| 131 | +variables {F G : Π i, C i ⥤ D i} |
| 132 | + |
| 133 | +/-- |
| 134 | +Assemble an `I`-indexed family of natural transformations into a single natural transformation. |
| 135 | +-/ |
| 136 | +@[simps] |
| 137 | +def pi (α : Π i, F i ⟶ G i) : functor.pi F ⟶ functor.pi G := |
| 138 | +{ app := λ f i, (α i).app (f i), } |
| 139 | + |
| 140 | +end nat_trans |
| 141 | + |
| 142 | +end category_theory |
0 commit comments