feat(category_theory/limits): special shapes (#1339)

* providing minimal API for limits of special shapes

* apis for special shapes

* fintype instances

* associators, unitors, braidings for binary product

* map

* instances

* assoc lemma

* coprod

* fix import

* names

* adding some docs

* updating tutorial on limits

* minor

* uniqueness of morphisms to terminal object

* better treatment of has_terminal

* various

* not there yet

* deleting a dumb file

* remove constructions for a later PR

* use @[reassoc]

* Update src/category_theory/limits/shapes/finite_products.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* improving the colimits tutorial

* minor

* notation for `prod_obj` and `sigma_obj`.

* reverting to `condition`

* implicit arguments

* more implicit arguments

* minor

* notational for initial and terminal objects

* various

* fix notation priorities

* remove unused case bash tactic

* fix whitespace

* comment

* notations

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -17,40 +17,51 @@ section MappingCylinder
 -- Let's construct the mapping cylinder.
 def to_pt (X : Top) : X ⟶ pt :=
 { val := λ _, unit.star, property := continuous_const }
-def I_0 : pt ⟶ I :=
+def I₀ : pt ⟶ I :=
 { val := λ _, ⟨(0 : ℝ), begin rw [set.left_mem_Icc], norm_num, end⟩,
   property := continuous_const }
-def I_1 : pt ⟶ I :=
+def I₁ : pt ⟶ I :=
 { val := λ _, ⟨(1 : ℝ), begin rw [set.right_mem_Icc], norm_num, end⟩,
   property := continuous_const }
 
-def cylinder (X : Top) : Top := limit (pair X I)
+def cylinder (X : Top) : Top := prod X I
 -- To define a map to the cylinder, we give a map to each factor.
--- `binary_fan.mk` is a helper method for constructing a `cone` over `pair X Y`.
-def cylinder_0 (X : Top) : X ⟶ cylinder X :=
-limit.lift (pair X I) (binary_fan.mk (𝟙 X) (to_pt X ≫ I_0))
-def cylinder_1 (X : Top) : X ⟶ cylinder X :=
-limit.lift (pair X I) (binary_fan.mk (𝟙 X) (to_pt X ≫ I_1))
+-- `prod.lift` is a helper method, providing a wrapper around `limit.lift` for binary products.
+def cylinder₀ (X : Top) : X ⟶ cylinder X :=
+prod.lift (𝟙 X) (to_pt X ≫ I₀)
+def cylinder₁ (X : Top) : X ⟶ cylinder X :=
+prod.lift (𝟙 X) (to_pt X ≫ I₁)
 
--- The mapping cylinder is the colimit of the diagram
+-- The mapping cylinder is the pushout of the diagram
 --    X
 --   ↙ ↘
 --  Y   (X x I)
-def mapping_cylinder {X Y : Top} (f : X ⟶ Y) : Top := colimit (span f (cylinder_1 X))
-
--- The mapping cone is the colimit of the diagram
+-- (`pushout` is implemented just as a wrapper around `colimit`) is
+def mapping_cylinder {X Y : Top} (f : X ⟶ Y) : Top := pushout f (cylinder₁ X)
+
+/-- We construct the map from `X` into the "bottom" of the mapping cylinder
+for `f : X ⟶ Y`, as the composition of the inclusion of `X` into the bottom of the
+cylinder `prod X I`, followed by the map `pushout.inr` of `prod X I` into `mapping_cylinder f`. -/
+def mapping_cylinder₀ {X Y : Top} (f : X ⟶ Y) : X ⟶ mapping_cylinder f :=
+cylinder₀ X ≫ pushout.inr
+
+/--
+The mapping cone is defined as the pushout of
+```
+         X
+        ↙ ↘
+ (Cyl f)   pt
+```
+(where the left arrow is `mapping_cylinder₀`).
+
+This makes it an iterated colimit; one could also define it in one step as the colimit of
+```
 --    X        X
 --   ↙ ↘      ↙ ↘
 --  Y   (X x I)  pt
--- Here we'll calculate it as an iterated colimit, as the colimit of
---         X
---        ↙ ↘
--- (Cyl f)   pt
-
-def mapping_cylinder_0 {X Y : Top} (f : X ⟶ Y) : X ⟶ mapping_cylinder f :=
-cylinder_0 X ≫ colimit.ι (span f (cylinder_1 X)) walking_span.right
-
-def mapping_cone {X Y : Top} (f : X ⟶ Y) : Top := colimit (span (mapping_cylinder_0 f) (to_pt X))
+```
+-/
+def mapping_cone {X Y : Top} (f : X ⟶ Y) : Top := pushout (mapping_cylinder₀ f) (to_pt X)
 
 -- TODO Hopefully someone will write a nice tactic for generating diagrams quickly,
 -- and we'll be able to verify that this iterated construction is the same as the colimit
@@ -61,29 +72,33 @@ section Gluing
 
 -- Here's two copies of the real line glued together at a point.
 def f : pt ⟶ R := { val := λ _, (0 : ℝ), property := continuous_const }
-def X : Top := colimit (span f f)
+
+/-- Two copies of the real line glued together at 0. -/
+def X : Top := pushout f f
 
 -- To define a map out of it, we define maps out of each copy of the line,
 -- and check the maps agree at 0.
--- `pushout_cocone.mk` is a helper method for constructing cocones over a span.
 def g : X ⟶ R :=
-colimit.desc (span f f) (pushout_cocone.mk (𝟙 _) (𝟙 _) rfl).
+pushout.desc (𝟙 _) (𝟙 _) rfl
 
 end Gluing
 
 universes v u w
 
 section Products
 
-def d : discrete ℕ ⥤ Top := functor.of_function (λ n : ℕ, R)
-
-def Y : Top := limit d
-
-def w : cone d := fan.mk (λ (n : ℕ), ⟨λ (_ : pt), (n : ℝ), continuous_const⟩)
+/-- The countably infinite product of copies of `ℝ`. -/
+def Y : Top := ∏ (λ n : ℕ, R)
 
+/-- We define a point of this infinite product by specifying its coordinates. -/
 def q : pt ⟶ Y :=
-limit.lift d w
+pi.lift (λ (n : ℕ), ⟨λ (_ : pt), (n : ℝ), continuous_const⟩)
+
+-- "Looking under the hood", we see that `q` is a `subtype`, whose `val` is a function `unit → Y.α`.
+-- #check q.val -- q.val : pt.α → Y.α
+-- `q.property` is the fact this function is continous (i.e. no content)
 
+-- We can check that this function is definitionally just the function we specified.
 example : (q.val ()).val (57 : ℕ) = ((57 : ℕ) : ℝ) := rfl
 
 end Products

src/category_theory/discrete_category.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import data.ulift
+import data.fintype
 import category_theory.opposites category_theory.equivalence
 
 namespace category_theory
@@ -13,6 +14,9 @@ universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.c
 -- We only work in `Type`, rather than `Sort`, as we need to use `ulift`.
 def discrete (α : Type u₁) := α
 
+instance {α : Type u₁} [fintype α] : fintype (discrete α) :=
+by { dsimp [discrete], apply_instance }
+
 instance discrete_category (α : Type u₁) : small_category (discrete α) :=
 { hom  := λ X Y, ulift (plift (X = Y)),
   id   := λ X, ulift.up (plift.up rfl),
@@ -30,27 +34,35 @@ include 𝒞
 
 namespace functor
 
-@[simp] def of_function {I : Type u₁} (F : I → C) : (discrete I) ⥤ C :=
+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 }
 
+@[simp] lemma of_function_obj  {I : Type u₁} (F : I → C) (i : I) : (of_function F).obj i = F i := rfl
+@[simp] lemma of_function_map  {I : Type u₁} (F : I → C) {i : discrete I} (f : i ⟶ i) :
+  (of_function F).map f = 𝟙 (F i) :=
+by { cases f, cases f, cases f, refl }
+
 end functor
 
 namespace nat_trans
 
-@[simp] def of_homs {I : Type u₁} {F G : discrete I ⥤ C}
+def of_homs {I : Type u₁} {F G : discrete I ⥤ C}
   (f : Π i : discrete I, F.obj i ⟶ G.obj i) : F ⟶ G :=
 { app := f }
 
-@[simp] def of_function {I : Type u₁} {F G : I → C} (f : Π i : I, F i ⟶ G i) :
+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) :=
 of_homs f
 
+@[simp] lemma of_function_app {I : Type u₁} {F G : I → C} (f : Π i : I, F i ⟶ G i) (i : I) :
+  (of_function f).app i = f i := rfl
+
 end nat_trans
 
 namespace nat_iso
 
-@[simp] def of_isos {I : Type u₁} {F G : discrete I ⥤ C}
+def of_isos {I : Type u₁} {F G : discrete I ⥤ C}
   (f : Π i : discrete I, F.obj i ≅ G.obj i) : F ≅ G :=
 of_components f (by tidy)
 

src/category_theory/functor_category.lean

@@ -63,7 +63,8 @@ infix ` ◫ `:80 := hcomp
 @[simp] lemma hcomp_app {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) (X : C) :
   (α ◫ β).app X = (β.app (F.obj X)) ≫ (I.map (α.app X)) := rfl
 
--- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we need to use associativity of functor composition
+-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we
+-- need to use associativity of functor composition
 
 lemma exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H)
   (γ : I ⟶ J) (δ : J ⟶ K) : (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ) :=

src/category_theory/limits/limits.lean

@@ -298,7 +298,7 @@ def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
 @[simp] lemma limit.is_limit_lift {F : J ⥤ C} [has_limit F] (c : cone F) :
   (limit.is_limit F).lift c = limit.lift F c := rfl
 
-@[simp] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
+@[simp,reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
   limit.lift F c ≫ limit.π F j = c.π.app j :=
 is_limit.fac _ c j
 
@@ -453,7 +453,7 @@ def lim : (J ⥤ C) ⥤ C :=
 
 variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
-@[simp] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
+@[simp,reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
 by apply is_limit.fac
 
 @[simp] lemma limit.lift_map (c : cone F) :