chore(category_theory/limits/types): cleanup (#3871)

Backporting some cleaning up work from `prop_limits`, while it rumbles onwards.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/limits.lean

@@ -63,8 +63,8 @@ end
 def limit_π_linear_map (F : J ⥤ Module R) (j) :
   limit (F ⋙ forget (Module R)) →ₗ[R] (F ⋙ forget (Module R)).obj j :=
 { to_fun := limit.π (F ⋙ forget (Module R)) j,
-  map_smul' := λ x y, by { simp only [types.types_limit_π], refl },
-  map_add' := λ x y, by { simp only [types.types_limit_π], refl } }
+  map_smul' := λ x y, rfl,
+  map_add' := λ x y, rfl }
 
 namespace has_limits
 -- The next two definitions are used in the construction of `has_limits (Module R)`.

src/algebra/category/Mon/limits.lean

@@ -58,8 +58,8 @@ instance limit_monoid (F : J ⥤ Mon) :
 def limit_π_monoid_hom (F : J ⥤ Mon) (j) :
   limit (F ⋙ forget Mon) →* (F ⋙ forget Mon).obj j :=
 { to_fun := limit.π (F ⋙ forget Mon) j,
-  map_one' := by { simp only [types.types_limit_π], refl },
-  map_mul' := λ x y, by { simp only [types.types_limit_π], refl } }
+  map_one' := rfl,
+  map_mul' := λ x y, rfl }
 
 namespace has_limits
 -- The next two definitions are used in the construction of `has_limits Mon`.

src/category_theory/limits/limits.lean

@@ -63,6 +63,7 @@ def mk_cone_morphism {t : cone F}
     congr_arg cone_morphism.hom this }
 
 /-- Limit cones on `F` are unique up to isomorphism. -/
+@[simps]
 def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t :=
 { hom := Q.lift_cone_morphism s,
   inv := P.lift_cone_morphism t,
@@ -416,6 +417,7 @@ def mk_cocone_morphism {t : cocone F}
     congr_arg cocone_morphism.hom this }
 
 /-- Colimit cocones on `F` are unique up to isomorphism. -/
+@[simps]
 def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s ≅ t :=
 { hom := P.desc_cocone_morphism t,
   inv := Q.desc_cocone_morphism s,

src/category_theory/limits/preserves/basic.lean

@@ -43,8 +43,16 @@ variables {D : Type u₂} [category.{v} D]
 
 variables {J : Type v} [small_category J] {K : J ⥤ C}
 
+/--
+A functor `F` preserves limits of shape `K` (written as `preserves_limit K F`)
+if `F` maps any limit cone over `K` to a limit cone.
+-/
 class preserves_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (preserves : Π {c : cone K}, is_limit c → is_limit (F.map_cone c))
+/--
+A functor `F` preserves colimits of shape `K` (written as `preserves_colimit K F`)
+if `F` maps any colimit cocone over `K` to a colimit cocone.
+-/
 class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c))
 
@@ -162,25 +170,54 @@ def preserves_colimit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K
     simp,
   end }
 
-/-
-A functor F : C → D reflects limits if whenever the image of a cone
-under F is a limit cone in D, the cone was already a limit cone in C.
-Note that again we do not assume a priori that D actually has any
-limits.
+/--
+A functor `F : C ⥤ D` reflects limits for `K : J ⥤ C` if
+whenever the image of a cone over `K` under `F` is a limit cone in `D`,
+the cone was already a limit cone in `C`.
+Note that we do not assume a priori that `D` actually has any limits.
 -/
-
 class reflects_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (reflects : Π {c : cone K}, is_limit (F.map_cone c) → is_limit c)
+/--
+A functor `F : C ⥤ D` reflects colimits for `K : J ⥤ C` if
+whenever the image of a cocone over `K` under `F` is a colimit cocone in `D`,
+the cocone was already a colimit cocone in `C`.
+Note that we do not assume a priori that `D` actually has any colimits.
+-/
 class reflects_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (reflects : Π {c : cocone K}, is_colimit (F.map_cocone c) → is_colimit c)
 
+/--
+A functor `F : C ⥤ D` reflects limits of shape `J` if
+whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
+the cone was already a limit cone in `C`.
+Note that we do not assume a priori that `D` actually has any limits.
+-/
 class reflects_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (reflects_limit : Π {K : J ⥤ C}, reflects_limit K F)
+/--
+A functor `F : C ⥤ D` reflects colimits of shape `J` if
+whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
+the cocone was already a colimit cocone in `C`.
+Note that we do not assume a priori that `D` actually has any colimits.
+-/
 class reflects_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (reflects_colimit : Π {K : J ⥤ C}, reflects_colimit K F)
 
+/--
+A functor `F : C ⥤ D` reflects limits if
+whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
+the cone was already a limit cone in `C`.
+Note that we do not assume a priori that `D` actually has any limits.
+-/
 class reflects_limits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
 (reflects_limits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_limits_of_shape J F)
+/--
+A functor `F : C ⥤ D` reflects colimits if
+whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
+the cocone was already a colimit cocone in `C`.
+Note that we do not assume a priori that `D` actually has any colimits.
+-/
 class reflects_colimits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) :=
 (reflects_colimits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_colimits_of_shape J F)
 
@@ -245,6 +282,29 @@ instance comp_reflects_colimit [reflects_colimit K F] [reflects_colimit (K ⋙ F
   reflects_colimit K (F ⋙ G) :=
 ⟨λ c h, reflects_colimit.reflects (reflects_colimit.reflects h)⟩
 
+/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`,
+then `F` preserves limits for `K`. -/
+def preserves_limit_of_reflects_of_preserves [preserves_limit K (F ⋙ G)]
+  [reflects_limit (K ⋙ F) G] : preserves_limit K F :=
+⟨λ c h,
+ begin
+  apply @reflects_limit.reflects _ _ _ _ _ _ _ G,
+  change limits.is_limit ((F ⋙ G).map_cone c),
+  exact preserves_limit.preserves h
+ end⟩
+
+/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
+then `F` preserves colimits for `K`. -/
+def preserves_colimit_of_reflects_of_preserves [preserves_colimit K (F ⋙ G)]
+  [reflects_colimit (K ⋙ F) G] : preserves_colimit K F :=
+⟨λ c h,
+ begin
+  apply @reflects_colimit.reflects _ _ _ _ _ _ _ G,
+  change limits.is_colimit ((F ⋙ G).map_cocone c),
+  exact preserves_colimit.preserves h
+ end⟩
+
+
 end
 
 variable (F : C ⥤ D)

src/category_theory/limits/shapes/types.lean

@@ -179,6 +179,6 @@ by ext
 @[simp] lemma sigma_desc {J : Type u} {f : J → Type u} {W : Type u} {g : Π j, f j ⟶ W} {p : Σ j, f j} :
   (sigma.desc g) p = g p.1 p.2 := rfl
 @[simp] lemma sigma_map {J : Type u} {f g : J → Type u} {h : Π j, f j ⟶ g j} :
-  sigma.map h = λ (k : Σ j, f j), (⟨k.1, h k.1 (k.2)⟩ : Σ j, g j) := rfl
+  limits.sigma.map h = λ (k : Σ j, f j), (⟨k.1, h k.1 (k.2)⟩ : Σ j, g j) := rfl
 
 end category_theory.limits.types

src/category_theory/limits/types.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Reid Barton
 -/
 import category_theory.limits.shapes.images
+import tactic.equiv_rw
 
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
@@ -14,79 +15,104 @@ namespace category_theory.limits.types
 
 variables {J : Type u} [small_category J]
 
-/-- (internal implementation) the limit cone of a functor, implemented as flat sections of a pi type -/
-def limit_ (F : J ⥤ Type u) : cone F :=
+/--
+(internal implementation) the limit cone of a functor,
+implemented as flat sections of a pi type
+-/
+def limit_cone (F : J ⥤ Type u) : cone F :=
 { X := F.sections,
   π := { app := λ j u, u.val j } }
 
 local attribute [elab_simple] congr_fun
 /-- (internal implementation) the fact that the proposed limit cone is the limit -/
-def limit_is_limit_ (F : J ⥤ Type u) : is_limit (limit_ F) :=
+def limit_cone_is_limit (F : J ⥤ Type u) : is_limit (limit_cone F) :=
 { lift := λ s v, ⟨λ j, s.π.app j v, λ j j' f, congr_fun (cone.w s f) _⟩,
   uniq' := by { intros, ext x j, exact congr_fun (w j) x } }
 
 instance : has_limits (Type u) :=
-{ has_limits_of_shape := λ J 𝒥,
-  { has_limit := λ F, by exactI { cone := limit_ F, is_limit := limit_is_limit_ F } } }
-
-
--- We don't make any of these `simp` lemmas:
--- it's up to the user to decide to stop using the limits API,
--- and rely on the particular implementation.
-lemma types_limit (F : J ⥤ Type u) :
-  limits.limit F = {u : Π j, F.obj j // ∀ {j j'} f, F.map f (u j) = u j'} := rfl
-lemma types_limit_π (F : J ⥤ Type u) (j : J) (g : limit F) :
-  limit.π F j g = g.val j := rfl
-lemma types_limit_pre
-  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : limit F) :
-  limit.pre F E g = (⟨λ k, g.val (E.obj k), by obviously⟩ : limit (E ⋙ F)) := rfl
-lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : limit F) :
-  (lim.map α : limit F → limit G) g =
-  (⟨λ j, (α.app j) (g.val j), λ j j' f,
-    by {rw ←functor_to_types.naturality, dsimp, rw ←(g.prop f)}⟩ : limit G) := rfl
-
-lemma types_limit_lift (F : J ⥤ Type u) (c : cone F) (x : c.X) :
-  limit.lift F c x = (⟨λ j, c.π.app j x, λ j j' f, congr_fun (cone.w c f) x⟩ : limit F) :=
+{ has_limits_of_shape := λ J 𝒥, by exactI
+  { has_limit := λ F,
+    { cone := limit_cone F, is_limit := limit_cone_is_limit F } } }
+
+/--
+The equivalence between the abstract limit of `F` in `Type u`
+and the "concrete" definition as the sections of `F`.
+-/
+def limit_equiv_sections (F : J ⥤ Type u) : (limit F : Type u) ≃ F.sections :=
+(is_limit.cone_point_unique_up_to_iso (limit.is_limit F) (limit_cone_is_limit F)).to_equiv
+
+@[simp]
+lemma limit_equiv_sections_apply (F : J ⥤ Type u) (x : limit F) (j : J) :
+  (((limit_equiv_sections F) x) : Π j, F.obj j) j = limit.π F j x :=
 rfl
 
-/-- (internal implementation) the limit cone of a functor, implemented as a quotient of a sigma type -/
-def colimit_ (F : J ⥤ Type u) : cocone F :=
-{ X := @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2),
+@[simp]
+lemma limit_equiv_sections_symm_apply (F : J ⥤ Type u) (x : F.sections) (j : J) :
+  limit.π F j ((limit_equiv_sections F).symm x) = (x : Π j, F.obj j) j :=
+begin
+  equiv_rw (limit_equiv_sections F).symm at x,
+  simp,
+end
+
+-- PROJECT: prove this for concrete categories where the forgetful functor preserves limits
+lemma limit_ext (F : J ⥤ Type u) (x y : limit F) (w : ∀ j, limit.π F j x = limit.π F j y) :
+  x = y :=
+begin
+  apply (limit_equiv_sections F).injective,
+  ext j,
+  simp [w j],
+end
+
+-- TODO: are there other limits lemmas that should have `_apply` versions?
+-- Can we generate these like with `@[reassoc]`?
+-- PROJECT: prove these for any concrete category where the forgetful functor preserves limits?
+@[simp]
+lemma lift_π_apply (F : J ⥤ Type u) (s : cone F) (j : J) (x : s.X) :
+  limit.π F j (limit.lift F s x) = s.π.app j x :=
+congr_fun (limit.lift_π s j) x
+
+/--
+A quotient type implementing the colimit of a functor `F : J ⥤ Type u`,
+as pairs `⟨j, x⟩` where `x : F.obj j`, modulo the equivalence relation generated by
+`⟨j, x⟩ ~ ⟨j', x'⟩` whenever there is a morphism `f : j ⟶ j'` so `F.map f x = x'`.
+-/
+@[nolint has_inhabited_instance]
+def quot (F : J ⥤ Type u) : Type u :=
+@quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2)
+
+/--
+(internal implementation) the colimit cocone of a functor,
+implemented as a quotient of a sigma type
+-/
+def colimit_cocone (F : J ⥤ Type u) : cocone F :=
+{ X := quot F,
   ι :=
   { app := λ j x, quot.mk _ ⟨j, x⟩,
     naturality' := λ j j' f, funext $ λ x, eq.symm (quot.sound ⟨f, rfl⟩) } }
 
 local attribute [elab_with_expected_type] quot.lift
 
 /-- (internal implementation) the fact that the proposed colimit cocone is the colimit -/
-def colimit_is_colimit_ (F : J ⥤ Type u) : is_colimit (colimit_ F) :=
+def colimit_cocone_is_colimit (F : J ⥤ Type u) : is_colimit (colimit_cocone F) :=
 { desc := λ s, quot.lift (λ (p : Σ j, F.obj j), s.ι.app p.1 p.2)
     (assume ⟨j, x⟩ ⟨j', x'⟩ ⟨f, hf⟩, by rw hf; exact (congr_fun (cocone.w s f) x).symm) }
 
 instance : has_colimits (Type u) :=
-{ has_colimits_of_shape := λ J 𝒥,
-  { has_colimit := λ F, by exactI { cocone := colimit_ F, is_colimit := colimit_is_colimit_ F } } }
-
-lemma types_colimit (F : J ⥤ Type u) :
-  limits.colimit F = @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2) := rfl
-lemma types_colimit_ι (F : J ⥤ Type u) (j : J) :
-  colimit.ι F j = λ x, quot.mk _ ⟨j, x⟩ := rfl
-lemma types_colimit_pre
-  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) :
-  colimit.pre F E =
-  quot.lift (λ p, quot.mk _ ⟨E.obj p.1, p.2⟩) (λ p p' ⟨f, h⟩, quot.sound ⟨E.map f, h⟩) := rfl
-lemma types_colimit_map {F G : J ⥤ Type u} (α : F ⟶ G) :
-  (colim.map α : colimit F → colimit G) =
-  quot.lift
-    (λ p, quot.mk _ ⟨p.1, (α.app p.1) p.2⟩)
-    (λ p p' ⟨f, h⟩, quot.sound ⟨f, by rw h; exact functor_to_types.naturality _ _ α f _⟩) := rfl
-
-lemma types_colimit_desc (F : J ⥤ Type u) (c : cocone F) :
-  colimit.desc F c =
-  quot.lift
-    (λ p, c.ι.app p.1 p.2)
-    (λ p p' ⟨f, h⟩, by rw h; exact (functor_to_types.naturality _ _ c.ι f _).symm) := rfl
+{ has_colimits_of_shape := λ J 𝒥, by exactI
+  { has_colimit := λ F,
+    { cocone := colimit_cocone F, is_colimit := colimit_cocone_is_colimit F } } }
+
+/--
+The equivalence between the abstract colimit of `F` in `Type u`
+and the "concrete" definition as a quotient.
+-/
+def colimit_equiv_quot (F : J ⥤ Type u) : (colimit F : Type u) ≃ quot F :=
+(is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit F) (colimit_cocone_is_colimit F)).to_equiv
 
+@[simp]
+lemma colimit_equiv_quot_symm_apply (F : J ⥤ Type u) (j : J) (x : F.obj j) :
+  (colimit_equiv_quot F).symm (quot.mk _ ⟨j, x⟩) = colimit.ι F j x :=
+rfl
 
 variables {α β : Type u} (f : α ⟶ β)