feat(category_theory/cofinal): cofinal functors (#4218)

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

src/category_theory/is_connected.lean

@@ -157,6 +157,19 @@ begin
   rw [w j, w j'],
 end)
 
+/--
+Another induction principle for `is_preconnected J`:
+given a type family `Z : J → Sort*` and
+a rule for transporting in *both* directions along a morphism in `J`,
+we can transport an `x : Z j₀` to a point in `Z j` for any `j`.
+-/
+lemma is_preconnected_induction [is_preconnected J] (Z : J → Sort*)
+  (h₁ : Π {j₁ j₂ : J} (f : j₁ ⟶ j₂), Z j₁ → Z j₂)
+  (h₂ : Π {j₁ j₂ : J} (f : j₁ ⟶ j₂), Z j₂ → Z j₁)
+  {j₀ : J} (x : Z j₀) (j : J) : nonempty (Z j) :=
+(induct_on_objects {j | nonempty (Z j)} ⟨x⟩
+  (λ j₁ j₂ f, ⟨by { rintro ⟨y⟩, exact ⟨h₁ f y⟩, }, by { rintro ⟨y⟩, exact ⟨h₂ f y⟩, }⟩) j : _)
+
 /-- j₁ and j₂ are related by `zag` if there is a morphism between them. -/
 @[reducible]
 def zag (j₁ j₂ : J) : Prop := nonempty (j₁ ⟶ j₂) ∨ nonempty (j₂ ⟶ j₁)

src/category_theory/isomorphism.lean

@@ -186,19 +186,19 @@ is_iso.inv_hom_id'
   inv f ≫ f ≫ g = g :=
 (as_iso f).inv_hom_id_assoc g
 
-instance (X : C) : is_iso (𝟙 X) :=
+instance id (X : C) : is_iso (𝟙 X) :=
 { inv := 𝟙 X }
 
 instance of_iso (f : X ≅ Y) : is_iso f.hom :=
 { .. f }
 
-instance of_iso_inverse (f : X ≅ Y) : is_iso f.inv :=
+instance of_iso_inv (f : X ≅ Y) : is_iso f.inv :=
 is_iso.of_iso f.symm
 
 variables {f g : X ⟶ Y} {h : Y ⟶ Z}
 
 instance inv_is_iso [is_iso f] : is_iso (inv f) :=
-is_iso.of_iso_inverse (as_iso f)
+is_iso.of_iso_inv (as_iso f)
 
 instance comp_is_iso [is_iso f] [is_iso h] : is_iso (f ≫ h) :=
 is_iso.of_iso $ (as_iso f) ≪≫ (as_iso h)

src/category_theory/limits/cofinal.lean

@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.limits.limits
+import category_theory.punit
+import category_theory.comma
+import category_theory.is_connected
+
+/-!
+# Cofinal functors
+
+A functor `F : C ⥤ D` is cofinal if for every `d : D`,
+the comma category of morphisms `d ⟶ F.obj c` is connected.
+
+We prove that when `F : C ⥤ D` is cofinal,
+the categories of cocones over `G : D ⥤ E` and over `F ⋙ G` are equivalent.
+(In fact, via an equivalence which does not change the cocone point.)
+
+As a consequence, the functor `G : D ⥤ E` has a colimit if and only if `F ⋙ F` does
+(and in either case, the colimits are isomorphic).
+
+There is a converse which we don't prove here.
+I think the correct statement is that if `colimit.pre G F : colimit (F ⋙ G) ⟶ colimit G`
+is an isomorphism for all functors `G : D ⥤ Type v`, then `F` is cofinal.
+(Unfortunately I don't know a reference that gives the proof.)
+
+## Naming
+There is some discrepancy in the literature about naming; some say 'final' instead of 'cofinal'.
+The explanation for this is that the 'co' prefix here is *not* the usual category-theoretic one
+indicating duality, but rather indicating the sense of "along with".
+
+While the trend seems to be towards using 'final', for now we go with the bulk of the literature
+and use 'cofinal'.
+
+## References
+* https://stacks.math.columbia.edu/tag/09WN
+* https://ncatlab.org/nlab/show/final+functor
+* Borceux, Handbook of Categorical Algebra I, Section 2.11.
+  (Note he reverses the roles of definition and main result relative to here!)
+-/
+
+noncomputable theory
+
+universes v u
+
+namespace category_theory
+open category_theory.limits
+
+variables {C : Type v} [small_category C]
+variables {D : Type v} [small_category D]
+
+/--
+A functor `F : C ⥤ D` is cofinal if for every `d : D`, the comma category of morphisms `d ⟶ F.obj c`
+is connected.
+
+See https://stacks.math.columbia.edu/tag/04E6
+-/
+def cofinal (F : C ⥤ D) : Prop :=
+∀ (d : D), is_connected (comma (functor.from_punit d) F)
+
+attribute [class] cofinal
+
+instance (F : C ⥤ D) [ℱ : cofinal F] (d : D) : is_connected (comma (functor.from_punit d) F) :=
+ℱ d
+
+namespace cofinal
+
+variables (F : C ⥤ D) [cofinal F]
+
+instance (d : D) : nonempty (comma (functor.from_punit d) F) := (‹cofinal F› d).is_nonempty
+
+variables {E : Type u} [category.{v} E] (G : D ⥤ E)
+
+/--
+When `F : C ⥤ D` is cofinal, we denote by `lift F d` an arbitrary choice of object in `C` such that
+there exists a morphism `d ⟶ F.obj (lift F d)`.
+-/
+def lift (d : D) : C :=
+(classical.arbitrary (comma (functor.from_punit d) F)).right
+
+/--
+When `F : C ⥤ D` is cofinal, we denote by `hom_to_lift` an arbitrary choice of morphism
+`d ⟶ F.obj (lift F d)`.
+-/
+def hom_to_lift (d : D) : d ⟶ F.obj (lift F d) :=
+(classical.arbitrary (comma (functor.from_punit d) F)).hom
+
+/--
+We provide an induction principle for reasoning about `lift` and `hom_to_lift`.
+We want to perform some construction (usually just a proof) about
+the particular choices `lift F d` and `hom_to_lift F d`,
+it suffices to perform that construction for some other pair of choices
+(denoted `X₀ : C` and `k₀ : d ⟶ F.obj X₀` below),
+and to show that how to transport such a construction
+*both* directions along a morphism between such choices.
+-/
+lemma induction {d : D} (Z : Π (X : C) (k : d ⟶ F.obj X), Prop)
+  (h₁ : Π X₁ X₂ (k₁ : d ⟶ F.obj X₁) (k₂ : d ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
+    (k₁ ≫ F.map f = k₂) → Z X₁ k₁ → Z X₂ k₂)
+  (h₂ : Π X₁ X₂ (k₁ : d ⟶ F.obj X₁) (k₂ : d ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
+    (k₁ ≫ F.map f = k₂) → Z X₂ k₂ → Z X₁ k₁)
+  {X₀ : C} {k₀ : d ⟶ F.obj X₀} (z : Z X₀ k₀) : Z (lift F d) (hom_to_lift F d) :=
+begin
+  apply nonempty.some,
+  apply @is_preconnected_induction _ _ _
+    (λ (Y : comma (functor.from_punit d) F), Z Y.right Y.hom) _ _ { right := X₀, hom := k₀, } z,
+  { intros, fapply h₁ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
+  { intros, fapply h₂ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
+end
+
+variables {F G}
+
+/--
+Given a cocone over `F ⋙ G`, we can construct a `cocone G` with the same cocone point.
+-/
+@[simps]
+def extend_cocone : cocone (F ⋙ G) ⥤ cocone G :=
+{ obj := λ c,
+  { X := c.X,
+    ι :=
+    { app := λ X, G.map (hom_to_lift F X) ≫ c.ι.app (lift F X),
+      naturality' := λ X Y f,
+      begin
+        dsimp, simp,
+        -- This would be true if we'd chosen `lift F X` to be `lift F Y`
+        -- and `hom_to_lift F X` to be `f ≫ hom_to_lift F Y`.
+        apply induction F
+          (λ Z k, G.map f ≫ G.map (hom_to_lift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z),
+        { intros Z₁ Z₂ k₁ k₂ g a z,
+        rw [←a, functor.map_comp, category.assoc, ←functor.comp_map, c.w, z], },
+        { intros Z₁ Z₂ k₁ k₂ g a z,
+        rw [←a, functor.map_comp, category.assoc, ←functor.comp_map, c.w] at z,
+        rw z, },
+        { rw [←functor.map_comp_assoc], },
+      end } },
+  map := λ X Y f,
+  { hom := f.hom, } }
+
+@[simp]
+lemma colimit_cocone_comp_aux (s : cocone (F ⋙ G)) (j : C) :
+  G.map (hom_to_lift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) =
+    s.ι.app j :=
+begin
+  -- This point is that this would be true if we took `lift (F.obj j)` to just be `j`
+  -- and `hom_to_lift (F.obj j)` to be `𝟙 (F.obj j)`.
+  apply induction F (λ X k, G.map k ≫ s.ι.app X = (s.ι.app j : _)),
+  { intros j₁ j₂ k₁ k₂ f w h, rw ←w, rw ← s.w f at h, simpa using h, },
+  { intros j₁ j₂ k₁ k₂ f w h, rw ←w at h, rw ← s.w f, simpa using h, },
+  { exact s.w (𝟙 _), },
+end
+
+variables (F)
+
+/--
+If `F` is cofinal,
+the category of cocones on `F ⋙ G` is equivalent to the category of cocones on `G`.
+-/
+@[simps]
+def cocones_equiv : cocone (F ⋙ G) ≌ cocone G :=
+{ functor := extend_cocone,
+  inverse := cocones.whiskering F,
+  unit_iso := nat_iso.of_components (λ c, cocones.ext (iso.refl _) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ c, cocones.ext (iso.refl _) (by tidy)) (by tidy), }.
+
+/--
+When `F` is cofinal, and `t : cocone G`,
+`t.whisker F` is a colimit coconne exactly when `t` is.
+-/
+def is_colimit_whisker_equiv (t : cocone G) : is_colimit (t.whisker F) ≃ is_colimit t :=
+is_colimit.of_cocone_equiv (cocones_equiv F).symm
+
+/--
+When `F` is cofinal, and `t : cocone (F ⋙ G)`,
+`extend_cocone.obj t` is a colimit coconne exactly when `t` is.
+-/
+def is_colimit_extend_cocone_equiv (t : cocone (F ⋙ G)) :
+  is_colimit (extend_cocone.obj t) ≃ is_colimit t :=
+is_colimit.of_cocone_equiv (cocones_equiv F)
+
+/-- Given a colimit cocone over `G` we can construct a colimit cocone over `F ⋙ G`. -/
+@[simps]
+def colimit_cocone_comp (t : colimit_cocone G) :
+  colimit_cocone (F ⋙ G) :=
+{ cocone := _,
+  is_colimit := (is_colimit_whisker_equiv F _).symm (t.is_colimit) }
+
+@[priority 100]
+instance comp_has_colimit [has_colimit G] :
+  has_colimit (F ⋙ G) :=
+has_colimit.mk (colimit_cocone_comp F (get_colimit_cocone G))
+
+lemma colimit_pre_is_iso_aux {t : cocone G} (P : is_colimit t) :
+  ((is_colimit_whisker_equiv F _).symm P).desc (t.whisker F) = 𝟙 t.X :=
+begin
+  dsimp [is_colimit_whisker_equiv],
+  apply P.hom_ext,
+  tidy,
+end
+
+instance colimit_pre_is_iso [has_colimit G] :
+  is_iso (colimit.pre G F) :=
+begin
+  rw colimit.pre_eq (colimit_cocone_comp F (get_colimit_cocone G)) (get_colimit_cocone G),
+  erw colimit_pre_is_iso_aux,
+  dsimp,
+  apply_instance,
+end
+
+/--
+When `F` is cofinal, and `G` has a colimit, then `F ⋙ G` has a colimit also and
+`colimit (F ⋙ G) ≅ colimit G`
+
+https://stacks.math.columbia.edu/tag/04E7
+-/
+def colimit_iso [has_colimit G] : colimit (F ⋙ G) ≅ colimit G := as_iso (colimit.pre G F)
+
+/-- Given a colimit cocone over `F ⋙ G` we can construct a colimit cocone over `G`. -/
+@[simps]
+def colimit_cocone_of_comp (t : colimit_cocone (F ⋙ G)) :
+  colimit_cocone G :=
+{ cocone := extend_cocone.obj t.cocone,
+  is_colimit := (is_colimit_extend_cocone_equiv F _).symm (t.is_colimit), }
+
+/--
+When `F` is cofinal, and `F ⋙ G` has a colimit, then `G` has a colimit also.
+
+We can't make this an instance, because `F` is not determined by the goal.
+(Even if this weren't a problem, it would cause a loop with `comp_has_colimit`.)
+-/
+lemma has_colimit_of_comp [has_colimit (F ⋙ G)] :
+  has_colimit G :=
+has_colimit.mk (colimit_cocone_of_comp F (get_colimit_cocone (F ⋙ G)))
+
+section
+local attribute [instance] has_colimit_of_comp
+
+/--
+When `F` is cofinal, and `F ⋙ G` has a colimit, then `G` has a colimit also and
+`colimit (F ⋙ G) ≅ colimit G`
+
+https://stacks.math.columbia.edu/tag/04E7
+-/
+def colimit_iso' [has_colimit (F ⋙ G)] : colimit (F ⋙ G) ≅ colimit G := as_iso (colimit.pre G F)
+
+end
+
+end cofinal
+
+end category_theory

src/category_theory/limits/limits.lean

@@ -559,6 +559,20 @@ def of_cocone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D}
   left_inv := by tidy,
   right_inv := by tidy, }
 
+@[simp] lemma of_cocone_equiv_apply_desc {D : Type u'} [category.{v} D] {G : K ⥤ D}
+  (h : cocone G ≌ cocone F) {c : cocone G} (P : is_colimit (h.functor.obj c)) (s) :
+  (of_cocone_equiv h P).desc s =
+    (h.unit.app c).hom ≫
+    (h.inverse.map {hom := P.desc (h.functor.obj s), w' := (by tidy)}).hom ≫
+    (h.unit_inv.app s).hom :=
+rfl
+
+@[simp] lemma of_cocone_equiv_symm_apply_desc {D : Type u'} [category.{v} D] {G : K ⥤ D}
+  (h : cocone G ≌ cocone F) {c : cocone G} (P : is_colimit c) (s) :
+  ((of_cocone_equiv h).symm P).desc s =
+    (h.functor.map {hom := P.desc (h.inverse.obj s), w' := (by tidy)}).hom ≫ (h.counit.app s).hom :=
+rfl
+
 /--
 A cocone precomposed with a natural isomorphism is a colimit cocone
 if and only if the original cocone is.
@@ -968,12 +982,10 @@ variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
 The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.
 -/
 def limit.pre : limit F ⟶ limit (E ⋙ F) :=
-limit.lift (E ⋙ F)
-  { X := limit F,
-    π := { app := λ k, limit.π F (E.obj k) } }
+limit.lift (E ⋙ F) ((limit.cone F).whisker E)
 
 @[simp] lemma limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
-by erw is_limit.fac
+by { erw is_limit.fac, refl }
 
 @[simp] lemma limit.lift_pre (c : cone F) :
   limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) :=
@@ -1245,6 +1257,23 @@ is_colimit.comp_cocone_point_unique_up_to_iso_hom _ _ _
   colimit.ι F j ≫ (is_colimit.cocone_point_unique_up_to_iso hc (colimit.is_colimit _)).inv = c.ι.app j :=
 is_colimit.comp_cocone_point_unique_up_to_iso_inv _ _ _
 
+/--
+Given any other colimit cocone for `F`, the chosen `colimit F` is isomorphic to the cocone point.
+-/
+def colimit.iso_colimit_cocone {F : J ⥤ C} [has_colimit F] (t : colimit_cocone F) :
+  colimit F ≅ t.cocone.X :=
+is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit F) t.is_colimit
+
+@[simp, reassoc] lemma colimit.iso_colimit_cocone_ι_hom
+  {F : J ⥤ C} [has_colimit F] (t : colimit_cocone F) (j : J) :
+  colimit.ι F j ≫ (colimit.iso_colimit_cocone t).hom = t.cocone.ι.app j :=
+by { dsimp [colimit.iso_colimit_cocone, is_colimit.cocone_point_unique_up_to_iso], tidy, }
+
+@[simp, reassoc] lemma colimit.iso_colimit_cocone_ι_inv
+  {F : J ⥤ C} [has_colimit F] (t : colimit_cocone F) (j : J) :
+  t.cocone.ι.app j ≫ (colimit.iso_colimit_cocone t).inv = colimit.ι F j :=
+by { dsimp [colimit.iso_colimit_cocone, is_colimit.cocone_point_unique_up_to_iso], tidy, }
+
 @[ext] lemma colimit.hom_ext {F : J ⥤ C} [has_colimit F] {X : C} {f f' : colimit F ⟶ X}
   (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f' :=
 (colimit.is_colimit F).hom_ext w
@@ -1356,12 +1385,10 @@ variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
 The canonical morphism from the colimit of `E ⋙ F` to the colimit of `F`.
 -/
 def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
-colimit.desc (E ⋙ F)
-  { X := colimit F,
-    ι := { app := λ k, colimit.ι F (E.obj k) } }
+colimit.desc (E ⋙ F) ((colimit.cocone F).whisker E)
 
 @[simp, reassoc] lemma colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
-by erw is_colimit.fac
+by { erw is_colimit.fac, refl, }
 
 @[simp] lemma colimit.pre_desc (c : cocone F) :
   colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) :=
@@ -1378,6 +1405,18 @@ begin
   exact (colimit.ι_pre F (D ⋙ E) j).symm
 end
 
+variables {E F}
+
+/---
+If we have particular colimit cocones available for `E ⋙ F` and for `F`,
+we obtain a formula for `colimit.pre F E`.
+-/
+lemma colimit.pre_eq (s : colimit_cocone (E ⋙ F)) (t : colimit_cocone F) :
+  colimit.pre F E =
+    (colimit.iso_colimit_cocone s).hom ≫ s.is_colimit.desc ((t.cocone).whisker E) ≫
+      (colimit.iso_colimit_cocone t).inv :=
+by tidy
+
 end pre
 
 section post