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

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 analysis.topology.topological_space
 import analysis.topology.continuity
@@ -27,6 +29,57 @@ 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) :=
+{ lift := λ s,
+    ⟨limit.lift (F ⋙ forget) (forget.map_cone s),
+     continuous_iff_le_coinduced.mpr $ lattice.supr_le $ λ j,
+       induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.π.app j).property⟩,
+  fac' := λ s j, subtype.eq rfl,
+  uniq' := λ s m w, subtype.eq $ (limit.is_limit (F ⋙ forget)).uniq'
+    (forget.map_cone s) m (λ j, subtype.ext.mp (w j)) }
+
+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) :=
+{ desc := λ s,
+    ⟨colimit.desc (F ⋙ forget) (forget.map_cocone s),
+     continuous_iff_induced_le.mpr $ lattice.le_infi $ λ j,
+       induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.ι.app j).property⟩,
+  fac' := λ s j, subtype.eq rfl,
+  uniq' := λ s m w, subtype.eq $ (colimit.is_colimit (F ⋙ forget)).uniq'
+    (forget.map_cocone s) m (λ j, subtype.ext.mp (w j)) }
+
+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/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