checkpoint

fix universe level in assoc_symm
move hcomp to functor_category, so that we can formulate it using categorical notation
add some extra stuff about natural isos and equivalences
prove some properties about cones and limits

src/category_theory/category.lean

@@ -66,7 +66,7 @@ restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
 attribute [trans] category_struct.comp
 
-lemma category.assoc_symm {C : Type u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
+lemma category.assoc_symm {C : Sort u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
   f ≫ (g ≫ h) = (f ≫ g) ≫ h :=
 by rw ←category.assoc
 

src/category_theory/equivalence.lean

@@ -91,6 +91,28 @@ calc
   end
 }
 
+def fun_inv_id_assoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F :=
+(functor.assoc _ _ _).symm ≪≫ nat_iso.hcomp e.fun_inv_id (iso.refl F) ≪≫ F.id_comp
+
+@[simp] lemma fun_inv_id_assoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+  (fun_inv_id_assoc e F).hom.app X = F.map (e.fun_inv_id.hom.app X) :=
+by { dsimp [fun_inv_id_assoc, nat_iso.hcomp], tidy }
+
+@[simp] lemma fun_inv_id_assoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+  (fun_inv_id_assoc e F).inv.app X = F.map (e.fun_inv_id.inv.app X) :=
+by { dsimp [fun_inv_id_assoc, nat_iso.hcomp], tidy }
+
+def inv_fun_id_assoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F :=
+(functor.assoc _ _ _).symm ≪≫ nat_iso.hcomp e.inv_fun_id (iso.refl F) ≪≫ F.id_comp
+
+@[simp] lemma inv_fun_id_assoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+  (inv_fun_id_assoc e F).hom.app X = F.map (e.inv_fun_id.hom.app X) :=
+by { dsimp [inv_fun_id_assoc, nat_iso.hcomp], tidy }
+
+@[simp] lemma inv_fun_id_assoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+  (inv_fun_id_assoc e F).inv.app X = F.map (e.inv_fun_id.inv.app X) :=
+by { dsimp [inv_fun_id_assoc, nat_iso.hcomp], tidy }
+
 end equivalence
 
 variables {C : Sort u₁} [𝒞 : category.{v₁} C]

src/category_theory/functor_category.lean

@@ -8,7 +8,7 @@ namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-open nat_trans
+open nat_trans category category_theory.functor
 
 variables (C : Sort u₁) [𝒞 : category.{v₁} C] (D : Sort u₂) [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
@@ -31,13 +31,11 @@ variables {C D} {E : Sort u₃} [ℰ : category.{v₃} E]
 
 namespace functor.category
 
-section
-
 @[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
 @[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
   (α ≫ β).app X = α.app X ≫ β.app X := rfl
 
-end
+end functor.category
 
 namespace nat_trans
 -- This section gives two lemmas about natural transformations
@@ -54,9 +52,26 @@ lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟶ G) (Z : D) {X Y : C} (f
   ((F.map f).app Z) ≫ ((T.app Y).app Z) = ((T.app X).app Z) ≫ ((G.map f).app Z) :=
 congr_fun (congr_arg app (T.naturality f)) Z
 
-end nat_trans
+/-- `hcomp α β` is the horizontal composition of natural transformations. -/
+def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : (F ⋙ H) ⟶ (G ⋙ I) :=
+{ app         := λ X : C, (β.app (F.obj X)) ≫ (I.map (α.app X)),
+  naturality' := begin
+                   intros, rw [functor.comp_map, functor.comp_map, assoc_symm, naturality, assoc],
+                   rw [← map_comp I, naturality, map_comp, assoc]
+                 end }
 
-end functor.category
+infix ` ◫ `:80 := hcomp
+
+@[simp] lemma hcomp_app {F G : C ⥤ D} {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) (X : C) :
+  (α ◫ β).app X = (β.app (F.obj X)) ≫ (I.map (α.app X)) := rfl
+
+-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we need to use associativity of functor composition
+
+lemma exchange {F G H : C ⥤ D} {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H)
+  (γ : I ⟶ J) (δ : J ⟶ K) : (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ) :=
+by { ext, intros, dsimp, rw [assoc, assoc, map_comp, assoc_symm (δ.app _), ← naturality, assoc] }
+
+end nat_trans
 
 namespace functor
 
@@ -67,7 +82,7 @@ protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
   { obj := λ j, (F.obj j).obj k,
     map := λ j j' f, (F.map f).app k,
     map_id' := λ X, begin rw category_theory.functor.map_id, refl end,
-    map_comp' := λ X Y Z f g, by rw [functor.map_comp, ←functor.category.comp_app] },
+    map_comp' := λ X Y Z f g, by rw [map_comp, ←functor.category.comp_app] },
   map := λ c c' f,
   { app := λ j, (F.obj j).map f,
     naturality' := λ X Y g, by dsimp; rw ←nat_trans.naturality } }.

src/category_theory/limits/cones.lean

@@ -6,6 +6,7 @@ import category_theory.whiskering
 import category_theory.const
 import category_theory.opposites
 import category_theory.yoneda
+import category_theory.equivalence
 
 universes v u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
 
@@ -187,6 +188,9 @@ namespace cones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.inv_comp_eq.mpr (w j) } }
 
+@[simp] lemma ext_hom_hom {c c' : cone F} (φ : c.X ≅ c'.X)
+  (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j) : (ext φ w).hom.hom = φ.hom := rfl
+
 def postcompose {G : J ⥤ C} (α : F ⟶ G) : cone F ⥤ cone G :=
 { obj := λ c, { X := c.X, π := c.π ≫ α },
   map := λ c₁ c₂ f, { hom := f.hom, w' :=
@@ -201,6 +205,20 @@ def postcompose {G : J ⥤ C} (α : F ⟶ G) : cone F ⥤ cone G :=
 @[simp] lemma postcompose_map_hom {G : J ⥤ C} (α : F ⟶ G) {c₁ c₂ : cone F} (f : c₁ ⟶ c₂):
   ((postcompose α).map f).hom = f.hom := rfl
 
+def postcompose_comp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
+  postcompose (α ≫ β) ≅ postcompose α ⋙ postcompose β :=
+by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }
+
+def postcompose_id : postcompose (𝟙 F) ≅ functor.id (cone F) :=
+by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }
+
+def postcompose_equivalence {G : J ⥤ C} (α : F ≅ G) : cone F ≌ cone G :=
+begin
+  refine ⟨postcompose α.hom, postcompose α.inv, _, _⟩,
+  { refine (postcompose_comp _ _).symm.trans _, rw [iso.hom_inv_id], exact postcompose_id },
+  { refine (postcompose_comp _ _).symm.trans _, rw [iso.inv_hom_id], exact postcompose_id }
+end
+
 def forget : cone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
 
@@ -253,6 +271,9 @@ namespace cocones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.comp_inv_eq.mpr (w j).symm } }
 
+@[simp] lemma ext_hom_hom {c c' : cocone F} (φ : c.X ≅ c'.X)
+  (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j) : (ext φ w).hom.hom = φ.hom := rfl
+
 def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G :=
 { obj := λ c, { X := c.X, ι := α ≫ c.ι },
   map := λ c₁ c₂ f, { hom := f.hom } }
@@ -266,6 +287,20 @@ def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G :=
 @[simp] lemma precompose_map_hom {G : J ⥤ C} (α : G ⟶ F) {c₁ c₂ : cocone F} (f : c₁ ⟶ c₂) :
   ((precompose α).map f).hom = f.hom := rfl
 
+def precompose_comp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
+  precompose (α ≫ β) ≅ precompose β ⋙ precompose α :=
+by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }
+
+def precompose_id : precompose (𝟙 F) ≅ functor.id (cocone F) :=
+by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }
+
+def precompose_equivalence {G : J ⥤ C} (α : G ≅ F) : cocone F ≌ cocone G :=
+begin
+  refine ⟨precompose α.hom, precompose α.inv, _, _⟩,
+  { refine (precompose_comp _ _).symm.trans _, rw [iso.inv_hom_id], exact precompose_id },
+  { refine (precompose_comp _ _).symm.trans _, rw [iso.hom_inv_id], exact precompose_id }
+end
+
 def forget : cocone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
 

src/category_theory/limits/limits.lean

@@ -1,10 +1,11 @@
 -- Copyright (c) 2018 Scott Morrison. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Reid Barton, Mario Carneiro, Scott Morrison
+-- Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
 
 import category_theory.whiskering
 import category_theory.yoneda
 import category_theory.limits.cones
+import category_theory.eq_to_hom
 
 open category_theory category_theory.category category_theory.functor
 
@@ -13,7 +14,7 @@ namespace category_theory.limits
 universes v u u' u'' w -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 -- See the notes at the top of cones.lean, explaining why we can't allow `J : Prop` here.
-variables {J : Type v} [small_category J]
+variables {J K : Type v} [small_category J] [small_category K]
 variables {C : Sort u} [𝒞 : category.{v+1} C]
 include 𝒞
 
@@ -325,8 +326,20 @@ lemma limit.lift_extend {F : J ⥤ C} [has_limit F] (c : cone F) {X : C} (f : X
   limit.lift F (c.extend f) = f ≫ limit.lift F c :=
 by obviously
 
+def has_limit_of_iso {F G : J ⥤ C} [has_limit F] (α : F ≅ G) : has_limit G :=
+begin
+  use (cones.postcompose α.hom).obj (limit.cone F),
+  refine ⟨λ s, limit.lift F ((cones.postcompose α.inv).obj s), _, _⟩,
+  { intros s j,
+    rw [cones.postcompose_obj_π, functor.category.comp_app, limit.cone_π],
+    rw [category.assoc_symm, limit.lift_π], simp },
+  intros s m w, apply limit.hom_ext, intro j,
+  rw [limit.lift_π, cones.postcompose_obj_π, category.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
+  simpa using w j
+end
+
 section pre
-variables {K : Type v} [small_category K]
+variables
 variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
 
 def limit.pre : limit F ⟶ limit (E ⋙ F) :=
@@ -379,14 +392,36 @@ by ext; erw [assoc, limit.post_π, ←H.map_comp, limit.post_π, limit.post_π];
 
 end post
 
-lemma limit.pre_post {K : Type v} [small_category K] {D : Sort u'} [category.{v+1} D]
+lemma limit.pre_post {D : Sort u'} [category.{v+1} D]
   (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
   [has_limit F] [has_limit (E ⋙ F)] [has_limit (F ⋙ G)] [has_limit ((E ⋙ F) ⋙ G)] :
 /- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs -/
 /- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or -/
   G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E :=
 by ext; erw [assoc, limit.post_π, ←G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]; refl
 
+-- def has_limit_of_equivalence {e : K ≌ J} [has_limit (e.functor ⋙ F)] : has_limit F :=
+-- begin
+--   use (cones.postcompose α.hom).obj (limit.cone F),
+--   refine ⟨λ s, limit.lift F ((cones.postcompose α.inv).obj s), _, _⟩,
+--   { intros s j,
+--     rw [cones.postcompose_obj_π, functor.category.comp_app, limit.cone_π],
+--     rw [category.assoc_symm, limit.lift_π], simp },
+--   intros s m w, apply limit.hom_ext, intro j,
+--   rw [limit.lift_π, cones.postcompose_obj_π, category.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
+--   simpa using w j
+-- end
+
+def has_limit_of_equivalence {e : K ≌ J} [has_limit F] : has_limit (e.functor ⋙ F) :=
+begin
+  use cone.whisker e.functor (limit.cone F),
+  refine ⟨λ s, _, _, _⟩,
+  have := limit.lift F _,
+  have := cone.whisker e.inverse s,
+  have := cones.postcompose_equivalence (e.inv_fun_id),
+  all_goals {sorry}
+end
+
 section lim_functor
 
 variables [has_limits_of_shape J C]
@@ -412,11 +447,11 @@ by apply is_limit.fac
   limit.lift F c ≫ lim.map α = limit.lift G ((cones.postcompose α).obj c) :=
 by ext; rw [assoc, lim.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
 
-lemma limit.map_pre {K : Type v} [small_category K] [has_limits_of_shape K C] (E : K ⥤ J) :
+lemma limit.map_pre [has_limits_of_shape K C] (E : K ⥤ J) :
   lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whisker_left E α) :=
 by ext; rw [assoc, limit.pre_π, lim.map_π, assoc, lim.map_π, ←assoc, limit.pre_π]; refl
 
-lemma limit.map_pre' {K : Type v} [small_category K] [has_limits_of_shape.{v} K C]
+lemma limit.map_pre' [has_limits_of_shape.{v} K C]
   (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
   limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whisker_right α F) :=
 by ext1; simp [(category.assoc _ _ _ _).symm]
@@ -441,6 +476,13 @@ nat_iso.of_components (λ F, nat_iso.of_components (λ W, limit.hom_iso F (unop
 
 end lim_functor
 
+def has_limits_of_shape_of_equivalence {J' : Type v} [small_category J']
+  (e : J ≌ J') [has_limits_of_shape J C] : has_limits_of_shape J' C :=
+begin
+  constructor, intro F,
+  sorry
+end
+
 end limit
 
 
@@ -544,8 +586,20 @@ begin
   ext1, rw [←category.assoc], simp
 end
 
+def has_colimit_of_iso {F G : J ⥤ C} [has_colimit F] (α : G ≅ F) : has_colimit G :=
+begin
+  use (cocones.precompose α.hom).obj (colimit.cocone F),
+  refine ⟨λ s, colimit.desc F ((cocones.precompose α.inv).obj s), _, _⟩,
+  { intros s j,
+    rw [cocones.precompose_obj_ι, functor.category.comp_app, colimit.cocone_ι],
+    rw [category.assoc, colimit.ι_desc, ←nat_iso.app_hom, ←iso.eq_inv_comp], refl },
+  intros s m w, apply colimit.hom_ext, intro j,
+  rw [colimit.ι_desc, cocones.precompose_obj_ι, category.comp_app, ←nat_iso.app_inv,
+    iso.eq_inv_comp],
+  simpa using w j
+end
+
 section pre
-variables {K : Type v} [small_category K]
 variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
 
 def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
@@ -615,7 +669,7 @@ end
 
 end post
 
-lemma colimit.pre_post {K : Type v} [small_category K] {D : Sort u'} [category.{v+1} D]
+lemma colimit.pre_post {D : Sort u'} [category.{v+1} D]
   (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
   [has_colimit F] [has_colimit (E ⋙ F)] [has_colimit (F ⋙ G)] [has_colimit ((E ⋙ F) ⋙ G)] :
 /- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs -/
@@ -657,11 +711,11 @@ by rw [←category.assoc, colim.ι_map, category.assoc]
   colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
 by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
 
-lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape K C] (E : K ⥤ J) :
+lemma colimit.pre_map [has_colimits_of_shape K C] (E : K ⥤ J) :
   colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
 by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl
 
-lemma colimit.pre_map' {K : Type v} [small_category K] [has_colimits_of_shape.{v} K C]
+lemma colimit.pre_map' [has_colimits_of_shape.{v} K C]
   (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
   colimit.pre F E₁ = colim.map (whisker_right α F) ≫ colimit.pre F E₂ :=
 by ext1; simp [(category.assoc _ _ _ _).symm]

src/category_theory/natural_isomorphism.lean

@@ -12,7 +12,10 @@ universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `categor
 
 namespace category_theory.nat_iso
 
+open category_theory.category category_theory.functor
+
 variables {C : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
+  {E : Sort u₃} [ℰ : category.{v₃} E]
 include 𝒞 𝒟
 
 def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
@@ -82,6 +85,15 @@ by tidy
 @[simp] def of_components.inv_app (app : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   (of_components app naturality).inv.app X = (app X).inv := rfl
 
+include ℰ
+def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I :=
+begin
+  refine ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, _, _⟩,
+  { ext, rw [←nat_trans.exchange], simp, refl },
+  ext, rw [←nat_trans.exchange], simp, refl
+end
+omit ℰ
+
 end category_theory.nat_iso
 
 open category_theory

src/category_theory/natural_transformation.lean

@@ -78,40 +78,7 @@ rfl
 by tidy
 end
 
-variables {E : Sort u₃} [ℰ : category.{v₃} E]
-include ℰ
-
-/-- `hcomp α β` is the horizontal composition of natural transformations. -/
-def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : nat_trans F G) (β : nat_trans H I) : nat_trans (F ⋙ H) (G ⋙ I) :=
-{ app         := λ X : C, (β.app (F.obj X)) ≫ (I.map (α.app X)),
-  naturality' := begin
-                   /- `obviously'` says: -/
-                   intros,
-                   dsimp,
-                   simp,
-                   -- Actually, obviously doesn't use exactly this sequence of rewrites, but achieves the same result
-                   rw [← assoc, naturality, assoc],
-                   conv { to_rhs, rw [← map_comp, ← α.naturality, map_comp] }
-                 end }
-
-infix ` ◫ `:80 := hcomp
-
-@[simp] lemma hcomp_app {F G : C ⥤ D} {H I : D ⥤ E} (α : nat_trans F G) (β : nat_trans H I) (X : C) :
-  (α ◫ β).app X = (β.app (F.obj X)) ≫ (I.map (α.app X)) := rfl
-
--- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we need to use associativity of functor composition
-
-lemma exchange {F G H : C ⥤ D} {I J K : D ⥤ E} (α : nat_trans F G) (β : nat_trans G H) (γ : nat_trans I J) (δ : nat_trans J K) :
-  ((vcomp α β) ◫ (vcomp γ δ)) = (vcomp (α ◫ γ) (β ◫ δ)) :=
-begin
-  -- `obviously'` says:
-  ext,
-  intros,
-  dsimp,
-  simp,
-  -- again, this isn't actually what obviously says, but it achieves the same effect.
-  conv { to_lhs, congr, skip, rw [←assoc, ←naturality, assoc] }
-end
+/- The horizontal composition is defined in `functor_category` -/
 
 end nat_trans