feat(category_theory/limit): limits and colimits

algebra/pi_instances.lean

@@ -11,7 +11,7 @@ import data.finset
 import tactic.pi_instances
 
 namespace pi
-universes u v
+universes u v w
 variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equiped with instances
 variables (x y : Π i, f i) (i : I)
@@ -106,6 +106,21 @@ lemma finset_prod_apply {α : Type*} {β γ} [comm_monoid β] (a : α) (s : fins
 show (s.val.map g).prod a = (s.val.map (λc, g c a)).prod,
   by rw [multiset_prod_apply, multiset.map_map]
 
+def is_ring_hom_pi
+  {α : Type u} {β : α → Type v} [R : Π a : α, ring (β a)]
+  {γ : Type w} [ring γ]
+  (f : Π a : α, γ → β a) [Rh : Π a : α, is_ring_hom (f a)] :
+  is_ring_hom (λ x b, f b x) :=
+begin
+  dsimp at *,
+  split,
+  -- It's a pity that these can't be done using `simp` lemmas.
+  { ext, rw [is_ring_hom.map_one (f x)], refl, },
+  { intros x y, ext1 z, rw [is_ring_hom.map_mul (f z)], refl, },
+  { intros x y, ext1 z, rw [is_ring_hom.map_add (f z)], refl, }
+end
+
+
 end pi
 
 namespace prod

category_theory/category.lean

@@ -24,8 +24,9 @@ namespace category_theory
 universes u v
 
 /-
-The propositional fields of `category` are annotated with the auto_param `obviously`, which is
-defined here as a [`replacer` tactic](https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#def_replacer).
+The propositional fields of `category` are annotated with the auto_param `obviously`,
+which is defined here as a
+[`replacer` tactic](https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#def_replacer).
 We then immediately set up `obviously` to call `tidy`. Later, this can be replaced with more
 powerful tactics.
 -/
@@ -43,36 +44,49 @@ class category (obj : Type u) : Type (max u (v+1)) :=
 (comp     : Π {X Y Z : obj}, hom X Y → hom Y Z → hom X Z)
 (id_comp' : ∀ {X Y : obj} (f : hom X Y), comp (id X) f = f . obviously)
 (comp_id' : ∀ {X Y : obj} (f : hom X Y), comp f (id Y) = f . obviously)
-(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z), comp (comp f g) h = comp f (comp g h) . obviously)
+(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
+  comp (comp f g) h = comp f (comp g h) . obviously)
 
 notation `𝟙` := category.id -- type as \b1
 infixr ` ≫ `:80 := category.comp -- type as \gg
 infixr ` ⟶ `:10 := category.hom -- type as \h
 
--- `restate_axiom` is a command that creates a lemma from a structure field, discarding any auto_param wrappers from the type.
+-- `restate_axiom` is a command that creates a lemma from a structure field,
+-- discarding any auto_param wrappers from the type.
 -- (It removes a backtick from the name, if it finds one, and otherwise adds "_lemma".)
 restate_axiom category.id_comp'
 restate_axiom category.comp_id'
 restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
 
 /--
-A `large_category` has objects in one universe level higher than the universe level of the morphisms.
-It is useful for examples such as the category of types, or the category of groups, etc.
+A `large_category` has objects in one universe level higher than the universe level of
+the morphisms. It is useful for examples such as the category of types, or the category
+of groups, etc.
 -/
 abbreviation large_category (C : Type (u+1)) : Type (u+1) := category.{u+1 u} C
 /--
 A `small_category` has objects and morphisms in the same universe level.
 -/
 abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C
 
+instance pempty_category : small_category pempty :=
+{ hom  := λ X Y, pempty,
+  id   := by obviously,
+  comp := by obviously }
+
+instance punit_category : small_category punit :=
+{ hom  := λ X Y, punit,
+  id   := by obviously,
+  comp := by obviously }
+
 structure bundled (c : Type u → Type v) :=
 (α : Type u)
 [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
 
@@ -82,7 +96,8 @@ In a typical example, `c` is the type class `topological_space` and `hom` is `co
 structure concrete_category {c : Type u → Type v}
   (hom : out_param $ ∀{α β : Type u}, c α → c β → (α → β) → Prop) :=
 (hom_id : ∀{α} (ia : c α), hom ia ia id)
-(hom_comp : ∀{α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g}, hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
+(hom_comp : ∀{α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g},
+  hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
 attribute [class] concrete_category
 
 instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
@@ -91,16 +106,24 @@ instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (
   id    := λa, ⟨@id a.1, h.hom_id a.2⟩,
   comp  := λa b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ }
 
-@[simp] lemma concrete_category_id {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
+@[simp] lemma concrete_category_id
+  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
   [h : concrete_category @hom] (X : bundled c) : subtype.val (𝟙 X) = id := rfl
-@[simp] lemma concrete_category_comp {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] {X Y Z : bundled c} (f : X ⟶ Y) (g : Y ⟶ Z): subtype.val (f ≫ g) = g.val ∘ f.val := rfl
+@[simp] lemma concrete_category_comp
+  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
+  [h : concrete_category @hom] {X Y Z : bundled c} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  subtype.val (f ≫ g) = g.val ∘ f.val := rfl
 
 instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
   [h : concrete_category @hom] {R S : bundled c} : has_coe_to_fun (R ⟶ S) :=
 { F := λ f, R → S,
   coe := λ f, f.1 }
 
+@[simp] lemma bundled_hom_coe
+  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
+  [h : concrete_category @hom] {R S : bundled c} (val : R → S) (prop) (r : R) :
+  (⟨val, prop⟩ : R ⟶ S) r = val r := rfl
+
 section
 variables {C : Type u} [𝒞 : category.{u v} C] {X Y Z : C}
 include 𝒞
@@ -125,7 +148,7 @@ universe u'
 instance ulift_category : category.{(max u u') v} (ulift.{u'} C) :=
 { hom  := λ X Y, (X.down ⟶ Y.down),
   id   := λ X, 𝟙 X.down,
-  comp := λ _ _ _ f g, f ≫ g }  
+  comp := λ _ _ _ f g, f ≫ g }
 
 -- We verify that this previous instance can lift small categories to large categories.
 example (D : Type u) [small_category D] : large_category (ulift.{u+1} D) := by apply_instance

category_theory/commas.lean

@@ -0,0 +1,60 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.types
+import category_theory.isomorphism
+import category_theory.whiskering
+
+namespace category_theory
+
+universes u₁ v₁ u₂ v₂ u₃ v₃
+variables {A : Type u₁} [𝒜 : category.{u₁ v₁} A]
+variables {B : Type u₂} [ℬ : category.{u₂ v₂} B]
+variables {T : Type u₃} [𝒯 : category.{u₃ v₃} T]
+include 𝒜 ℬ 𝒯
+
+structure comma (L : A ⥤ T) (R : B ⥤ T) :=
+(left : A . obviously)
+(right : B . obviously)
+(hom : L.obj left ⟶ R.obj right)
+
+variables {L : A ⥤ T} {R : B ⥤ T}
+
+structure comma_morphism (X Y : comma L R) :=
+(left : X.left ⟶ Y.left . obviously)
+(right : X.right ⟶ Y.right . obviously)
+(w' : L.map left ≫ Y.hom = X.hom ≫ R.map right . obviously)
+
+restate_axiom comma_morphism.w'
+
+namespace comma_morphism
+@[extensionality] lemma ext
+  {X Y : comma L R} {f g : comma_morphism X Y}
+  (l : f.left = g.left) (r : f.right = g.right) : f = g :=
+begin
+  cases f, cases g,
+  congr; assumption
+end
+end comma_morphism
+
+instance comma_category : category (comma L R) :=
+{ hom := comma_morphism,
+  id := λ X,
+  { left := 𝟙 X.left,
+    right := 𝟙 X.right },
+  comp := λ X Y Z f g,
+  { left := f.left ≫ g.left,
+    right := f.right ≫ g.right,
+    w' :=
+    begin
+      rw [functor.map_comp,
+          category.assoc,
+          g.w,
+          ←category.assoc,
+          f.w,
+          functor.map_comp,
+          category.assoc],
+    end }}
+
+end category_theory

category_theory/const.lean

@@ -0,0 +1,57 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.functor_category
+import category_theory.yoneda
+
+universes u u' v
+
+open category_theory
+
+namespace category_theory.functor
+
+variables (J : Type v) [small_category J]
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+
+def const : C ⥤ (J ⥤ C) :=
+{ obj := λ X,
+  { obj := λ j, X,
+    map := λ j j' f, 𝟙 X },
+  map := λ X Y f, { app := λ j, f } }
+
+namespace const
+@[simp] lemma obj_obj (X : C) (j : J) : ((const J).obj X).obj j = X := rfl
+@[simp] lemma obj_map (X : C) {j j' : J} (f : j ⟶ j') : ((const J).obj X).map f = 𝟙 X := rfl
+@[simp] lemma map_app {X Y : C} (f : X ⟶ Y) (j : J) : ((const J).map f).app j = f := rfl
+end const
+
+variables (J) {C}
+
+section
+variables {D : Type u'} [𝒟 : category.{u' v} D]
+include 𝒟
+
+@[simp] def const_compose (X : C) (F : C ⥤ D) : 
+  (const J).obj (F.obj X) ≅ (const J).obj X ⋙ F :=
+{ hom := { app := λ _, 𝟙 _ },
+  inv := { app := λ _, 𝟙 _ } }
+
+@[simp] lemma const_compose_symm_app (X : C) (F : C ⥤ D) (j : J) :
+  (const_compose J X F).inv.app j = 𝟙 _ := rfl
+
+end
+
+variables {J C}
+
+/--
+`F.cones` is the functor assigning to an object `X` the type of
+natural transformations from the constant functor with value `X` to `F`.
+
+`cone F` is equivalent, in the obvious way, to `Σ X, F.cones X`.
+-/
+def cones (F : J ⥤ C) : (Cᵒᵖ) ⥤ (Type v) :=
+  (const (Jᵒᵖ)) ⋙ (op_inv J C) ⋙ (yoneda.obj F)
+
+end category_theory.functor

category_theory/discrete_category.lean

@@ -0,0 +1,81 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Stephen Morgan, Scott Morrison
+
+import data.ulift
+import category_theory.natural_transformation
+import category_theory.isomorphism
+import category_theory.functor_category
+
+namespace category_theory
+
+universes u₁ v₁ u₂ v₂
+
+def discrete (α : Type u₁) := α
+
+@[extensionality] lemma plift.ext {P : Prop} (a b : plift P) : a = b :=
+begin
+  cases a, cases b, refl
+end
+
+instance discrete_category (α : Type u₁) : small_category (discrete α) :=
+{ hom  := λ X Y, ulift (plift (X = Y)),
+  id   := by obviously,
+  comp := by obviously }
+
+-- TODO this needs to wait for equivalences to arrive
+-- example : equivalence.{u₁ u₁ u₁ u₁} punit (discrete punit) := by obviously
+
+def discrete.lift {α : Type u₁} {β : Type u₂} (f : α → β) : (discrete α) ⥤ (discrete β) :=
+{ obj := f,
+  map := λ X Y g, begin cases g, cases g, cases g, exact 𝟙 (f X) end }
+
+variables (J : Type v₂) [small_category J]
+
+variables (C : Type u₂) [𝒞 : category.{u₂ v₂} C]
+include 𝒞
+
+section forget
+
+@[simp] def discrete.forget : (J ⥤ C) ⥤ (discrete J ⥤ C) :=
+{ obj := λ F,
+  { obj := F.obj,
+    map := λ X Y f, F.map (eq_to_hom f.down.down) },
+  map := λ F G α,
+  { app := α.app } }
+
+end forget
+
+@[simp] lemma discrete.functor_map_id
+  (F : discrete J ⥤ C) (j : discrete J) (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) :=
+begin
+  have h : f = 𝟙 j, cases f, cases f, ext,
+  rw h,
+  simp,
+end
+
+variables {C}
+
+namespace functor
+
+@[simp] def of_function {I : Type u₁} (F : I → C) : (discrete I) ⥤ C :=
+{ obj := F,
+  map := λ X Y f, begin cases f, cases f, cases f, exact 𝟙 (F X) end }
+
+end functor
+
+namespace nat_trans
+
+@[simp] def of_function {I : Type u₁} {F G : I → C} (f : Π i : I, F i ⟶ G i) :
+  (functor.of_function F) ⟹ (functor.of_function G) :=
+{ app := λ i, f i,
+  naturality' := λ X Y g,
+  begin
+    cases g, cases g, cases g,
+    dsimp [functor.of_function],
+    simp,
+  end }
+
+end nat_trans
+
+end category_theory