feat(category_theory): filtered colimits of types

src/category_theory/filtered.lean

@@ -0,0 +1,21 @@
+-- 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
+
+universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+
+namespace category_theory
+
+variables (C : Sort u) [𝒞 : category.{v} C]
+include 𝒞
+
+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)
+
+class is_filtered extends is_filtered_or_empty.{v} C : Prop :=
+(nonempty : nonempty C)
+
+end category_theory

src/category_theory/limits/types.lean

@@ -3,8 +3,10 @@
 -- Authors: Scott Morrison, Reid Barton
 
 import category_theory.limits.limits
+import category_theory.filtered
+import data.quot
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes u
 
 open category_theory
 open category_theory.limits
@@ -81,4 +83,71 @@ instance : has_colimits.{u} (Type u) :=
     (λ p, c.ι.app p.1 p.2)
     (λ p p' ⟨f, h⟩, by rw h; exact (functor_to_types.naturality _ _ c.ι f _).symm) := rfl
 
+namespace filtered_colimit
+/- For filtered colimits of types, we can give an explicit description
+  of the equivalence relation generated by the relation used to form
+  the colimit.  -/
+
+variables [is_filtered_or_empty.{u+1} J]
+variables (F : J ⥤ Type u)
+
+protected def r (x y : Σ j, F.obj j) : Prop :=
+∃ k (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2
+
+protected lemma r_equiv : equivalence (filtered_colimit.r F) :=
+⟨λ x, ⟨x.1, 𝟙 x.1, 𝟙 x.1, rfl⟩,
+ λ x y ⟨k, f, g, h⟩, ⟨k, g, f, h.symm⟩,
+ λ x y z ⟨k, f, g, h⟩ ⟨k', f', g', h'⟩,
+   let ⟨l, fl, gl, _⟩ := is_filtered_or_empty.cocone_objs.{u+1} k k',
+       ⟨m, n, hn⟩ := is_filtered_or_empty.cocone_maps (g ≫ fl) (f' ≫ gl) in
+   ⟨m, f ≫ fl ≫ n, g' ≫ gl ≫ n, calc
+      F.map (f ≫ fl ≫ n) x.2
+          = F.map (fl ≫ n) (F.map f x.2)  : by simp
+      ... = F.map (fl ≫ n) (F.map g y.2)  : by rw h
+      ... = F.map ((g ≫ fl) ≫ n) y.2      : by simp
+      ... = F.map ((f' ≫ gl) ≫ n) y.2     : by rw hn
+      ... = F.map (gl ≫ n) (F.map f' y.2) : by simp
+      ... = F.map (gl ≫ n) (F.map g' z.2) : by rw h'
+      ... = F.map (g' ≫ gl ≫ n) z.2       : by simp⟩⟩
+
+protected lemma r_ge (x y : Σ j, F.obj j) :
+  (∃ f : x.1 ⟶ y.1, y.2 = F.map f x.2) → filtered_colimit.r F x y :=
+λ ⟨f, hf⟩, ⟨y.1, f, 𝟙 y.1, by simp [hf]⟩
+
+protected lemma r_eq :
+  filtered_colimit.r F = eqv_gen (λ x y, ∃ f : x.1 ⟶ y.1, y.2 = F.map f x.2) :=
+begin
+  apply le_antisymm,
+  { rintros ⟨i, x⟩ ⟨j, y⟩ ⟨k, f, g, h⟩,
+    exact eqv_gen.trans _ ⟨k, F.map f x⟩ _ (eqv_gen.rel _ _ ⟨f, rfl⟩)
+      (eqv_gen.symm _ _ (eqv_gen.rel _ _ ⟨g, h⟩)) },
+  { intros x y,
+    convert relation.eqv_gen_mono (filtered_colimit.r_ge F),
+    apply propext,
+    symmetry,
+    exact relation.eqv_gen_iff_of_equivalence (filtered_colimit.r_equiv F) }
+end
+
+lemma colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
+  colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
+begin
+  change quot.mk _ _ = quot.mk _ _ ↔ _,
+  rw [quot.eq, ←filtered_colimit.r_eq],
+  refl
+end
+
+variables {t : cocone F} (ht : is_colimit t)
+local attribute [elab_simple] nat_trans.app
+lemma is_colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
+  t.ι.app i xi = t.ι.app j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
+let t' := colimit.cocone F,
+    e : t' ≅ t := is_colimit.unique (colimit.is_colimit F) ht,
+    e' : t'.X ≅ t.X := cocones.forget.on_iso e in
+begin
+  refine iff.trans _ (colimit_eq_iff F),
+  convert equiv.apply_eq_iff_eq e'.to_equiv _ _; rw ←e.hom.w; refl
+end
+
+end filtered_colimit
+
 end category_theory.limits.types

src/data/quot.lean

@@ -46,6 +46,10 @@ quot.hrec_on₂ qa qb f
   (λ _ _ _ p, c _ _ _ _ (setoid.refl _) p)
 end quotient
 
+lemma quot.eq {α : Type*} {r : α → α → Prop} {x y : α} :
+  quot.mk r x = quot.mk r y ↔ eqv_gen r x y :=
+⟨quot.exact r, quot.eqv_gen_sound⟩
+
 @[simp] theorem quotient.eq [r : setoid α] {x y : α} : ⟦x⟧ = ⟦y⟧ ↔ x ≈ y :=
 ⟨quotient.exact, quotient.sound⟩