mathlib documentation

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

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

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

Equations
@[simp]
theorem category_theory.arrow.mk_right {T : Type u} [category_theory.category T] {X Y : T} (f : X Y) :

def category_theory.arrow.mk {T : Type u} [category_theory.category T] {X Y : T} :

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

Equations
@[simp]
theorem category_theory.arrow.mk_hom {T : Type u} [category_theory.category T] {X Y : T} (f : X Y) :

@[simp]
theorem category_theory.arrow.mk_left {T : Type u} [category_theory.category T] {X Y : T} (f : X Y) :

@[simp]

def category_theory.arrow.hom_mk {T : Type u} [category_theory.category T] {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]

def category_theory.arrow.hom_mk' {T : Type u} [category_theory.category T] {X Y : T} {f : X Y} {P Q : T} {g : P Q} {u : X P} {v : Y Q} :

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} [category_theory.category T] {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} [category_theory.category T] {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} [category_theory.category T] {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} [category_theory.category T] {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} [category_theory.category T] {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} [category_theory.category T] {f g : category_theory.arrow T} :
(f g) → Prop

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
@[simp]
theorem category_theory.arrow.lift_struct.fac_right_assoc {T : Type u} [category_theory.category T] {f g : category_theory.arrow T} {sq : f g} (c : category_theory.arrow.lift_struct sq) {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} [category_theory.category T] {f g : category_theory.arrow T} {sq : f g} (c : category_theory.arrow.lift_struct sq) {X' : T} (f' : g.left X') :
f.hom c.lift f' = sq.left f'

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

@[simp]
theorem category_theory.arrow.lift_mk'_left_assoc {T : Type u} [category_theory.category T] {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v) [category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)] {X' : T} (f' : (category_theory.arrow.mk g).left X') :

@[simp]

@[simp]
theorem category_theory.arrow.lift_mk'_right_assoc {T : Type u} [category_theory.category T] {X Y P Q : T} {f : X Y} {g : P Q} {u : X P} {v : Y Q} (h : u g = f v) [category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)] {X' : T . "obviously"} (f' : Q X') :

@[simp]
theorem category_theory.functor.map_arrow_obj_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (a b : category_theory.arrow C) (f : a b) :

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (a b : category_theory.arrow C) (f : a b) :

@[simp]

@[simp]