# Documentation

Mathlib.CategoryTheory.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.

## Tags #

comma, arrow

def CategoryTheory.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.

Instances For
theorem CategoryTheory.Arrow.hom_ext {T : Type u} {X : } {Y : } (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g
@[simp]
theorem CategoryTheory.Arrow.id_left {T : Type u} (f : ) :
@[simp]
theorem CategoryTheory.Arrow.id_right {T : Type u} (f : ) :
().right =
theorem CategoryTheory.Arrow.comp_left_assoc {T : Type u} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) {Z : T} (h : Z.left Z) :
@[simp]
theorem CategoryTheory.Arrow.comp_left {T : Type u} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
theorem CategoryTheory.Arrow.comp_right_assoc {T : Type u} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) {Z : T} (h : Z.right Z) :
@[simp]
theorem CategoryTheory.Arrow.comp_right {T : Type u} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
().right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
theorem CategoryTheory.Arrow.mk_hom {T : Type u} {X : T} {Y : T} (f : X Y) :
().hom = f
@[simp]
theorem CategoryTheory.Arrow.mk_left {T : Type u} {X : T} {Y : T} (f : X Y) :
().left = X
@[simp]
theorem CategoryTheory.Arrow.mk_right {T : Type u} {X : T} {Y : T} (f : X Y) :
().right = Y
def CategoryTheory.Arrow.mk {T : Type u} {X : T} {Y : T} (f : X Y) :

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

Instances For
@[simp]
theorem CategoryTheory.Arrow.mk_eq {T : Type u} (f : ) :
= f
theorem CategoryTheory.Arrow.mk_injective {T : Type u} (A : T) (B : T) :
Function.Injective CategoryTheory.Arrow.mk
theorem CategoryTheory.Arrow.mk_inj {T : Type u} (A : T) (B : T) {f : A B} {g : A B} :
@[simp]
theorem CategoryTheory.Arrow.homMk_right {T : Type u} {f : } {g : } {u : f.left g.left} {v : f.right g.right} (w : ) :
().right = v
@[simp]
theorem CategoryTheory.Arrow.homMk_left {T : Type u} {f : } {g : } {u : f.left g.left} {v : f.right g.right} (w : ) :
().left = u
def CategoryTheory.Arrow.homMk {T : Type u} {f : } {g : } {u : f.left g.left} {v : f.right g.right} (w : ) :
f g

A morphism in the arrow category is a commutative square connecting two objects of the arrow category.

Instances For
@[simp]
theorem CategoryTheory.Arrow.homMk'_right {T : Type u} {X : T} {Y : T} {f : X Y} {P : T} {Q : T} {g : P Q} {u : X P} {v : Y Q} :
().right = v
@[simp]
theorem CategoryTheory.Arrow.homMk'_left {T : Type u} {X : T} {Y : T} {f : X Y} {P : T} {Q : T} {g : P Q} {u : X P} {v : Y Q} :
().left = u
def CategoryTheory.Arrow.homMk' {T : Type u} {X : T} {Y : T} {f : X Y} {P : T} {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.

Instances For
@[simp]
theorem CategoryTheory.Arrow.w_assoc {T : Type u} {f : } {g : } (sq : f g) {Z : T} (h : ().obj g.right Z) :
@[simp]
theorem CategoryTheory.Arrow.w {T : Type u} {f : } {g : } (sq : f g) :
@[simp]
theorem CategoryTheory.Arrow.w_mk_right_assoc {T : Type u} {f : } {X : T} {Y : T} {g : X Y} (sq : ) {Z : T} (h : Y Z) :
@[simp]
theorem CategoryTheory.Arrow.w_mk_right {T : Type u} {f : } {X : T} {Y : T} {g : X Y} (sq : ) :
@[simp]
theorem CategoryTheory.Arrow.isoMk_inv_right {T : Type u} {f : } {g : } (l : f.left g.left) (r : f.right g.right) (h : autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom) _auto✝) :
().inv.right = r.inv
@[simp]
theorem CategoryTheory.Arrow.isoMk_inv_left {T : Type u} {f : } {g : } (l : f.left g.left) (r : f.right g.right) (h : autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom) _auto✝) :
().inv.left = l.inv
@[simp]
theorem CategoryTheory.Arrow.isoMk_hom_right {T : Type u} {f : } {g : } (l : f.left g.left) (r : f.right g.right) (h : autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom) _auto✝) :
().hom.right = r.hom
@[simp]
theorem CategoryTheory.Arrow.isoMk_hom_left {T : Type u} {f : } {g : } (l : f.left g.left) (r : f.right g.right) (h : autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom) _auto✝) :
().hom.left = l.hom
def CategoryTheory.Arrow.isoMk {T : Type u} {f : } {g : } (l : f.left g.left) (r : f.right g.right) (h : autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom) _auto✝) :
f g

Create an isomorphism between arrows, by providing isomorphisms between the domains and codomains, and a proof that the square commutes.

Instances For
@[inline, reducible]
abbrev CategoryTheory.Arrow.isoMk' {T : Type u} {W : T} {X : T} {Y : T} {Z : T} (f : W X) (g : Y Z) (e₁ : W Y) (e₂ : X Z) (h : autoParam ( = ) _auto✝) :

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

Instances For
theorem CategoryTheory.Arrow.hom.congr_left {T : Type u} {f : } {g : } {φ₁ : f g} {φ₂ : f g} (h : φ₁ = φ₂) :
φ₁.left = φ₂.left
@[simp]
theorem CategoryTheory.Arrow.hom.congr_right {T : Type u} {f : } {g : } {φ₁ : f g} {φ₂ : f g} (h : φ₁ = φ₂) :
φ₁.right = φ₂.right
theorem CategoryTheory.Arrow.iso_w {T : Type u} {f : } {g : } (e : f g) :
theorem CategoryTheory.Arrow.iso_w' {T : Type u} {W : T} {X : T} {Y : T} {Z : T} {f : W X} {g : Y Z} :
instance CategoryTheory.Arrow.isIso_left {T : Type u} {f : } {g : } (sq : f g) [] :
instance CategoryTheory.Arrow.isIso_right {T : Type u} {f : } {g : } (sq : f g) [] :
@[simp]
theorem CategoryTheory.Arrow.inv_left {T : Type u} {f : } {g : } (sq : f g) [] :
().left = CategoryTheory.inv sq.left
@[simp]
theorem CategoryTheory.Arrow.inv_right {T : Type u} {f : } {g : } (sq : f g) [] :
().right = CategoryTheory.inv sq.right
instance CategoryTheory.Arrow.mono_left {T : Type u} {f : } {g : } (sq : f g) [] :
instance CategoryTheory.Arrow.epi_right {T : Type u} {f : } {g : } (sq : f g) [] :
@[simp]
theorem CategoryTheory.Arrow.square_to_iso_invert {T : Type u} (i : ) {X : T} {Y : T} (p : X Y) (sq : i ) :

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 CategoryTheory.Arrow.square_from_iso_invert {T : Type u} {X : T} {Y : T} (i : X Y) (p : ) (sq : 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.

@[simp]
theorem CategoryTheory.Arrow.squareToSnd_right {C : Type u} {X : C} {Y : C} {Z : C} {i : } {f : X Y} {g : Y Z} (sq : ) :
().right = sq.right
@[simp]
theorem CategoryTheory.Arrow.squareToSnd_left {C : Type u} {X : C} {Y : C} {Z : C} {i : } {f : X Y} {g : Y Z} (sq : ) :
().left =
def CategoryTheory.Arrow.squareToSnd {C : Type u} {X : C} {Y : C} {Z : C} {i : } {f : X Y} {g : Y Z} (sq : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Arrow.leftFunc_obj {C : Type u} :
CategoryTheory.Arrow.leftFunc.obj X = X.left
@[simp]
theorem CategoryTheory.Arrow.leftFunc_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.Arrow.leftFunc.map f = f.left

The functor sending an arrow to its source.

Instances For
@[simp]
theorem CategoryTheory.Arrow.rightFunc_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.Arrow.rightFunc.map f = f.right
@[simp]
theorem CategoryTheory.Arrow.rightFunc_obj {C : Type u} :
CategoryTheory.Arrow.rightFunc.obj X = X.right

The functor sending an arrow to its target.

Instances For
@[simp]
theorem CategoryTheory.Arrow.leftToRight_app {C : Type u} (f : ) :
CategoryTheory.Arrow.leftToRight.app f = f.hom
def CategoryTheory.Arrow.leftToRight {C : Type u} :
CategoryTheory.Arrow.leftFunc CategoryTheory.Arrow.rightFunc

The natural transformation from leftFunc to rightFunc, given by the arrow itself.

Instances For
@[simp]
theorem CategoryTheory.Functor.mapArrow_obj_hom {C : Type u₁} [] {D : Type u₂} [] (F : ) (a : ) :
(().obj a).hom = F.map a.hom
@[simp]
theorem CategoryTheory.Functor.mapArrow_obj_left {C : Type u₁} [] {D : Type u₂} [] (F : ) (a : ) :
(().obj a).left = F.obj a.left
@[simp]
theorem CategoryTheory.Functor.mapArrow_map_right {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : } (f : X Y), (().map f).right = F.map f.right
@[simp]
theorem CategoryTheory.Functor.mapArrow_map_left {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : } (f : X Y), (().map f).left = F.map f.left
@[simp]
theorem CategoryTheory.Functor.mapArrow_obj_right {C : Type u₁} [] {D : Type u₂} [] (F : ) (a : ) :
(().obj a).right = F.obj a.right
def CategoryTheory.Functor.mapArrow {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Functor.mapArrowFunctor_map_app_right (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (τ : X Y) (f : ), ((().map τ).app f).right = τ.app f.right
@[simp]
theorem CategoryTheory.Functor.mapArrowFunctor_map_app_left (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (τ : X Y) (f : ), ((().map τ).app f).left = τ.app f.left
@[simp]
theorem CategoryTheory.Functor.mapArrowFunctor_obj (C : Type u₁) [] (D : Type u₂) [] (F : ) :
def CategoryTheory.Functor.mapArrowFunctor (C : Type u₁) [] (D : Type u₂) [] :

The functor (C ⥤ D) ⥤ (Arrow C ⥤ Arrow D) which sends a functor F : C ⥤ D to F.mapArrow.

Instances For
def CategoryTheory.Functor.mapArrowEquivalence {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

The equivalence of categories Arrow C ≌ Arrow D induced by an equivalence C ≌ D.

Instances For
instance CategoryTheory.Functor.isEquivalenceMapArrow {C : Type u₁} [] {D : Type u₂} [] (F : ) :
def CategoryTheory.Arrow.isoOfNatIso {C : Type u_1} {D : Type u_2} [] [] {F : } {G : } (e : F G) (f : ) :
().obj f ().obj f

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

Instances For