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

@[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
@[reducible]
def category_theory.arrow.iso_mk' {T : Type u} [category_theory.category T] {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} [category_theory.category T] {f g : category_theory.arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) :
φ₁.left = φ₂.left
theorem category_theory.arrow.hom.congr_right {T : Type u} [category_theory.category T] {f g : category_theory.arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) :
φ₁.right = φ₂.right
@[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.

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

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

Equations