# mathlibdocumentation

category_theory.arrow

# 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

@[instance]
def category_theory.arrow.category (T : Type u)  :
def category_theory.arrow (T : Type u)  :
Type (max u v)

The arrow category of T has as objects all morphisms in T and as morphisms commutative squares in T.

Equations
@[instance]
def category_theory.arrow.inhabited (T : Type u) [inhabited T] :
Equations
@[simp]
theorem category_theory.arrow.id_left {T : Type u} (f : category_theory.arrow T) :
@[simp]
@[simp]
theorem category_theory.arrow.mk_right {T : Type u} {X Y : T} (f : X Y) :
def category_theory.arrow.mk {T : Type u} {X Y : T} (f : X Y) :

An object in the arrow category is simply a morphism in T.

Equations
@[simp]
theorem category_theory.arrow.mk_hom {T : Type u} {X Y : T} (f : X Y) :
@[simp]
theorem category_theory.arrow.mk_left {T : Type u} {X Y : T} (f : X Y) :
theorem category_theory.arrow.mk_injective {T : Type u} (A B : T) :
theorem category_theory.arrow.mk_inj {T : Type u} (A B : T) {f g : A B} :
@[instance]
def category_theory.arrow.has_coe {T : Type u} {X Y : T} :
has_coe (X Y)
Equations
@[simp]
theorem category_theory.arrow.hom_mk_right {T : Type u} {f g : category_theory.arrow T} {u : f.left g.left} {v : f.right g.right} (w : u g.hom = f.hom v) :
def category_theory.arrow.hom_mk {T : Type u} {f g : category_theory.arrow T} {u : f.left g.left} {v : f.right g.right} (w : u g.hom = f.hom v) :
f g

A morphism in the arrow category is a commutative square connecting two objects of the arrow category.

Equations
@[simp]
theorem category_theory.arrow.hom_mk_left {T : Type u} {f g : category_theory.arrow T} {u : f.left g.left} {v : f.right g.right} (w : u g.hom = f.hom v) :
def category_theory.arrow.hom_mk' {T : Type u} {X Y : T} {f : X Y} {P Q : T} {g : P Q} {u : X P} {v : Y Q} (w : u g = f v) :

We can also build a morphism in the arrow category out of any commutative square in T.

Equations
@[simp]
theorem category_theory.arrow.hom_mk'_right {T : Type u} {X Y : T} {f : X Y} {P Q : T} {g : P Q} {u : X P} {v : Y Q} (w : u g = f v) :
@[simp]
theorem category_theory.arrow.hom_mk'_left {T : Type u} {X Y : T} {f : X Y} {P Q : T} {g : P Q} {u : X P} {v : Y Q} (w : u g = f v) :
@[simp]
theorem category_theory.arrow.w {T : Type u} {f g : category_theory.arrow T} (sq : f g) :
sq.left g.hom = f.hom sq.right
@[simp]
theorem category_theory.arrow.w_assoc {T : Type u} {f g : category_theory.arrow T} (sq : f g) {X' : T . "obviously"} (f' : (𝟭 T).obj g.right X') :
sq.left g.hom f' = f.hom sq.right f'
@[simp]
theorem category_theory.arrow.w_mk_right {T : Type u} {f : category_theory.arrow T} {X Y : T} {g : X Y} (sq : f ) :
sq.left g = f.hom sq.right
@[simp]
theorem category_theory.arrow.w_mk_right_assoc {T : Type u} {f : category_theory.arrow T} {X Y : T} {g : X Y} (sq : f ) {X' : T . "obviously"} (f' : Y X') :
sq.left g f' = f.hom sq.right f'
@[instance]
def category_theory.arrow.category_theory.is_iso {T : Type u} {f g : category_theory.arrow T} (ff : f g)  :
@[simp]
theorem category_theory.arrow.iso_mk_hom_right {T : Type u} {f g : category_theory.arrow T} (l : f.left g.left) (r : f.right g.right) (h : l.hom g.hom = f.hom r.hom) :
h).hom.right = r.hom
@[simp]
theorem category_theory.arrow.iso_mk_hom_left {T : Type u} {f g : category_theory.arrow T} (l : f.left g.left) (r : f.right g.right) (h : l.hom g.hom = f.hom r.hom) :
h).hom.left = l.hom
def category_theory.arrow.iso_mk {T : Type u} {f g : category_theory.arrow T} (l : f.left g.left) (r : f.right g.right) (h : l.hom g.hom = f.hom r.hom) :
f g

Create an isomorphism between arrows, by providing isomorphisms between the domains and codomains, and a proof that the square commutes.

Equations
@[simp]
theorem category_theory.arrow.iso_mk_inv_left {T : Type u} {f g : category_theory.arrow T} (l : f.left g.left) (r : f.right g.right) (h : l.hom g.hom = f.hom r.hom) :
h).inv.left = l.inv
@[simp]
theorem category_theory.arrow.iso_mk_inv_right {T : Type u} {f g : category_theory.arrow T} (l : f.left g.left) (r : f.right g.right) (h : l.hom g.hom = f.hom r.hom) :
h).inv.right = r.inv
@[simp]
theorem category_theory.arrow.square_to_iso_invert {T : Type u} (i : category_theory.arrow T) {X Y : T} (p : X Y) (sq : i ) :
i.hom sq.right p.inv = sq.left

Given a square from an arrow i to an isomorphism p, express the source part of sq in terms of the inverse of p.

theorem category_theory.arrow.square_from_iso_invert {T : Type u} {X Y : T} (i : X Y) (p : category_theory.arrow T) (sq : p) :
i.inv sq.left p.hom = sq.right

Given a square from an isomorphism i to an arrow p, express the target part of sq in terms of the inverse of i.

theorem category_theory.arrow.lift_struct.ext {T : Type u} {_inst_1 : category_theory.category T} {f g : category_theory.arrow T} {sq : f g} (x y : category_theory.arrow.lift_struct sq) (h : x.lift = y.lift) :
x = y
@[ext]
structure category_theory.arrow.lift_struct {T : Type u} {f g : category_theory.arrow T} (sq : f g) :
Type v

A lift of a commutative square is a diagonal morphism making the two triangles commute.

@[simp]
theorem category_theory.arrow.lift_struct.fac_left {T : Type u} {f g : category_theory.arrow T} {sq : f g}  :
f.hom c.lift = sq.left
@[simp]
theorem category_theory.arrow.lift_struct.fac_right {T : Type u} {f g : category_theory.arrow T} {sq : f g}  :
c.lift g.hom = sq.right
@[class]
structure category_theory.arrow.has_lift {T : Type u} {f g : category_theory.arrow T} (sq : f g) :
Prop
• exists_lift :

has_lift sq says that there is some lift_struct sq, i.e., that it is possible to find a diagonal morphism making the two triangles commute.

Instances
theorem category_theory.arrow.has_lift.mk {T : Type u} {f g : category_theory.arrow T} {sq : f g}  :
@[simp]
theorem category_theory.arrow.lift_struct.fac_right_assoc {T : Type u} {f g : category_theory.arrow T} {sq : f g} {X' : T . "obviously"} (f' : g.right X') :
c.lift g.hom f' = sq.right f'
@[simp]
theorem category_theory.arrow.lift_struct.fac_left_assoc {T : Type u} {f g : category_theory.arrow T} {sq : f g} {X' : T . "obviously"} (f' : g.left X') :
f.hom c.lift f' = sq.left f'
def category_theory.arrow.has_lift.struct {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :

Given has_lift sq, obtain a lift.

Equations
def category_theory.arrow.lift {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :

If there is a lift of a commutative square sq, we can access it by saying lift sq.

theorem category_theory.arrow.lift.fac_left {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
= sq.left
theorem category_theory.arrow.lift.fac_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
= sq.right
@[simp]
theorem category_theory.arrow.lift.fac_right_of_to_mk {T : Type u} {X Y : T} {f : category_theory.arrow T} {g : X Y} (sq : f )  :
= sq.right
@[simp]
theorem category_theory.arrow.lift.fac_right_of_to_mk_assoc {T : Type u} {X Y : T} {f : category_theory.arrow T} {g : X Y} (sq : f ) {X' : T . "obviously"} (f' : Y X') :
g f' = sq.right f'
@[simp]
theorem category_theory.arrow.lift.fac_left_of_from_mk_assoc {T : Type u} {X Y : T} {f : X Y} {g : category_theory.arrow T} (sq : g) {X' : T} (f' : g.left X') :
f = sq.left f'
@[simp]
theorem category_theory.arrow.lift.fac_left_of_from_mk {T : Type u} {X Y : T} {f : X Y} {g : category_theory.arrow T} (sq : g)  :
= sq.left
@[simp]
theorem category_theory.arrow.lift_mk'_left_assoc {T : Type u} {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v) {X' : T} (f' : X') :
= u f'
@[simp]
theorem category_theory.arrow.lift_mk'_left {T : Type u} {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v)  :
@[simp]
theorem category_theory.arrow.lift_mk'_right {T : Type u} {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v)  :
@[simp]
theorem category_theory.arrow.lift_mk'_right_assoc {T : Type u} {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v) {X' : T . "obviously"} (f' : Q X') :
= v f'
@[instance]
@[instance]
@[simp]
theorem category_theory.arrow.square_to_snd_right {C : Type u} {X Y Z : C} {i : category_theory.arrow C} {f : X Y} {g : Y Z} (sq : i ) :
@[simp]
theorem category_theory.arrow.square_to_snd_left {C : Type u} {X Y Z : C} {i : category_theory.arrow C} {f : X Y} {g : Y Z} (sq : i ) :
= sq.left f
def category_theory.arrow.square_to_snd {C : Type u} {X Y Z : C} {i : category_theory.arrow C} {f : X Y} {g : Y Z} (sq : i ) :

A helper construction: given a square between i and f ≫ g, produce a square between i and g, whose top leg uses f: A → X ↓f ↓i Y --> A → Y ↓g ↓i ↓g B → Z B → Z

Equations
@[simp]
theorem category_theory.arrow.left_func_map {C : Type u} (_x _x_1 : (𝟭 C)) (f : _x _x_1) :
def category_theory.arrow.left_func {C : Type u}  :

The functor sending an arrow to its source.

Equations
@[simp]
theorem category_theory.arrow.left_func_obj {C : Type u} (X : (𝟭 C)) :
def category_theory.arrow.right_func {C : Type u}  :

The functor sending an arrow to its target.

Equations
@[simp]
theorem category_theory.arrow.right_func_obj {C : Type u} (X : (𝟭 C)) :
@[simp]
theorem category_theory.arrow.right_func_map {C : Type u} (_x _x_1 : (𝟭 C)) (f : _x _x_1) :

The natural transformation from left_func to right_func, given by the arrow itself.

Equations
@[simp]
@[simp]
theorem category_theory.functor.map_arrow_obj_hom {C : Type u₁} {D : Type u₂} (F : C D) (a : category_theory.arrow C) :
(F.map_arrow.obj a).hom = F.map a.hom
@[simp]
theorem category_theory.functor.map_arrow_map_right {C : Type u₁} {D : Type u₂} (F : C D) (a b : category_theory.arrow C) (f : a b) :
def category_theory.functor.map_arrow {C : Type u₁} {D : Type u₂} (F : C D) :

A functor C ⥤ D induces a functor between the corresponding arrow categories.

Equations
@[simp]
theorem category_theory.functor.map_arrow_map_left {C : Type u₁} {D : Type u₂} (F : C D) (a b : category_theory.arrow C) (f : a b) :
@[simp]
theorem category_theory.functor.map_arrow_obj_right {C : Type u₁} {D : Type u₂} (F : C D) (a : category_theory.arrow C) :
@[simp]
theorem category_theory.functor.map_arrow_obj_left {C : Type u₁} {D : Type u₂} (F : C D) (a : category_theory.arrow C) :