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} (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} [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) :
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} (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
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} (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} [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) :
@[simp]
theorem category_theory.arrow.w {T : Type u} [category_theory.category T] {f g : category_theory.arrow T} (sq : f ⟶ g) :
@[simp]
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') :
@[simp]
@[simp]
theorem category_theory.arrow.w_mk_right_assoc {T : Type u} [category_theory.category T] {f : category_theory.arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ category_theory.arrow.mk g) {X' : T . "obviously"} (f' : Y ⟶ X') :
def category_theory.arrow.iso_mk {T : Type u} [category_theory.category T] {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]

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

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} [category_theory.category T] {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.

@[class]
structure category_theory.arrow.has_lift {T : Type u} [category_theory.category T] {f g : category_theory.arrow T} (sq : 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' : g.right ⟶ X') :
@[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 . "obviously"} (f' : g.left ⟶ X') :

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'_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') :

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

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

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