# 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} :
(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) :

@[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} :
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} :
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) :

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

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'

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) :
x.lift = y.liftx = y

@[ext]
structure category_theory.arrow.lift_struct {T : Type u} {f g : category_theory.arrow T} :
(f g)Type v

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

@[class]
structure category_theory.arrow.has_lift {T : Type u} {f g : category_theory.arrow T} :
(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' : (𝟭 T).obj 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} (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_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.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₂}  :
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) :