feat(category_theory): functoriality of (co)cones

leanprover-community · Dec 3, 2018 · 5a0df7d · 5a0df7d
1 parent 5856459
commit 5a0df7d
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 0 deletions.
diff --git a/category_theory/limits/cones.lean b/category_theory/limits/cones.lean
@@ -45,6 +45,28 @@ lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟹ (const J).obj X) := rfl
 
 end functor
 
+section functoriality
+variables (J C)
+
+def cones : (J ⥤ C) ⥤ Cᵒᵖ ⥤ Type _ :=
+{ obj := functor.cones,
+  map := λ F G f, whisker_left _ $ whisker_left _ (yoneda.map f) }
+
+def cocones : (J ⥤ C)ᵒᵖ ⥤ C ⥤ Type _ :=
+{ obj := functor.cocones,
+  map := λ F G f, whisker_left _ (coyoneda.map f) }
+
+variables {J C}
+
+@[simp] lemma cones_obj (F : J ⥤ C) : (cones J C).obj F = F.cones := rfl
+@[simp] lemma cones_map  {F G : J ⥤ C} {f : F ⟶ G} :
+(cones J C).map f = (whisker_left _ $ whisker_left _ (yoneda.map f)) := rfl
+
+@[simp] lemma cocones_obj (F : J ⥤ C) : (cocones J C).obj F = F.cocones := rfl
+@[simp] lemma cocones_map  {F G : J ⥤ C} {f : F ⟶ G} :
+(cocones J C).map f = (whisker_left _ (coyoneda.map f)) := rfl
+
+end functoriality
 
 namespace limits
 

diff --git a/category_theory/limits/limits.lean b/category_theory/limits/limits.lean
@@ -373,6 +373,9 @@ begin
   refl
 end
 
+def lim_yoneda : lim ⋙ yoneda ≅ category_theory.cones J C :=
+nat_iso.of_components (λ F, nat_iso.of_components (limit.hom_iso F) (by tidy)) (by tidy)
+
 end lim_functor
 
 end limit
@@ -575,6 +578,11 @@ begin
   refl
 end
 
+def colim_coyoneda : colim.op ⋙ coyoneda ≅ category_theory.cocones J C :=
+nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso F)
+  (by {tidy, dsimp [functor.cocones], rw category.assoc }))
+  (by {tidy, rw [← category.assoc,← category.assoc], tidy })
+
 end colim_functor
 
 end colimit

diff --git a/category_theory/opposites.lean b/category_theory/opposites.lean
@@ -79,6 +79,15 @@ definition op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ :=
 
 end
 
+namespace category
+variables {C} {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+@[simp] lemma op_id_app (F : (C ⥤ D)ᵒᵖ) (X : C) : (𝟙 F : F ⟹ F).app X = 𝟙 (F.obj X) := rfl
+@[simp] lemma op_comp_app {F G H : (C ⥤ D)ᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
+  ((α ≫ β) : H ⟹ F).app X = (β : H ⟹ G).app X ≫ (α : G ⟹ F).app X := rfl
+end category
+
 section
 
 variable (C)