feat(category_theory/limit): special shapes of limits

(This is just rebasing what remains of the old limits PR, onto what has been merged into mathlib. No endorsement of the content is implied. :-)

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

@@ -71,13 +71,23 @@ 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
 
@@ -110,6 +120,11 @@ instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (
 { 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 𝒞

category_theory/discrete_category.lean

@@ -0,0 +1,77 @@
+-- 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 plift_subsingleton (P : Prop) : subsingleton (plift P) :=
+subsingleton.intro (λ 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 𝒞
+
+@[simp] def discrete.forget : discrete J ⥤ J :=
+{ obj := λ X, X,
+  map := λ X Y f, eq_to_hom f.down.down }
+
+@[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

category_theory/examples/CommRing/products.lean

@@ -0,0 +1,32 @@
+import algebra.pi_instances
+import category_theory.examples.rings
+import category_theory.limits
+
+universes u v w
+
+namespace category_theory.examples
+
+open category_theory
+open category_theory.limits
+
+def CommRing.pi {β : Type u} (f : β → CommRing.{u}) : CommRing :=
+{ α := Π b : β, (f b), str := by apply_instance }
+
+def CommRing.pi_π {β : Type u} (f : β → CommRing) (b : β): CommRing.pi f ⟶ f b :=
+{ val := λ g, g b, property := by tidy }
+
+@[simp] def CommRing.hom_pi
+  {α : Type u} {β : α → CommRing} {γ : CommRing}
+  (f : Π a : α, γ ⟶ β a) : γ ⟶ CommRing.pi β :=
+{ val := λ x b, f b x,
+  property := begin convert pi.is_ring_hom_pi (λ a, (f a).val) end }
+
+local attribute [extensionality] subtype.eq
+
+instance CommRing_has_products : has_products.{v+1 v} CommRing :=
+{ fan := λ β f, { X := CommRing.pi f,
+                  π := { app := CommRing.pi_π f } },
+  is_product := λ β f, { lift := λ s, CommRing.hom_pi (λ j, s.π.app j),
+                         uniq' := begin tidy, rw ←w, tidy, end } }.
+
+end category_theory.examples

category_theory/examples/Top/products.lean

@@ -0,0 +1,30 @@
+import category_theory.examples.topological_spaces
+import category_theory.limits.products
+import analysis.topology.continuity
+
+universes u v w
+
+open category_theory.limits
+open category_theory.examples
+
+def Top.pi {β : Type u} (f : β → Top.{u}) : Top :=
+{ α := Π b : β, (f b), str := by apply_instance }
+
+def Top.pi_π {β : Type u} (f : β → Top) (b : β): Top.pi f ⟶ f b :=
+{ val := λ g, g b, property := continuous_apply _ }
+
+@[simp] def Top.hom_pi
+  {α : Type u} {β : α → Top} {γ : Top}
+  (f : Π a : α, γ ⟶ β a) : γ ⟶ Top.pi β :=
+{ val := λ x b, f b x,
+  property := continuous_pi (λ a, (f a).property) }
+
+local attribute [extensionality] subtype.eq
+
+instance : has_products.{u+1 u} Top :=
+{ fan := λ β f,
+  { X := Top.pi f,
+    π := { app := Top.pi_π f } },
+  is_product := λ β f,
+  { lift := λ s, Top.hom_pi (λ j, s.π.app j),
+    uniq' := λ s m w, begin tidy, rw ←w, tidy, end } }.

category_theory/examples/rings.lean

@@ -33,21 +33,26 @@ instance Ring_hom_is_ring_hom {R S : Ring} (f : R ⟶ S) : is_ring_hom (f : R 
 
 instance (x : CommRing) : comm_ring x := x.str
 
-@[reducible] def is_comm_ring_hom {α β} [comm_ring α] [comm_ring β] (f : α → β) : Prop :=
-is_ring_hom f
+-- Here we don't use the `concrete` machinery,
+-- because it would require introducing a useless synonym for `is_ring_hom`.
+instance : category CommRing :=
+{ hom := λ R S, { f : R → S // is_ring_hom f },
+  id := λ R, ⟨ id, by resetI; apply_instance ⟩,
+  comp := λ R S T g h, ⟨ h.1 ∘ g.1, begin haveI := g.2, haveI := h.2, apply_instance end ⟩ }
 
-instance concrete_is_comm_ring_hom : concrete_category @is_comm_ring_hom :=
-⟨by introsI α ia; apply_instance,
-  by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
+instance CommRing_hom_coe {R S : CommRing} : has_coe_to_fun (R ⟶ S) :=
+{ F := λ f, R → S,
+  coe := λ f, f.1 }
+
+@[simp] lemma CommRing_hom_coe_app {R S : CommRing} (f : R ⟶ S) (r : R) : f r = f.val r := rfl
 
-instance CommRing_hom_is_comm_ring_hom {R S : CommRing} (f : R ⟶ S) : is_comm_ring_hom (f : R → S) := f.2
+instance CommRing_hom_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
 
 namespace CommRing
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
-def forget_to_CommMon : CommRing ⥤ CommMon := 
-concrete_functor
-  (by intros _ c; exact { ..c })
-  (by introsI _ _ _ _ f i;  exact { ..i })
+def forget_to_CommMon : CommRing ⥤ CommMon :=
+{ obj := λ X, { α := X.1, str := by apply_instance },
+  map := λ X Y f, ⟨ f, by apply_instance ⟩ }
 
 instance : faithful (forget_to_CommMon) := {}
 

category_theory/examples/topological_spaces.lean

@@ -36,6 +36,12 @@ instance : small_category (opens X) := by apply_instance
 def nbhd (x : X.α) := { U : opens X // x ∈ U }
 def nbhds (x : X.α) : small_category (nbhd x) := begin unfold nbhd, apply_instance end
 
+end category_theory.examples
+
+open category_theory.examples
+
+namespace topological_space.opens
+
 /-- `opens.map f` gives the functor from open sets in Y to open set in X,
     given by taking preimages under f. -/
 def map
@@ -56,4 +62,4 @@ nat_iso.of_components (λ U, eq_to_iso (congr_fun (congr_arg _ (congr_arg _ h))
 
 @[simp] def map_iso_id {X : Top.{u}} (h) : map_iso (𝟙 X) (𝟙 X) h = iso.refl (map _) := rfl
 
-end category_theory.examples
+end topological_space.opens

category_theory/functor.lean

@@ -90,6 +90,17 @@ include 𝒞
 @[simp] def ulift_up : C ⥤ (ulift.{u₂} C) :=
 { obj := λ X, ⟨ X ⟩,
   map := λ X Y f, f }
+
+def empty : pempty ⥤ C := by obviously
+
+variables {C}
+
+-- punit.{u} : Sort u, so punit.{v₂+1} is a small_category.{v₂}.
+def of_obj (X : C) : punit.{v₂+1} ⥤ C :=
+{ obj := λ Y, X,
+  map := λ Y Z f, 𝟙 X }
+
+@[simp] lemma of_obj_obj (X : C) (a : punit) : ((of_obj X).obj a) = X := rfl
 end
 
 end functor

category_theory/functor_category.lean

@@ -6,15 +6,15 @@ import category_theory.natural_transformation
 
 namespace category_theory
 
-universes u₁ v₁ u₂ v₂ u₃ v₃
+universes u v u₁ v₁ u₂ v₂ u₃ v₃
 
 open nat_trans
 
 variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
 /--
-`functor.category C D` gives the category structure on functor and natural transformations
+`functor.category C D` gives the category structure on functors and natural transformations
 between categories `C` and `D`.
 
 Notice that if `C` and `D` are both small categories at the same universe level,