/
functor_category.lean
98 lines (74 loc) · 4.03 KB
/
functor_category.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
-/
import category_theory.natural_transformation
namespace category_theory
universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
open nat_trans category category_theory.functor
variables (C : Type u₁) [𝒞 : category.{v₁} C] (D : Type u₂) [𝒟 : category.{v₂} D]
include 𝒞 𝒟
/--
`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,
this is another small category at that level.
However if `C` and `D` are both large categories at the same universe level,
this is a small category at the next higher level.
-/
instance functor.category : category.{(max u₁ v₂)} (C ⥤ D) :=
{ hom := λ F G, nat_trans F G,
id := λ F, nat_trans.id F,
comp := λ _ _ _ α β, vcomp α β }
variables {C D} {E : Type u₃} [ℰ : category.{v₃} E]
variables {F G H I : C ⥤ D}
namespace nat_trans
@[simp] lemma vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : vcomp α β = α ≫ β := rfl
lemma congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw h
@[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
@[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
(α ≫ β).app X = α.app X ≫ β.app X := rfl
include ℰ
lemma app_naturality {F G : C ⥤ (D ⥤ E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :
((F.obj X).map f) ≫ ((T.app X).app Z) = ((T.app X).app Y) ≫ ((G.obj X).map f) :=
(T.app X).naturality f
lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) :
((F.map f).app Z) ≫ ((T.app Y).app Z) = ((T.app X).app Z) ≫ ((G.map f).app Z) :=
congr_fun (congr_arg app (T.naturality f)) Z
/-- `hcomp α β` is the horizontal composition of natural transformations. -/
def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : (F ⋙ H) ⟶ (G ⋙ I) :=
{ app := λ X : C, (β.app (F.obj X)) ≫ (I.map (α.app X)),
naturality' := begin
intros, rw [functor.comp_map, functor.comp_map, assoc_symm, naturality, assoc],
rw [← map_comp I, naturality, map_comp, assoc]
end }
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. (It's true without the explicit associator,
-- because functor composition is definitionally associative, but relying on the definitional equality
-- causes bad problems with elaboration later.)
lemma exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H)
(γ : I ⟶ J) (δ : J ⟶ K) : (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ) :=
by { ext, dsimp, rw [assoc, assoc, map_comp, assoc_symm (δ.app _), ← naturality, assoc] }
end nat_trans
open nat_trans
namespace functor
include ℰ
protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
{ obj := λ k,
{ obj := λ j, (F.obj j).obj k,
map := λ j j' f, (F.map f).app k,
map_id' := λ X, begin rw category_theory.functor.map_id, refl end,
map_comp' := λ X Y Z f g, by rw [map_comp, ←comp_app] },
map := λ c c' f,
{ app := λ j, (F.obj j).map f } }.
@[simp] lemma flip_obj_obj (F : C ⥤ (D ⥤ E)) (c) (d) : (F.flip.obj d).obj c = (F.obj c).obj d := rfl
@[simp] lemma flip_obj_map (F : C ⥤ (D ⥤ E)) {c c' : C} (f : c ⟶ c') (d : D) :
(F.flip.obj d).map f = (F.map f).app d := rfl
@[simp] lemma flip_map_app (F : C ⥤ (D ⥤ E)) {d d' : D} (f : d ⟶ d') (c : C) :
(F.flip.map f).app c = (F.obj c).map f := rfl
end functor
end category_theory