From 8b1fd0f4dffc46e27d13c13d1970f8487cc5007a Mon Sep 17 00:00:00 2001
From: hoteluser <hoteluser@room-835.local>
Date: Sat, 1 Sep 2018 22:53:40 +0200
Subject: [PATCH] (co)limits in Type u; small & filtered categories

---
 src/category_theory/small.lean           | 24 +++++++++++++++++++++++
 src/category_theory/universal/types.lean | 33 ++++++++++++++++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 src/category_theory/small.lean

diff --git a/src/category_theory/small.lean b/src/category_theory/small.lean
new file mode 100644
index 0000000..3d29256
--- /dev/null
+++ b/src/category_theory/small.lean
@@ -0,0 +1,24 @@
+/- Categories which are small relative to a cardinal κ.
+   κ-filtered categories.
+   Normally we care about these concepts for categories which are
+   used to index (co)limits, so we work with small_categories. -/
+
+import category_theory.category
+import category_theory.functor
+import category_theory.universal.colimits -- for cocone
+import set_theory.cardinal
+
+universe u
+
+namespace category_theory
+
+variables (κ : cardinal.{u})
+
+def is_kappa_small (I : Type u) [small_category.{u} I] : Prop :=
+cardinal.mk (Σ (a b : I), a ⟶ b) < κ
+
+structure kappa_filtered (C : Type u) [small_category.{u} C] : Prop :=
+(has_cocones : ∀ (I : Type u) [small_category.{u} I] (hI : is_kappa_small κ I) (F : I ↝ C),
+  nonempty (universal.cocone F))
+
+end category_theory
diff --git a/src/category_theory/universal/types.lean b/src/category_theory/universal/types.lean
index ba8791d..db84ecd 100644
--- a/src/category_theory/universal/types.lean
+++ b/src/category_theory/universal/types.lean
@@ -1,3 +1,4 @@
+import category_theory.functor
 import .limits
 import .colimits

@@ -43,6 +44,38 @@ instance : has_coequalizers.{u+1 u} (Type u) :=
     end,
   is_coequalizer := sorry }

+namespace types
+open category_theory
+
+variables {J : Type u} [𝒥 : small_category J]
+include 𝒥
+
+def limit (F : J ↝ Type u) : cone F :=
+{ X := {u : Π j, F j // ∀ (j j' : J) (f : j ⟶ j'), F.map f (u j) = u j'},
+  π := λ j u, u.val j }
+
+def limit_is_limit (F : J ↝ Type u) : is_limit (limit F) :=
+{ lift := λ s v, ⟨λ j, s.π j v, λ j j' f, congr_fun (s.w f) _⟩ }
+
+instance : has_limits.{u+1 u} (Type u) :=
+{ limit := @limit, is_limit := @limit_is_limit }
+
+def colimit (F : J ↝ Type u) : cocone F :=
+{ X := @quot (Σ j, F j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2),
+  ι := λ j x, quot.mk _ ⟨j, x⟩,
+  w := λ j j' f, funext $ λ x, eq.symm (quot.sound ⟨f, rfl⟩) }
+
+local attribute [elab_with_expected_type] quot.lift
+def colimit_is_colimit (F : J ↝ Type u) : is_colimit (colimit F) :=
+{ desc := λ s, quot.lift (λ (p : Σ j, F j), s.ι p.1 p.2)
+    (assume ⟨j, x⟩ ⟨j', x'⟩ ⟨f, hf⟩,
+      by rw hf; exact (congr_fun (s.w f) x).symm) }
+
+instance : has_colimits.{u+1 u} (Type u) :=
+{ colimit := @colimit, is_colimit := @colimit_is_colimit }
+
+end types
+
 end category_theory.universal


--
2.5.4 (Apple Git-61)