feat(category_theory/examples/topological_spaces): limits and colimits (#518)

Author: rwbarton

category_theory/category.lean

@@ -73,11 +73,11 @@ abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C
 
 structure bundled (c : Type u → Type v) :=
 (α : Type u)
-[str : c α]
+(str : c α)
 
 instance (c : Type u → Type v) : has_coe_to_sort (bundled c) :=
 { S := Type u, coe := bundled.α }
- 
+
 def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c :=
 @bundled.mk c α str
 

category_theory/examples/topological_spaces.lean

@@ -4,6 +4,8 @@
 
 import category_theory.full_subcategory
 import category_theory.functor_category
+import category_theory.limits.preserves
+import category_theory.limits.types
 import category_theory.natural_isomorphism
 import category_theory.eq_to_hom
 import analysis.topology.topological_space
@@ -28,6 +30,49 @@ instance : concrete_category @continuous := ⟨@continuous_id, @continuous.comp
 
 -- local attribute [class] continuous
 -- instance {R S : Top} (f : R ⟶ S) : continuous (f : R → S) := f.2
+
+section
+open category_theory.limits
+
+variables {J : Type u} [small_category J]
+
+def limit (F : J ⥤ Top.{u}) : cone F :=
+{ X := ⟨limit (F ⋙ forget), ⨆ j, (F.obj j).str.induced (limit.π (F ⋙ forget) j)⟩,
+  π :=
+  { app := λ j, ⟨limit.π (F ⋙ forget) j, continuous_iff_induced_le.mpr (lattice.le_supr _ j)⟩,
+    naturality' := λ j j' f, subtype.eq ((limit.cone (F ⋙ forget)).π.naturality f) } }
+
+def limit_is_limit (F : J ⥤ Top.{u}) : is_limit (limit F) :=
+by refine is_limit.of_faithful forget (limit.is_limit _) (λ s, ⟨_, _⟩) (λ s, rfl);
+   exact continuous_iff_le_coinduced.mpr (lattice.supr_le $ λ j,
+     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.π.app j).property)
+
+instance : has_limits.{u+1 u} Top.{u} :=
+λ J 𝒥 F, by exactI { cone := limit F, is_limit := limit_is_limit F }
+
+instance : preserves_limits (forget : Top.{u} ⥤ Type u) :=
+λ J 𝒥 F, by exactI preserves_limit_of_preserves_limit_cone
+  (limit.is_limit F) (limit.is_limit (F ⋙ forget))
+
+def colimit (F : J ⥤ Top.{u}) : cocone F :=
+{ X := ⟨colimit (F ⋙ forget), ⨅ j, (F.obj j).str.coinduced (colimit.ι (F ⋙ forget) j)⟩,
+  ι :=
+  { app := λ j, ⟨colimit.ι (F ⋙ forget) j, continuous_iff_le_coinduced.mpr (lattice.infi_le _ j)⟩,
+    naturality' := λ j j' f, subtype.eq ((colimit.cocone (F ⋙ forget)).ι.naturality f) } }
+
+def colimit_is_colimit (F : J ⥤ Top.{u}) : is_colimit (colimit F) :=
+by refine is_colimit.of_faithful forget (colimit.is_colimit _) (λ s, ⟨_, _⟩) (λ s, rfl);
+   exact continuous_iff_induced_le.mpr (lattice.le_infi $ λ j,
+     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.ι.app j).property)
+
+instance : has_colimits.{u+1 u} Top.{u} :=
+λ J 𝒥 F, by exactI { cocone := colimit F, is_colimit := colimit_is_colimit F }
+
+instance : preserves_colimits (forget : Top.{u} ⥤ Type u) :=
+λ J 𝒥 F, by exactI preserves_colimit_of_preserves_colimit_cocone
+  (colimit.is_colimit F) (colimit.is_colimit (F ⋙ forget))
+
+end
 end Top
 
 variables {X : Top.{u}}

category_theory/limits/limits.lean

@@ -102,6 +102,21 @@ h.hom_iso W ≪≫
   { app := λ j, p.1 j,
     naturality' := λ j j' f, begin dsimp, erw [id_comp], exact (p.2 f).symm end } }
 
+/-- If G : C → D is a faithful functor which sends t to a limit cone,
+  then it suffices to check that the induced maps for the image of t
+  can be lifted to maps of C. -/
+def of_faithful {t : cone F} {D : Type u'} [category.{u' v} D] (G : C ⥤ D) [faithful G]
+  (ht : is_limit (G.map_cone t)) (lift : Π (s : cone F), s.X ⟶ t.X)
+  (h : ∀ s, G.map (lift s) = ht.lift (G.map_cone s)) : is_limit t :=
+{ lift := lift,
+  fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
+  uniq' := λ s m w, begin
+    apply G.injectivity, rw h,
+    refine ht.uniq (G.map_cone s) _ (λ j, _),
+    convert ←congr_arg (λ f, G.map f) (w j),
+    apply G.map_comp
+  end }
+
 end is_limit
 
 /-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
@@ -189,6 +204,21 @@ h.hom_iso W ≪≫
   { app := λ j, p.1 j,
     naturality' := λ j j' f, begin dsimp, erw [comp_id], exact (p.2 f) end } }
 
+/-- If G : C → D is a faithful functor which sends t to a colimit cocone,
+  then it suffices to check that the induced maps for the image of t
+  can be lifted to maps of C. -/
+def of_faithful {t : cocone F} {D : Type u'} [category.{u' v} D] (G : C ⥤ D) [faithful G]
+  (ht : is_colimit (G.map_cocone t)) (desc : Π (s : cocone F), t.X ⟶ s.X)
+  (h : ∀ s, G.map (desc s) = ht.desc (G.map_cocone s)) : is_colimit t :=
+{ desc := desc,
+  fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
+  uniq' := λ s m w, begin
+    apply G.injectivity, rw h,
+    refine ht.uniq (G.map_cocone s) _ (λ j, _),
+    convert ←congr_arg (λ f, G.map f) (w j),
+    apply G.map_comp
+  end }
+
 end is_colimit
 
 section limit

category_theory/types.lean

@@ -55,13 +55,13 @@ instance ulift_functor_faithful : fully_faithful ulift_functor :=
     congr_arg ulift.down ((congr_fun p (ulift.up x)) : ((ulift.up (f x)) = (ulift.up (g x)))) }
 
 section forget
-variables (C : Type u → Type v) {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
+variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
 include i
 
 /-- The forgetful functor from a bundled category to `Type`. -/
 def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λa b h, h.1 }
 
-instance forget.faithful : faithful (forget C) := {}
+instance forget.faithful : faithful (forget : bundled C ⥤ Type u) := {}
 
 end forget