/
arrow.lean
135 lines (100 loc) · 4.36 KB
/
arrow.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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
/-
Copyright (c) 2020 Markus Himmel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import category_theory.comma
/-!
# The category of arrows
The category of arrows, with morphisms commutative squares.
We set this up as a specialization of the comma category `comma L R`,
where `L` and `R` are both the identity functor.
We also define the typeclass `has_lift`, representing a choice of a lift
of a commutative square (that is, a diagonal morphism making the two triangles commute).
## Tags
comma, arrow
-/
namespace category_theory
universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
variables {T : Type u} [category.{v} T]
section
variables (T)
/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
squares in `T`. -/
@[derive category]
def arrow := comma.{v v v} (𝟭 T) (𝟭 T)
-- Satisfying the inhabited linter
instance arrow.inhabited [inhabited T] : inhabited (arrow T) :=
{ default := show comma (𝟭 T) (𝟭 T), from default (comma (𝟭 T) (𝟭 T)) }
end
namespace arrow
@[simp] lemma id_left (f : arrow T) : comma_morphism.left (𝟙 f) = 𝟙 (f.left) := rfl
@[simp] lemma id_right (f : arrow T) : comma_morphism.right (𝟙 f) = 𝟙 (f.right) := rfl
/-- An object in the arrow category is simply a morphism in `T`. -/
@[simps]
def mk {X Y : T} (f : X ⟶ Y) : arrow T :=
{ left := X,
right := Y,
hom := f }
/-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
category. -/
@[simps]
def hom_mk {f g : arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right}
(w : u ≫ g.hom = f.hom ≫ v) : f ⟶ g :=
{ left := u,
right := v,
w' := w }
/-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/
@[simps]
def hom_mk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
(w : u ≫ g = f ≫ v) : arrow.mk f ⟶ arrow.mk g :=
{ left := u,
right := v,
w' := w }
@[reassoc] lemma w {f g : arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := sq.w
/-- A lift of a commutative square is a diagonal morphism making the two triangles commute. -/
@[ext] class has_lift {f g : arrow T} (sq : f ⟶ g) :=
(lift : f.right ⟶ g.left)
(fac_left : f.hom ≫ lift = sq.left)
(fac_right : lift ≫ g.hom = sq.right)
attribute [simp, reassoc] has_lift.fac_left has_lift.fac_right
/-- If we have chosen a lift of a commutative square `sq`, we can access it by saying `lift sq`. -/
abbreviation lift {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : f.right ⟶ g.left :=
has_lift.lift sq
lemma lift.fac_left {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : f.hom ≫ lift sq = sq.left :=
by simp
lemma lift.fac_right {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : lift sq ≫ g.hom = sq.right :=
by simp
@[simp, reassoc]
lemma lift_mk'_left {X Y P Q : T} {f : X ⟶ Y} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
(h : u ≫ g = f ≫ v) [has_lift $ arrow.hom_mk' h] : f ≫ lift (arrow.hom_mk' h) = u :=
by simp only [←arrow.mk_hom f, lift.fac_left, arrow.hom_mk'_left]
@[simp, reassoc]
lemma lift_mk'_right {X Y P Q : T} {f : X ⟶ Y} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
(h : u ≫ g = f ≫ v) [has_lift $ arrow.hom_mk' h] : lift (arrow.hom_mk' h) ≫ g = v :=
by simp only [←arrow.mk_hom g, lift.fac_right, arrow.hom_mk'_right]
section
instance subsingleton_has_lift_of_epi {f g : arrow T} (sq : f ⟶ g) [epi f.hom] :
subsingleton (has_lift sq) :=
subsingleton.intro $ λ a b, has_lift.ext a b $ (cancel_epi f.hom).1 $ by simp
instance subsingleton_has_lift_of_mono {f g : arrow T} (sq : f ⟶ g) [mono g.hom] :
subsingleton (has_lift sq) :=
subsingleton.intro $ λ a b, has_lift.ext a b $ (cancel_mono g.hom).1 $ by simp
end
end arrow
namespace functor
universes v₁ v₂ u₁ u₂
variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
/-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/
@[simps]
def map_arrow (F : C ⥤ D) : arrow C ⥤ arrow D :=
{ obj := λ a,
{ left := F.obj a.left,
right := F.obj a.right,
hom := F.map a.hom, },
map := λ a b f,
{ left := F.map f.left,
right := F.map f.right,
w' := by { have w := f.w, simp only [id_map] at w, dsimp, simp only [←F.map_comp, w], } } }
end functor
end category_theory