refactor(category_theory/cones): golf and cleanup cones (#6756)

No mathematical content here, basically just golfing and tidying in preparation for future PRs.

src/category_theory/limits/cones.lean

@@ -8,12 +8,14 @@ import category_theory.discrete_category
 import category_theory.yoneda
 import category_theory.reflects_isomorphisms
 
-universes v u u' -- morphism levels before object levels. See note [category_theory universes].
+universes v u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 open category_theory
 
 variables {J : Type v} [small_category J]
-variables {C : Type u} [category.{v} C]
+variables {K : Type v} [small_category K]
+variables {C : Type u₁} [category.{v} C]
+variables {D : Type u₂} [category.{v} D]
 
 open category_theory
 open category_theory.category
@@ -31,7 +33,7 @@ natural transformations from the constant functor with value `X` to `F`.
 An object representing this functor is a limit of `F`.
 -/
 @[simps]
-def cones : Cᵒᵖ ⥤ Type v := (const J).op ⋙ (yoneda.obj F)
+def cones : Cᵒᵖ ⥤ Type v := (const J).op ⋙ yoneda.obj F
 
 /--
 `F.cocones` is the functor assigning to an object `X` the type of
@@ -79,14 +81,11 @@ structure cone (F : J ⥤ C) :=
 
 instance inhabited_cone (F : discrete punit ⥤ C) : inhabited (cone F) :=
 ⟨{ X := F.obj punit.star,
-  π :=
-  { app := λ X, match X with
-    | punit.star := 𝟙 _
-    end } }⟩
+   π := { app := λ ⟨⟩, 𝟙 _ } }⟩
 
 @[simp, reassoc] lemma cone.w {F : J ⥤ C} (c : cone F) {j j' : J} (f : j ⟶ j') :
   c.π.app j ≫ F.map f = c.π.app j' :=
-by { rw ← (c.π.naturality f), apply id_comp }
+by { rw ← c.π.naturality f, apply id_comp }
 
 /--
 A `c : cocone F` is
@@ -101,41 +100,36 @@ structure cocone (F : J ⥤ C) :=
 
 instance inhabited_cocone (F : discrete punit ⥤ C) : inhabited (cocone F) :=
 ⟨{ X := F.obj punit.star,
-  ι :=
-  { app := λ X, match X with
-    | punit.star := 𝟙 _
-    end } }⟩
+   ι := { app := λ ⟨⟩, 𝟙 _ } }⟩
 
 @[simp, reassoc] lemma cocone.w {F : J ⥤ C} (c : cocone F) {j j' : J} (f : j ⟶ j') :
   F.map f ≫ c.ι.app j' = c.ι.app j :=
-by { rw (c.ι.naturality f), apply comp_id }
+by { rw c.ι.naturality f, apply comp_id }
 
 variables {F : J ⥤ C}
 
 namespace cone
 
 /-- The isomorphism between a cone on `F` and an element of the functor `F.cones`. -/
+@[simps]
 def equiv (F : J ⥤ C) : cone F ≅ Σ X, F.cones.obj X :=
 { hom := λ c, ⟨op c.X, c.π⟩,
-  inv := λ c, { X := unop c.1, π := c.2 },
-  hom_inv_id' := begin ext1, cases x, refl, end,
-  inv_hom_id' := begin ext1, cases x, refl, end }
+  inv := λ c, { X := c.1.unop, π := c.2 },
+  hom_inv_id' := by { ext1, cases x, refl },
+  inv_hom_id' := by { ext1, cases x, refl } }
 
 /-- A map to the vertex of a cone naturally induces a cone by composition. -/
-@[simp] def extensions (c : cone F) : yoneda.obj c.X ⟶ F.cones :=
+@[simps] def extensions (c : cone F) :
+  yoneda.obj c.X ⟶ F.cones :=
 { app := λ X f, (const J).map f ≫ c.π }
 
 /-- A map to the vertex of a cone induces a cone by composition. -/
-@[simp] def extend (c : cone F) {X : C} (f : X ⟶ c.X) : cone F :=
+@[simps] def extend (c : cone F) {X : C} (f : X ⟶ c.X) : cone F :=
 { X := X,
   π := c.extensions.app (op X) f }
 
-@[simp] lemma extend_π  (c : cone F) {X : Cᵒᵖ} (f : unop X ⟶ c.X) :
-  (extend c f).π = c.extensions.app X f :=
-rfl
-
 /-- Whisker a cone by precomposition of a functor. -/
-@[simps] def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cone F) : cone (E ⋙ F) :=
+@[simps] def whisker (E : K ⥤ J) (c : cone F) : cone (E ⋙ F) :=
 { X := c.X,
   π := whisker_left E c.π }
 
@@ -147,27 +141,23 @@ namespace cocone
 def equiv (F : J ⥤ C) : cocone F ≅ Σ X, F.cocones.obj X :=
 { hom := λ c, ⟨c.X, c.ι⟩,
   inv := λ c, { X := c.1, ι := c.2 },
-  hom_inv_id' := begin ext1, cases x, refl, end,
-  inv_hom_id' := begin ext1, cases x, refl, end }
+  hom_inv_id' := by { ext1, cases x, refl },
+  inv_hom_id' := by { ext1, cases x, refl } }
 
 /-- A map from the vertex of a cocone naturally induces a cocone by composition. -/
-@[simp] def extensions (c : cocone F) : coyoneda.obj (op c.X) ⟶ F.cocones :=
+@[simps] def extensions (c : cocone F) : coyoneda.obj (op c.X) ⟶ F.cocones :=
 { app := λ X f, c.ι ≫ (const J).map f }
 
 /-- A map from the vertex of a cocone induces a cocone by composition. -/
-@[simp] def extend (c : cocone F) {X : C} (f : c.X ⟶ X) : cocone F :=
+@[simps] def extend (c : cocone F) {X : C} (f : c.X ⟶ X) : cocone F :=
 { X := X,
   ι := c.extensions.app X f }
 
-@[simp] lemma extend_ι (c : cocone F) {X : C} (f : c.X ⟶ X) :
-  (extend c f).ι = c.extensions.app X f :=
-rfl
-
 /--
 Whisker a cocone by precomposition of a functor. See `whiskering` for a functorial
 version.
 -/
-@[simps] def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cocone F) : cocone (E ⋙ F) :=
+@[simps] def whisker (E : K ⥤ J) (c : cocone F) : cocone (E ⋙ F) :=
 { X := c.X,
   ι := whisker_left E c.ι }
 
@@ -183,10 +173,10 @@ restate_axiom cone_morphism.w'
 attribute [simp, reassoc] cone_morphism.w
 
 instance inhabited_cone_morphism (A : cone F) : inhabited (cone_morphism A A) :=
-⟨{ hom := 𝟙 _}⟩
+⟨{ hom := 𝟙 _ }⟩
 
 /-- The category of cones on a given diagram. -/
-@[simps] instance cone.category : category.{v} (cone F) :=
+@[simps] instance cone.category : category (cone F) :=
 { hom  := λ A B, cone_morphism A B,
   comp := λ X Y Z f g, { hom := f.hom ≫ g.hom },
   id   := λ B, { hom := 𝟙 B.X } }
@@ -214,16 +204,17 @@ Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to
 -/
 @[simps] 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' :=
-  by intro; erw ← category.assoc; simp [-category.assoc] } }
+  map := λ c₁ c₂ f, { hom := f.hom } }
 
 /-- Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as
 postcomposing by `α` and then by `β`. -/
+@[simps]
 def postcompose_comp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
   postcompose (α ≫ β) ≅ postcompose α ⋙ postcompose β :=
 nat_iso.of_components (λ s, cones.ext (iso.refl _) (by tidy)) (by tidy)
 
 /-- Postcomposing by the identity does not change the cone up to isomorphism. -/
+@[simps]
 def postcompose_id : postcompose (𝟙 F) ≅ 𝟭 (cone F) :=
 nat_iso.of_components (λ s, cones.ext (iso.refl _) (by tidy)) (by tidy)
 
@@ -242,37 +233,32 @@ def postcompose_equivalence {G : J ⥤ C} (α : F ≅ G) : cone F ≌ cone G :=
 Whiskering on the left by `E : K ⥤ J` gives a functor from `cone F` to `cone (E ⋙ F)`.
 -/
 @[simps]
-def whiskering {K : Type v} [small_category K] (E : K ⥤ J) : cone F ⥤ cone (E ⋙ F) :=
+def whiskering (E : K ⥤ J) : cone F ⥤ cone (E ⋙ F) :=
 { obj := λ c, c.whisker E,
-  map := λ c c' f, { hom := f.hom, } }
+  map := λ c c' f, { hom := f.hom } }
 
 /--
 Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
 @[simps]
-def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
+def whiskering_equivalence (e : K ≌ J) :
   cone F ≌ cone (e.functor ⋙ F) :=
 { functor := whiskering e.functor,
-  inverse := whiskering e.inverse ⋙
-    postcompose ((functor.associator _ _ _).inv ≫ (whisker_right (e.counit_iso).hom F) ≫
-      (functor.left_unitor F).hom),
+  inverse := whiskering e.inverse ⋙ postcompose (e.inv_fun_id_assoc F).hom,
   unit_iso := nat_iso.of_components (λ s, cones.ext (iso.refl _) (by tidy)) (by tidy),
   counit_iso := nat_iso.of_components (λ s, cones.ext (iso.refl _)
   (begin
     intro k,
-    have t := s.π.naturality (e.unit_inv.app k),
-    dsimp at t,
-    simp only [←e.counit_app_functor k, id_comp] at t,
-    dsimp,
-    simp [t],
+    dsimp, -- See library note [dsimp, simp]
+    simpa [e.counit_app_functor] using s.w (e.unit_inv.app k),
   end)) (by tidy), }
 
 /--
 The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
 (possibly after changing the indexing category by an equivalence).
 -/
-@[simps functor_obj]
-def equivalence_of_reindexing {K : Type v} [small_category K] {G : K ⥤ C}
+@[simps functor inverse unit_iso counit_iso]
+def equivalence_of_reindexing {G : K ⥤ C}
   (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : cone F ≌ cone G :=
 (whiskering_equivalence e).trans (postcompose_equivalence α)
 
@@ -284,7 +270,7 @@ variable (F)
 def forget : cone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
 
-variables {D : Type u'} [category.{v} D] (G : C ⥤ D)
+variables (G : C ⥤ D)
 
 /-- A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially. -/
 @[simps] def functoriality : cone F ⥤ cone (F ⋙ G) :=
@@ -293,7 +279,7 @@ variables {D : Type u'} [category.{v} D] (G : C ⥤ D)
     π := { app := λ j, G.map (A.π.app j), naturality' := by intros; erw ←G.map_comp; tidy } },
   map := λ X Y f,
   { hom := G.map f.hom,
-    w'  := by intros; rw [←functor.map_comp, f.w] } }
+    w' := λ j, by simp [-cone_morphism.w, ←f.w j] } }
 
 instance functoriality_full [full G] [faithful G] : full (functoriality F G) :=
 { preimage := λ X Y t,
@@ -348,7 +334,7 @@ instance inhabited_cocone_morphism (A : cocone F) : inhabited (cocone_morphism A
 restate_axiom cocone_morphism.w'
 attribute [simp, reassoc] cocone_morphism.w
 
-@[simps] instance cocone.category : category.{v} (cocone F) :=
+@[simps] instance cocone.category : category (cocone F) :=
 { hom  := λ A B, cocone_morphism A B,
   comp := λ _ _ _ f g,
   { hom := f.hom ≫ g.hom },
@@ -403,15 +389,15 @@ def precompose_equivalence {G : J ⥤ C} (α : G ≅ F) : cocone F ≌ cocone G
 Whiskering on the left by `E : K ⥤ J` gives a functor from `cocone F` to `cocone (E ⋙ F)`.
 -/
 @[simps]
-def whiskering {K : Type v} [small_category K] (E : K ⥤ J) : cocone F ⥤ cocone (E ⋙ F) :=
+def whiskering (E : K ⥤ J) : cocone F ⥤ cocone (E ⋙ F) :=
 { obj := λ c, c.whisker E,
   map := λ c c' f, { hom := f.hom, } }
 
 /--
 Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
 @[simps]
-def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
+def whiskering_equivalence (e : K ≌ J) :
   cocone F ≌ cocone (e.functor ⋙ F) :=
 { functor := whiskering e.functor,
   inverse := whiskering e.inverse ⋙
@@ -421,19 +407,16 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
   counit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _)
   (begin
     intro k,
-    have t := s.ι.naturality (e.unit.app k),
-    dsimp at t,
-    simp only [←e.counit_inv_app_functor k, comp_id] at t,
     dsimp,
-    simp [t],
+    simpa [e.counit_inv_app_functor k] using s.w (e.unit.app k),
   end)) (by tidy), }
 
 /--
 The categories of cocones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
 (possibly after changing the indexing category by an equivalence).
 -/
 @[simps functor_obj]
-def equivalence_of_reindexing {K : Type v} [small_category K] {G : K ⥤ C}
+def equivalence_of_reindexing {G : K ⥤ C}
   (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : cocone F ≌ cocone G :=
 (whiskering_equivalence e).trans (precompose_equivalence α.symm)
 
@@ -445,7 +428,7 @@ variable (F)
 def forget : cocone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
 
-variables {D : Type u'} [category.{v} D] (G : C ⥤ D)
+variables (G : C ⥤ D)
 
 /-- A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially. -/
 @[simps] def functoriality : cocone F ⥤ cocone (F ⋙ G) :=
@@ -510,7 +493,6 @@ end limits
 
 namespace functor
 
-variables {D : Type u'} [category.{v} D]
 variables {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D)
 
 open category_theory.limits
@@ -636,8 +618,6 @@ def map_cocone_precompose_equivalence_functor {α : F ≅ G} {c} :
     (cocones.precompose_equivalence (iso_whisker_right α H : _)).functor.obj (H.map_cocone c) :=
 cocones.ext (iso.refl _) (by tidy)
 
-variables {K : Type v} [small_category K]
-
 /--
 `map_cone` commutes with `whisker`
 -/
@@ -682,16 +662,14 @@ variables {F : J ⥤ C}
 { X := unop c.X,
   π :=
   { app := λ j, (c.ι.app (op j)).unop,
-    naturality' := λ j j' f, has_hom.hom.op_inj
-    begin dsimp, simp only [comp_id], exact (c.w f.op).symm, end } }
+    naturality' := λ j j' f, has_hom.hom.op_inj (c.ι.naturality f.op).symm } }
 
 /-- Change a `cone F.op` into a `cocone F`. -/
 @[simps] def cone.unop (c : cone F.op) : cocone F :=
 { X := unop c.X,
   ι :=
   { app := λ j, (c.π.app (op j)).unop,
-    naturality' := λ j j' f, has_hom.hom.op_inj
-    begin dsimp, simp only [id_comp], exact (c.w f.op), end } }
+    naturality' := λ j j' f, has_hom.hom.op_inj (c.π.naturality f.op).symm } }
 
 variables (F)
 
@@ -778,16 +756,17 @@ namespace category_theory.functor
 open category_theory.limits
 
 variables {F : J ⥤ C}
-variables {D : Type u'} [category.{v} D]
 
 section
 variables (G : C ⥤ D)
 
 /-- The opposite cocone of the image of a cone is the image of the opposite cocone. -/
+@[simps {rhs_md := semireducible}]
 def map_cone_op (t : cone F) : (G.map_cone t).op ≅ (G.op.map_cocone t.op) :=
 cocones.ext (iso.refl _) (by tidy)
 
 /-- The opposite cone of the image of a cocone is the image of the opposite cone. -/
+@[simps {rhs_md := semireducible}]
 def map_cocone_op {t : cocone F} : (G.map_cocone t).op ≅ (G.op.map_cone t.op) :=
 cones.ext (iso.refl _) (by tidy)
 

src/category_theory/limits/is_limit.lean

@@ -449,7 +449,7 @@ def of_nat_iso {X : C} (h : yoneda.obj X ≅ F.cones) :
     rw ←hom_of_cone_of_hom h m,
     congr,
     rw cone_of_hom_fac,
-    dsimp, cases s, congr' with j, exact w j,
+    dsimp [cone.extend], cases s, congr' with j, exact w j,
   end }
 end
 
@@ -864,7 +864,7 @@ def of_nat_iso {X : C} (h : coyoneda.obj (op X) ≅ F.cocones) :
     rw ←hom_of_cocone_of_hom h m,
     congr,
     rw cocone_of_hom_fac,
-    dsimp, cases s, congr' with j, exact w j,
+    dsimp [cocone.extend], cases s, congr' with j, exact w j,
   end }
 end