feat(category_theory/filtered): finite diagrams in filtered categorie…

…s admit cocones (#4026)

This is only step towards eventual results about filtered colimits commuting with finite limits, `forget CommRing` preserving filtered colimits, and applications to `Scheme`.



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

src/category_theory/filtered.lean

@@ -3,7 +3,8 @@ Copyright (c) 2019 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton
 -/
-import category_theory.category
+import category_theory.fin_category
+import category_theory.limits.cones
 import order.bounded_lattice
 
 /-!
@@ -19,7 +20,20 @@ We give a simple characterisation of this condition as
 Filtered colimits are often better behaved than arbitrary colimits.
 See `category_theory/limits/types` for some details.
 
-(We'll prove existence of cocones for finite diagrams in a subsequent PR.)
+Filtered categories are nice because colimits indexed by filtered categories tend to be
+easier to describe than general colimits (and often often preserved by functors).
+
+In this file we show that any functor from a finite category to a filtered category admits a cocone:
+* `cocone_nonempty [fin_category J] [is_filtered C] (F : J ⥤ C) : nonempty (cocone F)`
+More generally,
+for any finite collection of objects and morphisms between them in a filtered category
+(even if not closed under composition) there exists some object `Z` receiving maps from all of them,
+so that all the triangles (one edge from the finite set, two from morphisms to `Z`) commute.
+This formulation is often more useful in practice. We give two variants,
+`sup_exists'`, which takes a single finset of objects, and a finset of morphisms
+(bundled with their sources and targets), and
+`sup_exists`, which takes a finset of objects, and an indexed family (indexed by source and target)
+of finsets of morphisms.
 
 ## Future work
 * Finite limits commute with filtered colimits
@@ -42,7 +56,6 @@ class is_filtered_or_empty : Prop :=
 (cocone_objs : ∀ (X Y : C), ∃ Z (f : X ⟶ Z) (g : Y ⟶ Z), true)
 (cocone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ Z (h : Y ⟶ Z), f ≫ h = g ≫ h)
 
-
 section prio
 set_option default_priority 100 -- see Note [default priority]
 
@@ -70,4 +83,182 @@ instance is_filtered_of_semilattice_sup_top
 { nonempty := ⟨⊤⟩,
   ..category_theory.is_filtered_or_empty_of_semilattice_sup α }
 
+namespace is_filtered
+
+variables {C} [is_filtered C]
+
+/--
+`max j j'` is an arbitrary choice of object to the right of both `j` and `j'`,
+whose existence is ensured by `is_filtered`.
+-/
+noncomputable def max (j j' : C) : C :=
+(is_filtered_or_empty.cocone_objs j j').some
+
+/--
+`left_to_max j j'` is an arbitrarily choice of morphism from `j` to `max j j'`,
+whose existence is ensured by `is_filtered`.
+-/
+noncomputable def left_to_max (j j' : C) : j ⟶ max j j' :=
+(is_filtered_or_empty.cocone_objs j j').some_spec.some
+
+/--
+`right_to_max j j'` is an arbitrarily choice of morphism from `j'` to `max j j'`,
+whose existence is ensured by `is_filtered`.
+-/
+noncomputable def right_to_max (j j' : C) : j' ⟶ max j j' :=
+(is_filtered_or_empty.cocone_objs j j').some_spec.some_spec.some
+
+/--
+`coeq f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of object
+which admits a morphism `coeq_hom f f' : j' ⟶ coeq f f'` such that
+`coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
+Its existence is ensured by `is_filtered`.
+-/
+noncomputable def coeq {j j' : C} (f f' : j ⟶ j') : C :=
+(is_filtered_or_empty.cocone_maps f f').some
+
+/--
+`coeq_hom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
+`coeq_hom f f' : j' ⟶ coeq f f'` such that
+`coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
+Its existence is ensured by `is_filtered`.
+-/
+noncomputable def coeq_hom {j j' : C} (f f' : j ⟶ j') : j' ⟶ coeq f f' :=
+(is_filtered_or_empty.cocone_maps f f').some_spec.some
+
+/--
+`coeq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
+`f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
+-/
+lemma coeq_condition {j j' : C} (f f' : j ⟶ j') : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f' :=
+(is_filtered_or_empty.cocone_maps f f').some_spec.some_spec
+
+open category_theory.limits
+
+/--
+Any finite collection of objects in a filtered category has an object "to the right".
+-/
+lemma sup_objs_exists (O : finset C) : ∃ (S : C), ∀ {X}, X ∈ O → _root_.nonempty (X ⟶ S) :=
+begin
+  classical,
+  apply finset.induction_on O,
+  { exact ⟨is_filtered.nonempty.some, (by rintros - ⟨⟩)⟩, },
+  { rintros X O' nm ⟨S', w'⟩,
+    use max X S',
+    rintros Y mY,
+    by_cases h : X = Y,
+    { subst h, exact ⟨left_to_max _ _⟩, },
+    { exact ⟨(w' (by finish)).some ≫ right_to_max _ _⟩, }, }
+end
+
+/--
+An alternative formulation of `sup_exists`, using a single `finset` of morphisms,
+rather than a family indexed by the sources and targets.
+
+Given any `finset` of objects `{X, ...}` and
+indexed collection of `finset`s of morphisms `{f, ...}` in `C`,
+there is an object `S`, with a morphism `T X : X ⟶ S` from each `X`,
+such that the triangles commute: `f ≫ T X = T Y`, for `f : X ⟶ Y` in the `finset`.
+-/
+lemma sup_exists' (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) :
+  ∃ (S : C) (T : Π {X : C}, X ∈ O → (X ⟶ S)), ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
+    (⟨X, Y, mX, mY, f⟩ : (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) ∈ H → f ≫ T mY = T mX :=
+begin
+  classical,
+  apply finset.induction_on H,
+  { obtain ⟨S, f⟩ := sup_objs_exists O,
+    refine ⟨S, λ X mX, (f mX).some, _⟩,
+    rintros - - - - - ⟨⟩, },
+  { rintros ⟨X, Y, mX, mY, f⟩ H' nmf ⟨S', T', w'⟩,
+    refine ⟨coeq (f ≫ T' mY) (T' mX), λ Z mZ, T' mZ ≫ coeq_hom (f ≫ T' mY) (T' mX), _⟩,
+    intros X' Y' mX' mY' f' mf',
+    rw [←category.assoc],
+    by_cases h : X = X' ∧ Y = Y',
+    { rcases h with ⟨rfl, rfl⟩,
+      by_cases hf : f = f',
+      { subst hf,
+        apply coeq_condition, },
+      { rw w' _ _ (by finish), }, },
+    { rw w' _ _ (by finish), }, },
+end
+
+/--
+Given any `finset` of objects `{X, ...}` and
+indexed collection of `finset`s of morphisms `{f, ...}` in `C`,
+there is an object `S`, with a morphism `T X : X ⟶ S` from each `X`,
+such that the triangles commute: `f ≫ T X = T Y`, for `f : X ⟶ Y` in the `finset`.
+-/
+lemma sup_exists (O : finset C) (H : Π X Y, X ∈ O → Y ∈ O → finset (X ⟶ Y)) :
+  ∃ (S : C) (T : Π {X : C}, X ∈ O → (X ⟶ S)), ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
+    f ∈ H _ _ mX mY → f ≫ T mY = T mX :=
+begin
+  classical,
+  let H' : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y) :=
+    O.attach.bind (λ X : { X // X ∈ O }, O.attach.bind (λ Y : { Y // Y ∈ O },
+      (H X.1 Y.1 X.2 Y.2).image (λ f, ⟨X.1, Y.1, X.2, Y.2, f⟩))),
+  obtain ⟨S, T, w⟩ := sup_exists' O H',
+  refine ⟨S, @T, _⟩,
+  intros X Y mX mY f mf,
+  apply w,
+  simp only [finset.mem_attach, exists_prop, finset.mem_bind, exists_prop_of_true, finset.mem_image,
+    subtype.exists, subtype.coe_mk, subtype.val_eq_coe],
+  refine ⟨X, mX, Y, mY, f, mf, rfl, (by simp)⟩,
+end
+
+/--
+An arbitrary choice of object "to the right" of a finite collection of objects `O` and morphisms `H`,
+making all the triangles commute.
+-/
+noncomputable
+def sup (O : finset C) (H : Π X Y, X ∈ O → Y ∈ O → finset (X ⟶ Y)) : C :=
+(sup_exists O H).some
+
+/--
+The morphisms to `sup O H`.
+-/
+noncomputable
+def to_sup (O : finset C) (H : Π X Y, X ∈ O → Y ∈ O → finset (X ⟶ Y)) {X : C} (m : X ∈ O) :
+  X ⟶ sup O H :=
+(sup_exists O H).some_spec.some m
+
+/--
+The triangles of consisting of a morphism in `H` and the maps to `sup O H` commute.
+-/
+lemma to_sup_commutes (O : finset C) (H : Π X Y, X ∈ O → Y ∈ O → finset (X ⟶ Y))
+  {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y} (mf : f ∈ H _ _ mX mY) :
+  f ≫ to_sup O H mY = to_sup O H mX :=
+(sup_exists O H).some_spec.some_spec mX mY mf
+
+variables {J : Type v} [small_category J] [fin_category J]
+
+/--
+If we have `is_filtered C`, then for any functor `F : J ⥤ C` with `fin_category J`,
+there exists a cocone over `F`.
+-/
+lemma cocone_nonempty (F : J ⥤ C) : _root_.nonempty (cocone F) :=
+begin
+  classical,
+  let O := (finset.univ.image F.obj),
+  let H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y) :=
+    finset.univ.bind (λ X : J, finset.univ.bind (λ Y : J, finset.univ.image (λ f : X ⟶ Y,
+      ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩))),
+  obtain ⟨Z, f, w⟩ := sup_exists' O H,
+  refine ⟨⟨Z, ⟨λ X, f (by simp), _⟩⟩⟩,
+  intros j j' g,
+  dsimp,
+  simp only [category.comp_id],
+  apply w,
+  simp only [finset.mem_univ, finset.mem_bind, exists_and_distrib_left,
+    exists_prop_of_true, finset.mem_image],
+  exact ⟨j, rfl, j', g, (by simp)⟩,
+end
+
+/--
+An arbitrarily chosen cocone over `F : J ⥤ C`, for `fin_category J` and `is_filtered C`.
+-/
+noncomputable def cocone (F : J ⥤ C) : cocone F :=
+(cocone_nonempty F).some
+
+end is_filtered
+
 end category_theory

src/category_theory/fin_category.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import data.fintype.basic
+import category_theory.discrete_category
+
+universes v u
+
+namespace category_theory
+
+instance discrete_fintype {α : Type*} [fintype α] : fintype (discrete α) :=
+by { dsimp [discrete], apply_instance }
+
+instance discrete_hom_fintype {α : Type*} [decidable_eq α] (X Y : discrete α) : fintype (X ⟶ Y) :=
+by { apply ulift.fintype }
+
+/-- A category with a `fintype` of objects, and a `fintype` for each morphism space. -/
+class fin_category (J : Type v) [small_category J] :=
+(decidable_eq_obj : decidable_eq J . tactic.apply_instance)
+(fintype_obj : fintype J . tactic.apply_instance)
+(decidable_eq_hom : Π (j j' : J), decidable_eq (j ⟶ j') . tactic.apply_instance)
+(fintype_hom : Π (j j' : J), fintype (j ⟶ j') . tactic.apply_instance)
+
+attribute [instance] fin_category.decidable_eq_obj fin_category.fintype_obj
+                     fin_category.decidable_eq_hom fin_category.fintype_hom
+
+-- We need a `decidable_eq` instance here to construct `fintype` on the morphism spaces.
+instance fin_category_discrete_of_decidable_fintype (J : Type v) [decidable_eq J] [fintype J] :
+  fin_category (discrete J) :=
+{ }
+
+end category_theory

src/category_theory/limits/shapes/finite_limits.lean

@@ -4,37 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.fintype.basic
+import category_theory.fin_category
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.equalizers
 import category_theory.limits.shapes.pullbacks
 
 universes v u
 
-namespace category_theory
-
-instance discrete_fintype {α : Type*} [fintype α] : fintype (discrete α) :=
-by { dsimp [discrete], apply_instance }
-
-instance discrete_hom_fintype {α : Type*} [decidable_eq α] (X Y : discrete α) : fintype (X ⟶ Y) :=
-by { apply ulift.fintype }
-
-/-- A category with a `fintype` of objects, and a `fintype` for each morphism space. -/
-class fin_category (J : Type v) [small_category J] :=
-(decidable_eq_obj : decidable_eq J . tactic.apply_instance)
-(fintype_obj : fintype J . tactic.apply_instance)
-(decidable_eq_hom : Π (j j' : J), decidable_eq (j ⟶ j') . tactic.apply_instance)
-(fintype_hom : Π (j j' : J), fintype (j ⟶ j') . tactic.apply_instance)
-
-attribute [instance] fin_category.decidable_eq_obj fin_category.fintype_obj
-                     fin_category.decidable_eq_hom fin_category.fintype_hom
-
--- We need a `decidable_eq` instance here to construct `fintype` on the morphism spaces.
-instance fin_category_discrete_of_decidable_fintype (J : Type v) [decidable_eq J] [fintype J] :
-  fin_category (discrete J) :=
-{ }
-
-end category_theory
-
 open category_theory
 
 namespace category_theory.limits

src/logic/basic.lean

@@ -723,14 +723,20 @@ by simp [and_comm]
 
 @[simp] theorem exists_eq {a' : α} : ∃ a, a = a' := ⟨_, rfl⟩
 
-@[simp] theorem exists_eq' {a' : α} : Exists (eq a') := ⟨_, rfl⟩
+@[simp] theorem exists_eq' {a' : α} : ∃ a, a' = a := ⟨_, rfl⟩
 
 @[simp] theorem exists_eq_left {a' : α} : (∃ a, a = a' ∧ p a) ↔ p a' :=
 ⟨λ ⟨a, e, h⟩, e ▸ h, λ h, ⟨_, rfl, h⟩⟩
 
 @[simp] theorem exists_eq_right {a' : α} : (∃ a, p a ∧ a = a') ↔ p a' :=
 (exists_congr $ by exact λ a, and.comm).trans exists_eq_left
 
+@[simp] theorem exists_apply_eq_apply {α β : Type*} (f : α → β) (a' : α) : ∃ a, f a = f a' :=
+⟨a', rfl⟩
+
+@[simp] theorem exists_apply_eq_apply' {α β : Type*} (f : α → β) (a' : α) : ∃ a, f a' = f a :=
+⟨a', rfl⟩
+
 @[simp] theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} :
   (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a) :=
 ⟨λ ⟨b, ⟨a, ha, hab⟩, hb⟩, ⟨a, ha, hab.symm ▸ hb⟩, λ ⟨a, hp, hq⟩, ⟨f a, ⟨a, hp, rfl⟩, hq⟩⟩