feat(category_theory/limits): colimits from finite colimits and filte…

…red colimits (#16373)

We will use this in the future to show that if C has finite colimits, then Ind(C) is cocomplete.

src/category_theory/functor/flat.lean

@@ -169,8 +169,7 @@ variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₁} D
 
 local attribute [instance] has_finite_limits_of_has_finite_limits_of_size
 
-@[priority 100]
-instance cofiltered_of_has_finite_limits [has_finite_limits C] : is_cofiltered C :=
+lemma cofiltered_of_has_finite_limits [has_finite_limits C] : is_cofiltered C :=
 { cocone_objs := λ A B, ⟨limits.prod A B, limits.prod.fst, limits.prod.snd, trivial⟩,
   cocone_maps :=  λ A B f g, ⟨equalizer f g, equalizer.ι f g, equalizer.condition f g⟩,
   nonempty := ⟨⊤_ C⟩ }
@@ -183,7 +182,7 @@ begin
     apply has_finite_limits_of_has_finite_limits_of_size.{v₁} (structured_arrow X F),
     intros J sJ fJ, resetI, constructor
   end,
-  apply_instance
+  exact cofiltered_of_has_finite_limits
 end⟩
 
 namespace preserves_finite_limits_of_flat

src/category_theory/limits/constructions/filtered.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.limits.constructions.limits_of_products_and_equalizers
+import category_theory.limits.opposites
+
+/-!
+# Constructing colimits from finite colimits and filtered colimits
+
+We construct colimits of size `w` from finite colimits and filtered colimits of size `w`. Since
+`w`-sized colimits are constructured from coequalizers and `w`-sized coproducts, it suffices to
+construct `w`-sized coproducts from finite coproducts and `w`-sized filtered colimits.
+
+The idea is simple: to construct coproducts of shape `α`, we take the colimit of the filtered
+diagram of all coproducts of finite subsets of `α`.
+
+We also deduce the dual statement by invoking the original statement in `Cᵒᵖ`.
+-/
+
+universes w v u
+
+noncomputable theory
+
+open category_theory
+
+variables {C : Type u} [category.{v} C] {α : Type w}
+
+namespace category_theory.limits
+
+namespace coproducts_from_finite_filtered
+local attribute [tidy] tactic.case_bash
+
+/-- If `C` has finite coproducts, a functor `discrete α ⥤ C` lifts to a functor
+    `finset (discrete α) ⥤ C` by taking coproducts. -/
+@[simps]
+def lift_to_finset [has_finite_coproducts C] (F : discrete α ⥤ C) : finset (discrete α) ⥤ C :=
+{ obj := λ s, ∐ λ x : s, F.obj x,
+  map := λ s t h, sigma.desc (λ y, sigma.ι (λ x : t, F.obj x) ⟨y, h.down.down y.2⟩) }
+
+/-- If `C` has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
+    taking the colimit of the diagram formed by the coproducts of finite sets over the indexing
+    type. -/
+@[simps]
+def lift_to_finset_colimit_cocone [has_finite_coproducts C] [has_filtered_colimits_of_size.{w w} C]
+  [decidable_eq α] (F : discrete α ⥤ C) : colimit_cocone F :=
+{ cocone :=
+  { X := colimit (lift_to_finset F),
+    ι := discrete.nat_trans $ λ j,
+      @sigma.ι _ _ _ (λ x : ({j} : finset (discrete α)), F.obj x) _ ⟨j, by simp⟩ ≫
+      colimit.ι (lift_to_finset F) {j} },
+  is_colimit :=
+  { desc := λ s, colimit.desc (lift_to_finset F)
+    { X := s.X,
+      ι := { app := λ t, sigma.desc (λ x, s.ι.app x) } },
+    uniq' := λ s m h,
+    begin
+      ext t ⟨⟨j, hj⟩⟩,
+      convert h j using 1,
+      { simp [← colimit.w (lift_to_finset F) ⟨⟨finset.singleton_subset_iff.2 hj⟩⟩], refl },
+      { tidy }
+    end } }
+
+end coproducts_from_finite_filtered
+
+open coproducts_from_finite_filtered
+
+lemma has_coproducts_of_finite_and_filtered [has_finite_coproducts C]
+  [has_filtered_colimits_of_size.{w w} C] : has_coproducts.{w} C :=
+λ α, by { classical, exactI ⟨λ F, has_colimit.mk (lift_to_finset_colimit_cocone F)⟩ }
+
+lemma has_colimits_of_finite_and_filtered [has_finite_colimits C]
+  [has_filtered_colimits_of_size.{w w} C] : has_colimits_of_size.{w w} C :=
+have has_coproducts.{w} C, from has_coproducts_of_finite_and_filtered,
+by exactI has_colimits_of_has_coequalizers_and_coproducts
+
+lemma has_products_of_finite_and_cofiltered [has_finite_products C]
+  [has_cofiltered_limits_of_size.{w w} C] : has_products.{w} C :=
+have has_coproducts.{w} Cᵒᵖ, from has_coproducts_of_finite_and_filtered,
+by exactI has_products_of_opposite
+
+lemma has_limits_of_finite_and_cofiltered [has_finite_limits C]
+  [has_cofiltered_limits_of_size.{w w} C] : has_limits_of_size.{w w} C :=
+have has_products.{w} C, from has_products_of_finite_and_cofiltered,
+by exactI has_limits_of_has_equalizers_and_products
+
+end category_theory.limits

src/category_theory/limits/filtered.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.filtered
+import category_theory.limits.has_limits
+
+/-!
+# Possession of filtered colimits
+-/
+
+universes w' w v u
+
+noncomputable theory
+
+open category_theory
+
+variables {C : Type u} [category.{v} C]
+
+namespace category_theory.limits
+
+section
+variables (C)
+
+/-- Class for having all cofiltered limits of a given size. -/
+class has_cofiltered_limits_of_size : Prop :=
+(has_limits_of_shape : Π (I : Type w) [category.{w'} I] [is_cofiltered I], has_limits_of_shape I C)
+
+/-- Class for having all filtered colimits of a given size. -/
+class has_filtered_colimits_of_size : Prop :=
+(has_colimits_of_shape : Π (I : Type w) [category.{w'} I] [is_filtered I],
+  has_colimits_of_shape I C)
+
+end
+
+@[priority 100]
+instance has_limits_of_shape_of_has_cofiltered_limits [has_cofiltered_limits_of_size.{w' w} C]
+  (I : Type w) [category.{w'} I] [is_cofiltered I] : has_limits_of_shape I C :=
+has_cofiltered_limits_of_size.has_limits_of_shape _
+
+@[priority 100]
+instance has_colimits_of_shape_of_has_filtered_colimits [has_filtered_colimits_of_size.{w' w} C]
+  (I : Type w) [category.{w'} I] [is_filtered I] : has_colimits_of_shape I C :=
+has_filtered_colimits_of_size.has_colimits_of_shape _
+
+end category_theory.limits

src/category_theory/limits/opposites.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Floris van Doorn
 -/
+import category_theory.limits.filtered
 import category_theory.limits.shapes.finite_products
 import category_theory.discrete_category
 import tactic.equiv_rw
@@ -216,20 +217,40 @@ has_limit.mk
 { cone := cone_of_cocone_left_op (colimit.cocone F.left_op),
   is_limit := is_limit_cone_of_cocone_left_op _ (colimit.is_colimit _) }
 
+lemma has_limit_of_has_colimit_op (F : J ⥤ C) [has_colimit F.op] : has_limit F :=
+has_limit.mk
+{ cone := (colimit.cocone F.op).unop,
+  is_limit := is_limit_cocone_unop _ (colimit.is_colimit _) }
+
 /--
 If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
 -/
 lemma has_limits_of_shape_op_of_has_colimits_of_shape [has_colimits_of_shape Jᵒᵖ C] :
   has_limits_of_shape J Cᵒᵖ :=
 { has_limit := λ F, has_limit_of_has_colimit_left_op F }
 
+lemma has_limits_of_shape_of_has_colimits_of_shape_op [has_colimits_of_shape Jᵒᵖ Cᵒᵖ] :
+  has_limits_of_shape J C :=
+{ has_limit := λ F, has_limit_of_has_colimit_op F }
+
 local attribute [instance] has_limits_of_shape_op_of_has_colimits_of_shape
 
 /--
 If `C` has colimits, we can construct limits for `Cᵒᵖ`.
 -/
 instance has_limits_op_of_has_colimits [has_colimits C] : has_limits Cᵒᵖ := ⟨infer_instance⟩
 
+lemma has_limits_of_has_colimits_op [has_colimits Cᵒᵖ] : has_limits C :=
+{ has_limits_of_shape := λ J hJ, by exactI has_limits_of_shape_of_has_colimits_of_shape_op }
+
+instance has_cofiltered_limits_op_of_has_filtered_colimits
+  [has_filtered_colimits_of_size.{v₂ u₂} C] : has_cofiltered_limits_of_size.{v₂ u₂} Cᵒᵖ :=
+{ has_limits_of_shape := λ I hI₁ hI₂, by exactI has_limits_of_shape_op_of_has_colimits_of_shape }
+
+lemma has_cofiltered_limits_of_has_filtered_colimits_op
+  [has_filtered_colimits_of_size.{v₂ u₂} Cᵒᵖ] : has_cofiltered_limits_of_size.{v₂ u₂} C :=
+{ has_limits_of_shape := λ I hI₂ hI₂, by exactI has_limits_of_shape_of_has_colimits_of_shape_op }
+
 /--
 If `F.left_op : Jᵒᵖ ⥤ C` has a limit, we can construct a colimit for `F : J ⥤ Cᵒᵖ`.
 -/
@@ -238,58 +259,100 @@ has_colimit.mk
 { cocone := cocone_of_cone_left_op (limit.cone F.left_op),
   is_colimit := is_colimit_cocone_of_cone_left_op _ (limit.is_limit _) }
 
+lemma has_colimit_of_has_limit_op (F : J ⥤ C) [has_limit F.op] : has_colimit F :=
+has_colimit.mk
+{ cocone := (limit.cone F.op).unop,
+  is_colimit := is_colimit_cone_unop _ (limit.is_limit _) }
+
 /--
 If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
 -/
-lemma has_colimits_of_shape_op_of_has_limits_of_shape [has_limits_of_shape Jᵒᵖ C] :
+instance has_colimits_of_shape_op_of_has_limits_of_shape [has_limits_of_shape Jᵒᵖ C] :
   has_colimits_of_shape J Cᵒᵖ :=
 { has_colimit := λ F, has_colimit_of_has_limit_left_op F }
 
-local attribute [instance] has_colimits_of_shape_op_of_has_limits_of_shape
+lemma has_colimits_of_shape_of_has_limits_of_shape_op [has_limits_of_shape Jᵒᵖ Cᵒᵖ] :
+  has_colimits_of_shape J C :=
+{ has_colimit := λ F, has_colimit_of_has_limit_op F }
 
 /--
 If `C` has limits, we can construct colimits for `Cᵒᵖ`.
 -/
 instance has_colimits_op_of_has_limits [has_limits C] : has_colimits Cᵒᵖ := ⟨infer_instance⟩
 
-variables (X : Type v₁)
+lemma has_colimits_of_has_limits_op [has_limits Cᵒᵖ] : has_colimits C :=
+{ has_colimits_of_shape := λ J hJ, by exactI has_colimits_of_shape_of_has_limits_of_shape_op }
+
+instance has_filtered_colimits_op_of_has_cofiltered_limits
+  [has_cofiltered_limits_of_size.{v₂ u₂} C] : has_filtered_colimits_of_size.{v₂ u₂} Cᵒᵖ :=
+{ has_colimits_of_shape := λ I hI₁ hI₂, by exactI infer_instance }
+
+lemma has_filtered_colimits_of_has_cofiltered_limits_op
+  [has_cofiltered_limits_of_size.{v₂ u₂} Cᵒᵖ] : has_filtered_colimits_of_size.{v₂ u₂} C :=
+{ has_colimits_of_shape := λ I hI₁ hI₂, by exactI has_colimits_of_shape_of_has_limits_of_shape_op }
+
+variables (X : Type v₂)
 /--
 If `C` has products indexed by `X`, then `Cᵒᵖ` has coproducts indexed by `X`.
 -/
-instance has_coproducts_opposite [has_products_of_shape X C] :
+instance has_coproducts_of_shape_opposite [has_products_of_shape X C] :
   has_coproducts_of_shape X Cᵒᵖ :=
 begin
   haveI : has_limits_of_shape (discrete X)ᵒᵖ C :=
     has_limits_of_shape_of_equivalence (discrete.opposite X).symm,
   apply_instance
 end
 
+lemma has_coproducts_of_shape_of_opposite [has_products_of_shape X Cᵒᵖ] :
+  has_coproducts_of_shape X C :=
+begin
+  haveI : has_limits_of_shape (discrete X)ᵒᵖ Cᵒᵖ :=
+    has_limits_of_shape_of_equivalence (discrete.opposite X).symm,
+  exact has_colimits_of_shape_of_has_limits_of_shape_op
+end
+
 /--
 If `C` has coproducts indexed by `X`, then `Cᵒᵖ` has products indexed by `X`.
 -/
-instance has_products_opposite [has_coproducts_of_shape X C] :
+instance has_products_of_shape_opposite [has_coproducts_of_shape X C] :
   has_products_of_shape X Cᵒᵖ :=
 begin
   haveI : has_colimits_of_shape (discrete X)ᵒᵖ C :=
     has_colimits_of_shape_of_equivalence (discrete.opposite X).symm,
   apply_instance
 end
 
+lemma has_products_of_shape_of_opposite [has_coproducts_of_shape X Cᵒᵖ] :
+  has_products_of_shape X C :=
+begin
+  haveI : has_colimits_of_shape (discrete X)ᵒᵖ Cᵒᵖ :=
+    has_colimits_of_shape_of_equivalence (discrete.opposite X).symm,
+  exact has_limits_of_shape_of_has_colimits_of_shape_op
+end
+
+instance has_products_opposite [has_coproducts.{v₂} C] : has_products.{v₂} Cᵒᵖ :=
+λ X, infer_instance
+
+lemma has_products_of_opposite [has_coproducts.{v₂} Cᵒᵖ] : has_products.{v₂} C :=
+λ X, has_products_of_shape_of_opposite X
+
+instance has_coproducts_opposite [has_products.{v₂} C] : has_coproducts.{v₂} Cᵒᵖ :=
+λ X, infer_instance
+
+lemma has_coproducts_of_opposite [has_products.{v₂} Cᵒᵖ] : has_coproducts.{v₂} C :=
+λ X, has_coproducts_of_shape_of_opposite X
+
 instance has_finite_coproducts_opposite [has_finite_products C] : has_finite_coproducts Cᵒᵖ :=
-{ out := λ J 𝒟, begin
-    resetI,
-    haveI : has_limits_of_shape (discrete J)ᵒᵖ C :=
-      has_limits_of_shape_of_equivalence (discrete.opposite J).symm,
-    apply_instance,
-  end }
+{ out := λ J _, by exactI infer_instance }
+
+lemma has_finite_coproducts_of_opposite [has_finite_products Cᵒᵖ] : has_finite_coproducts C :=
+{ out := λ J _, by exactI has_coproducts_of_shape_of_opposite J }
 
 instance has_finite_products_opposite [has_finite_coproducts C] : has_finite_products Cᵒᵖ :=
-{ out := λ J 𝒟, begin
-    resetI,
-    haveI : has_colimits_of_shape (discrete J)ᵒᵖ C :=
-      has_colimits_of_shape_of_equivalence (discrete.opposite J).symm,
-    apply_instance,
-  end }
+{ out := λ J _, by exactI infer_instance }
+
+lemma has_finite_products_of_opposite [has_finite_coproducts Cᵒᵖ] : has_finite_products C :=
+{ out := λ J _, by exactI has_products_of_shape_of_opposite J }
 
 instance has_equalizers_opposite [has_coequalizers C] : has_equalizers Cᵒᵖ :=
 begin
@@ -324,7 +387,7 @@ instance has_pushouts_opposite [has_pullbacks C] : has_pushouts Cᵒᵖ :=
 begin
   haveI : has_limits_of_shape walking_spanᵒᵖ C :=
     has_limits_of_shape_of_equivalence walking_span_op_equiv.symm,
-  apply has_colimits_of_shape_op_of_has_limits_of_shape,
+  apply_instance
 end
 
 /-- The canonical isomorphism relating `span f.op g.op` and `(cospan f g).op` -/