mathlib3 documentation

category_theory.arrow

The category of arrows #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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
@[simp]

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

Equations
@[simp]
@[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} (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) :
sq.left g.hom = f.hom sq.right
@[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} (f' : (𝟭 T).obj g.right X') :
sq.left g.hom f' = f.hom sq.right f'
@[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} (f' : Y X') :
sq.left g f' = f.hom sq.right f'
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

A functor C ⥤ D induces a functor between the corresponding arrow categories.

Equations
@[simp]

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

Equations