feat(category_theory): assorted small changes from the old limits PR

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

@@ -60,6 +60,10 @@ restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
 attribute [trans] category.comp
 
+lemma category.assoc_symm {C : Type u} [category.{u v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
+  f ≫ (g ≫ h) = (f ≫ g) ≫ h :=
+by rw ←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
@@ -110,6 +114,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,63 @@
+-- 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₁) := α
+
+instance discrete_category (α : Type u₁) : small_category (discrete α) :=
+{ hom  := λ X Y, ulift (plift (X = Y)),
+  id   := by tidy,
+  comp := by tidy }
+
+variables {C : Type u₂} [𝒞 : category.{u₂ v₂} C]
+include 𝒞
+
+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
+
+namespace discrete
+omit 𝒞
+def lift {α : Type u₁} {β : Type u₂} (f : α → β) : (discrete α) ⥤ (discrete β) :=
+functor.of_function f
+
+include 𝒞
+variables (J : Type v₂)
+
+@[simp] lemma 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
+end discrete
+
+end category_theory

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

@@ -82,6 +82,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
@@ -102,4 +108,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,7 @@ include 𝒞
 @[simp] def ulift_up : C ⥤ (ulift.{u₂} C) :=
 { obj := λ X, ⟨ X ⟩,
   map := λ X Y f, f }
+
 end
 
 end functor

category_theory/functor_category.lean

@@ -14,7 +14,7 @@ variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟
 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,

category_theory/limits/cones.lean

@@ -104,6 +104,7 @@ by convert ←(c.ι.naturality f); apply comp_id
 variables {F : J ⥤ C}
 
 namespace cone
+
 @[simp] def extensions (c : cone F) : yoneda.obj c.X ⟶ F.cones :=
 { app := λ X f, ((const J).map f) ≫ c.π }
 
@@ -239,7 +240,6 @@ end cocones
 
 end limits
 
-
 namespace functor
 
 variables {D : Type u'} [category.{u' v} D]

category_theory/limits/limits.lean

@@ -1,6 +1,6 @@
 -- Copyright (c) 2018 Scott Morrison. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Scott Morrison, Reid Barton, Mario Carneiro
+-- Authors: Reid Barton, Mario Carneiro, Scott Morrison
 
 import category_theory.whiskering
 import category_theory.yoneda
@@ -100,7 +100,7 @@ h.hom_iso W ≪≫
    by convert ←(π.naturality f).symm; apply id_comp⟩,
   inv := λ p,
   { app := λ j, p.1 j,
-    naturality' := λ j j' f, begin dsimp, erw [id_comp], exact (p.2 f).symm end } }
+    naturality' := λ j j' f, begin dsimp, rw [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
@@ -202,7 +202,7 @@ h.hom_iso W ≪≫
    by convert ←(ι.naturality f); apply comp_id⟩,
   inv := λ p,
   { app := λ j, p.1 j,
-    naturality' := λ j j' f, begin dsimp, erw [comp_id], exact (p.2 f) end } }
+    naturality' := λ j j' f, begin dsimp, rw [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
@@ -301,6 +301,10 @@ def limit.hom_iso' (F : J ⥤ C) [has_limit F] (W : C) :
   (W ⟶ limit F) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
 (limit.is_limit F).hom_iso' W
 
+lemma limit.lift_extend {F : J ⥤ C} [has_limit F] (c : cone F) {X : C} (f : X ⟶ c.X) :
+  limit.lift F (c.extend f) = f ≫ limit.lift F c :=
+by obviously
+
 section pre
 variables {K : Type v} [small_category K]
 variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
@@ -499,6 +503,12 @@ def colimit.hom_iso' (F : J ⥤ C) [has_colimit F] (W : C) :
   (colimit F ⟶ W) ≅ { p : Π j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
 (colimit.is_colimit F).hom_iso' W
 
+lemma colimit.desc_extend (F : J ⥤ C) [has_colimit F] (c : cocone F) {X : C} (f : c.X ⟶ X) :
+  colimit.desc F (c.extend f) = colimit.desc F c ≫ f :=
+begin
+  ext1, simp [category.assoc_symm], refl
+end
+
 section pre
 variables {K : Type v} [small_category K]
 variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
@@ -521,8 +531,7 @@ variables (D : L ⥤ K) [has_colimit (D ⋙ E ⋙ F)]
 @[simp] lemma colimit.pre_pre : colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) :=
 begin
   ext j,
-  erw [←assoc, colimit.ι_pre, colimit.ι_pre],
-  -- Why doesn't another erw [colimit.ι_pre] work here, like it did in limit.pre_pre?
+  rw [←assoc, colimit.ι_pre, colimit.ι_pre],
   letI : has_colimit ((D ⋙ E) ⋙ F) := show has_colimit (D ⋙ E ⋙ F), by apply_instance,
   exact (colimit.ι_pre F (D ⋙ E) j).symm
 end
@@ -557,7 +566,7 @@ by ext; rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_desc, colimit.
   colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H) :=
 begin
   ext,
-  erw [←assoc, colimit.ι_post, ←H.map_comp, colimit.ι_post],
+  rw [←assoc, colimit.ι_post, ←H.map_comp, colimit.ι_post],
   exact (colimit.ι_post F (G ⋙ H) j).symm
 end
 
@@ -571,7 +580,7 @@ lemma colimit.pre_post {K : Type v} [small_category K] {D : Type u'} [category.{
   colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G :=
 begin
   ext,
-  erw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_pre, ←assoc],
+  rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_pre, ←assoc],
   letI : has_colimit (E ⋙ F ⋙ G) := show has_colimit ((E ⋙ F) ⋙ G), by apply_instance,
   erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
 end

category_theory/opposites.lean

@@ -30,6 +30,7 @@ def op_op : (Cᵒᵖ)ᵒᵖ ⥤ C :=
 namespace functor
 
 section
+
 variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒟
 

category_theory/pempty.lean

@@ -17,7 +17,7 @@ namespace functor
 variables (C : Type u) [𝒞 : category.{u v} C]
 include 𝒞
 
-def empty : pempty ⥤ C := by obviously
+def empty : pempty ⥤ C := by tidy
 
 end functor
 

category_theory/punit.lean

@@ -13,20 +13,4 @@ instance punit_category : small_category punit :=
   id   := λ _, punit.star,
   comp := λ _ _ _ _ _, punit.star }
 
-namespace functor
-variables {C : Type u} [𝒞 : category.{u v} C]
-include 𝒞
-
-/-- The constant functor. For `X : C`, `of.obj X` is the functor `punit ⥤ C`
-  that maps `punit.star` to `X`. -/
-def of : C ⥤ (punit.{w+1} ⥤ C) := const punit
-
-namespace of
-@[simp] lemma obj_obj (X : C) : (of.obj X).obj = λ _, X := rfl
-@[simp] lemma obj_map (X : C) : (of.obj X).map = λ _ _ _, 𝟙 X := rfl
-@[simp] lemma map_app {X Y : C} (f : X ⟶ Y) : (of.map f).app = λ _, f := rfl
-end of
-
-end functor
-
 end category_theory

data/ulift.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+Transport through constant families.
+-/
+
+universes u₁ u₂
+
+@[simp] lemma plift.rec.constant {α : Sort u₁} {β : Sort u₂} (b : β) : @plift.rec α (λ _, β) (λ _, b) = λ _, b :=
+funext (λ x, plift.cases_on x (λ a, eq.refl (plift.rec (λ a', b) {down := a})))
+
+@[simp] lemma ulift.rec.constant {α : Type u₁} {β : Sort u₂} (b : β) : @ulift.rec α (λ _, β) (λ _, b) = λ _, b :=
+funext (λ x, ulift.cases_on x (λ a, eq.refl (ulift.rec (λ a', b) {down := a})))

tactic/ext.lean

@@ -150,6 +150,13 @@ begin
 end
 end ulift
 
+namespace plift
+@[extensionality] lemma ext {P : Prop} (a b : plift P) : a = b :=
+begin
+  cases a, cases b, refl
+end
+end plift
+
 namespace tactic
 
 meta def try_intros : ext_patt → tactic ext_patt