feat(category_theory/limits): support for special shapes of (co)limits (#938)

feat(category_theory/limits): support for special shapes of (co)limits

Author: kim-em

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -0,0 +1,90 @@
+import category_theory.instances.Top.limits
+import category_theory.limits.shapes
+import topology.instances.real
+
+/- This file contains some demos of using the (co)limits API to do topology. -/
+
+noncomputable theory
+
+open category_theory
+open category_theory.instances
+open category_theory.limits
+
+def R : Top := Top.of ℝ
+def I : Top := Top.of (set.Icc 0 1 : set ℝ)
+def pt : Top := Top.of unit
+
+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 :=
+{ val := λ _, ⟨(0 : ℝ), begin rw [set.left_mem_Icc], norm_num, end⟩,
+  property := continuous_const }
+def I_1 : 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)
+-- 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))
+
+-- The mapping cylinder is the colimit 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
+--    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))
+
+-- 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
+-- over a single diagram.
+end MappingCylinder
+
+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)
+
+-- 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).
+
+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⟩)
+
+def q : pt ⟶ Y :=
+limit.lift d w
+
+example : (q.val ()).val (57 : ℕ) = ((57 : ℕ) : ℝ) := rfl
+
+end Products

src/category_theory/discrete_category.lean

@@ -48,10 +48,10 @@ def lift {α : Type u₁} {β : Type u₂} (f : α → β) : (discrete α) ⥤ (
 functor.of_function f
 
 include 𝒞
-variables (J : Type v₂)
+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) :=
+  (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,

src/category_theory/instances/Top/basic.lean

@@ -20,6 +20,8 @@ instance topological_space_unbundled (x : Top) : topological_space x := x.str
 namespace Top
 instance concrete_category_continuous : concrete_category @continuous := ⟨@continuous_id, @continuous.comp⟩
 
+def of (X : Type u) [topological_space X] : Top := ⟨X, by apply_instance⟩
+
 def discrete : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊤⟩,
   map := λ X Y f, ⟨f, continuous_top⟩ }

src/category_theory/limits/shapes/binary_products.lean

@@ -0,0 +1,39 @@
+-- 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.limits.cones
+import category_theory.discrete_category
+
+universes v u
+
+open category_theory
+
+namespace category_theory.limits
+
+@[derive decidable_eq] inductive walking_pair : Type v
+| left | right
+
+def pair_function {C : Sort u} (X Y : C) : walking_pair → C
+| walking_pair.left := X
+| walking_pair.right := Y
+
+variables {C : Sort u} [𝒞 : category.{v+1} C]
+include 𝒞
+
+def pair (X Y : C) : discrete walking_pair ⥤ C :=
+functor.of_function (pair_function X Y)
+
+abbreviation binary_fan (X Y : C) := cone (pair X Y)
+abbreviation binary_cofan (X Y : C) := cocone (pair X Y)
+
+variables {X Y : C}
+
+def binary_fan.mk {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : binary_fan X Y :=
+{ X := P,
+  π := { app := λ j, walking_pair.cases_on j π₁ π₂ }}
+def binary_cofan.mk {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : binary_cofan X Y :=
+{ X := P,
+  ι := { app := λ j, walking_pair.cases_on j ι₁ ι₂ }}
+
+end category_theory.limits

src/category_theory/limits/shapes/default.lean

@@ -0,0 +1,8 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.products
+import category_theory.limits.shapes.equalizers
+import category_theory.limits.shapes.pullbacks

src/category_theory/limits/shapes/equalizers.lean

@@ -0,0 +1,158 @@
+-- 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.eq_to_hom
+import category_theory.limits.cones
+
+open category_theory
+
+namespace category_theory.limits
+
+local attribute [tidy] tactic.case_bash
+
+universes v u
+
+@[derive decidable_eq] inductive walking_parallel_pair : Type v
+| zero | one
+
+open walking_parallel_pair
+
+inductive walking_parallel_pair_hom : walking_parallel_pair → walking_parallel_pair → Type v
+| left : walking_parallel_pair_hom zero one
+| right : walking_parallel_pair_hom zero one
+| id : Π X : walking_parallel_pair.{v}, walking_parallel_pair_hom X X
+
+open walking_parallel_pair_hom
+
+def walking_parallel_pair_hom.comp :
+  Π (X Y Z : walking_parallel_pair)
+    (f : walking_parallel_pair_hom X Y) (g : walking_parallel_pair_hom Y Z),
+    walking_parallel_pair_hom X Z
+  | _ _ _ (id _) h := h
+  | _ _ _ left   (id one) := left
+  | _ _ _ right  (id one) := right
+.
+
+instance walking_parallel_pair_hom_category : small_category.{v+1} walking_parallel_pair :=
+{ hom  := walking_parallel_pair_hom,
+  id   := walking_parallel_pair_hom.id,
+  comp := walking_parallel_pair_hom.comp }
+
+lemma walking_parallel_pair_hom_id (X : walking_parallel_pair.{v}) :
+  walking_parallel_pair_hom.id X = 𝟙 X :=
+rfl
+
+variables {C : Sort u} [𝒞 : category.{v+1} C]
+include 𝒞
+variables {X Y : C}
+
+def parallel_pair (f g : X ⟶ Y) : walking_parallel_pair.{v} ⥤ C :=
+{ obj := λ x, match x with
+  | zero := X
+  | one := Y
+  end,
+  map := λ x y h, match x, y, h with
+  | _, _, (id _) := 𝟙 _
+  | _, _, left := f
+  | _, _, right := g
+  end }.
+
+@[simp] lemma parallel_pair_map_left (f g : X ⟶ Y) : (parallel_pair f g).map left = f := rfl
+@[simp] lemma parallel_pair_map_right (f g : X ⟶ Y) : (parallel_pair f g).map right = g := rfl
+
+@[simp] lemma parallel_pair_functor_obj
+  {F : walking_parallel_pair.{v} ⥤ C} (j : walking_parallel_pair.{v}) :
+  (parallel_pair (F.map left) (F.map right)).obj j = F.obj j :=
+begin
+  cases j; refl
+end
+
+abbreviation fork (f g : X ⟶ Y) := cone (parallel_pair f g)
+abbreviation cofork (f g : X ⟶ Y) := cocone (parallel_pair f g)
+
+variables {f g : X ⟶ Y}
+
+attribute [simp] walking_parallel_pair_hom_id
+
+def fork.of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : fork f g :=
+{ X := P,
+  π :=
+  { app := λ X, begin cases X, exact ι, exact ι ≫ f, end,
+    naturality' := λ X Y f,
+    begin
+      cases X; cases Y; cases f; dsimp; simp,
+      exact w
+    end }}
+def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :=
+{ X := P,
+  ι :=
+  { app := λ X, begin cases X, exact f ≫ π, exact π, end,
+    naturality' := λ X Y f,
+    begin
+      cases X; cases Y; cases f; dsimp; simp,
+      exact eq.symm w
+    end }}
+
+@[simp] lemma fork.of_ι_app_zero {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
+  (fork.of_ι ι w).π.app zero = ι := rfl
+@[simp] lemma fork.of_ι_app_one {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
+  (fork.of_ι ι w).π.app one = ι ≫ f := rfl
+
+def fork.ι (t : fork f g) := t.π.app zero
+def cofork.π (t : cofork f g) := t.ι.app one
+def fork.condition (t : fork f g) : (fork.ι t) ≫ f = (fork.ι t) ≫ g :=
+begin
+  erw [t.w left, ← t.w right], refl
+end
+def cofork.condition (t : cofork f g) : f ≫ (cofork.π t) = g ≫ (cofork.π t) :=
+begin
+  erw [t.w left, ← t.w right], refl
+end
+
+def cone.of_fork
+  {F : walking_parallel_pair.{v} ⥤ C} (t : fork (F.map left) (F.map right)) : cone F :=
+{ X := t.X,
+  π :=
+  { app := λ X, t.π.app X ≫ eq_to_hom (by tidy),
+    naturality' := λ j j' g,
+    begin
+      cases j; cases j'; cases g; dsimp; simp,
+      erw ← t.w left, refl,
+      erw ← t.w right, refl,
+    end } }.
+def cocone.of_cofork
+  {F : walking_parallel_pair.{v} ⥤ C} (t : cofork (F.map left) (F.map right)) : cocone F :=
+{ X := t.X,
+  ι :=
+  { app := λ X, eq_to_hom (by tidy) ≫ t.ι.app X,
+    naturality' := λ j j' g,
+    begin
+      cases j; cases j'; cases g; dsimp; simp,
+      erw ← t.w left, refl,
+      erw ← t.w right, refl,
+    end } }.
+
+@[simp] lemma cone.of_fork_π
+  {F : walking_parallel_pair.{v} ⥤ C} (t : fork (F.map left) (F.map right)) (j):
+  (cone.of_fork t).π.app j = t.π.app j ≫ eq_to_hom (by tidy) := rfl
+
+@[simp] lemma cocone.of_cofork_ι
+  {F : walking_parallel_pair.{v} ⥤ C} (t : cofork (F.map left) (F.map right)) (j):
+  (cocone.of_cofork t).ι.app j = eq_to_hom (by tidy) ≫ t.ι.app j := rfl
+
+def fork.of_cone
+  {F : walking_parallel_pair.{v} ⥤ C} (t : cone F) : fork (F.map left) (F.map right) :=
+{ X := t.X,
+  π := { app := λ X, t.π.app X ≫ eq_to_hom (by tidy) } }
+def cofork.of_cocone
+  {F : walking_parallel_pair.{v} ⥤ C} (t : cocone F) : cofork (F.map left) (F.map right) :=
+{ X := t.X,
+  ι := { app := λ X, eq_to_hom (by tidy) ≫ t.ι.app X } }
+
+@[simp] lemma fork.of_cone_π {F : walking_parallel_pair.{v} ⥤ C} (t : cone F) (j) :
+  (fork.of_cone t).π.app j = t.π.app j ≫ eq_to_hom (by tidy) := rfl
+@[simp] lemma cofork.of_cocone_ι {F : walking_parallel_pair.{v} ⥤ C} (t : cocone F) (j) :
+  (cofork.of_cocone t).ι.app j = eq_to_hom (by tidy) ≫ t.ι.app j := rfl
+
+end category_theory.limits

src/category_theory/limits/shapes/products.lean

@@ -0,0 +1,32 @@
+-- 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.limits.cones
+import category_theory.discrete_category
+
+universes v u
+
+open category_theory
+
+namespace category_theory.limits
+
+variables {β : Type v}
+variables {C : Sort u} [𝒞 : category.{v+1} C]
+include 𝒞
+
+-- We don't need an analogue of `pair` (for binary products), `parallel_pair` (for equalizers),
+-- or `(co)span`, since we already have `functor.of_function`.
+
+abbreviation fan (f : β → C) := cone (functor.of_function f)
+abbreviation cofan (f : β → C) := cocone (functor.of_function f)
+
+def fan.mk {f : β → C} {P : C} (p : Π b, P ⟶ f b) : fan f :=
+{ X := P,
+  π := { app := p } }
+
+def cofan.mk {f : β → C} {P : C} (p : Π b, f b ⟶ P) : cofan f :=
+{ X := P,
+  ι := { app := p } }
+
+end category_theory.limits