# 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

@[protected, 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
Instances for category_theory.arrow
@[protected, 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) :
@[simp]
theorem category_theory.arrow.mk_eq {T : Type u} (f : category_theory.arrow T) :
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} :
@[protected, 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'
@[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
@[reducible]
def category_theory.arrow.iso_mk' {T : Type u} {W X Y Z : T} (f : W X) (g : Y Z) (e₁ : W Y) (e₂ : X Z) (h : e₁.hom g = f e₂.hom) :

A variant of arrow.iso_mk that creates an iso between two arrow.mks with a better type signature.

theorem category_theory.arrow.hom.congr_left {T : Type u} {f g : category_theory.arrow T} {φ₁ φ₂ : f g} (h : φ₁ = φ₂) :
φ₁.left = φ₂.left
theorem category_theory.arrow.hom.congr_right {T : Type u} {f g : category_theory.arrow T} {φ₁ φ₂ : f g} (h : φ₁ = φ₂) :
φ₁.right = φ₂.right
theorem category_theory.arrow.iso_w {T : Type u} {f g : category_theory.arrow T} (e : f g) :
theorem category_theory.arrow.iso_w' {T : Type u} {W X Y Z : T} {f : W X} {g : Y Z}  :
@[protected, instance]
def category_theory.arrow.is_iso_left {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[protected, instance]
def category_theory.arrow.is_iso_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[simp]
theorem category_theory.arrow.inv_left {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[simp]
theorem category_theory.arrow.inv_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[simp]
theorem category_theory.arrow.left_hom_inv_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
sq.left = f.hom
theorem category_theory.arrow.inv_left_hom_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
f.hom sq.right = g.hom
@[protected, instance]
def category_theory.arrow.mono_left {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[protected, instance]
def category_theory.arrow.epi_right {T : Type u} {f g : category_theory.arrow T} (sq : f g)  :
@[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.

@[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) :
def category_theory.arrow.iso_of_nat_iso {C : Type u_1} {D : Type u_2} {F G : C D} (e : F G) (f : category_theory.arrow C) :

The images of f : arrow C by two isomorphic functors F : C ⥤ D are isomorphic arrows in D.

Equations