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) [CategoryTheory.Category.{v, u} 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

• CategoryTheory.Arrow T = CategoryTheory.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.id T)

instance CategoryTheory.instCategoryArrow (T : Type u) [CategoryTheory.Category.{v, u} T] : CategoryTheory.Category.{v, max u v} (CategoryTheory.Arrow T)

Equations

• CategoryTheory.instCategoryArrow T = CategoryTheory.commaCategory

instance CategoryTheory.Arrow.inhabited (T : Type u) [CategoryTheory.Category.{v, u} T] [Inhabited T] : Inhabited (CategoryTheory.Arrow T)

Equations

• CategoryTheory.Arrow.inhabited T = { default := let_fun this := default; this }

theorem CategoryTheory.Arrow.hom_ext {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

@[simp]

theorem CategoryTheory.Arrow.id_left {T : Type u} [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : (CategoryTheory.CategoryStruct.id f).left = CategoryTheory.CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.Arrow.id_right {T : Type u} [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : (CategoryTheory.CategoryStruct.id f).right = CategoryTheory.CategoryStruct.id f.right

@[simp]

theorem CategoryTheory.Arrow.comp_left {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left

theorem CategoryTheory.Arrow.comp_left_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : T} (h : Z.left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).left h = CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp g.left h)

@[simp]

theorem CategoryTheory.Arrow.comp_right {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right

theorem CategoryTheory.Arrow.comp_right_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : T} (h : Z.right ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).right h = CategoryTheory.CategoryStruct.comp f.right (CategoryTheory.CategoryStruct.comp g.right h)

def CategoryTheory.Arrow.mk {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : CategoryTheory.Arrow T

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

Equations

• CategoryTheory.Arrow.mk f = { left := X, right := Y, hom := f }

@[simp]

theorem CategoryTheory.Arrow.mk_right {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Arrow.mk f).right = Y

@[simp]

theorem CategoryTheory.Arrow.mk_hom {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Arrow.mk f).hom = f

@[simp]

theorem CategoryTheory.Arrow.mk_left {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Arrow.mk f).left = X

@[simp]

theorem CategoryTheory.Arrow.mk_eq {T : Type u} [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : CategoryTheory.Arrow.mk f.hom = f

theorem CategoryTheory.Arrow.mk_injective {T : Type u} [CategoryTheory.Category.{v, u} T] (A B : T) : Function.Injective CategoryTheory.Arrow.mk

theorem CategoryTheory.Arrow.mk_inj {T : Type u} [CategoryTheory.Category.{v, u} T] (A B : T) {f g : A ⟶ B} : CategoryTheory.Arrow.mk f = CategoryTheory.Arrow.mk g ↔ f = g

instance CategoryTheory.Arrow.instCoeOutHom {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} : CoeOut (X ⟶ Y) (CategoryTheory.Arrow T)

Equations

• CategoryTheory.Arrow.instCoeOutHom = { coe := CategoryTheory.Arrow.mk }

def CategoryTheory.Arrow.homMk {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right} (w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v) : f ⟶ g

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

Equations

• CategoryTheory.Arrow.homMk w = { left := u, right := v, w := w }

@[simp]

theorem CategoryTheory.Arrow.homMk_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right} (w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v) : (CategoryTheory.Arrow.homMk w).left = u

@[simp]

theorem CategoryTheory.Arrow.homMk_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right} (w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v) : (CategoryTheory.Arrow.homMk w).right = v

def CategoryTheory.Arrow.homMk' {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q} (w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v) : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g

We can also build a morphism in the arrow category out of any commutative square in T.

Equations

• CategoryTheory.Arrow.homMk' w = { left := u, right := v, w := w }

@[simp]

theorem CategoryTheory.Arrow.homMk'_right {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q} (w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v) : (CategoryTheory.Arrow.homMk' w).right = v

@[simp]

theorem CategoryTheory.Arrow.homMk'_left {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q} (w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v) : (CategoryTheory.Arrow.homMk' w).left = u

@[simp]

theorem CategoryTheory.Arrow.w {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) : CategoryTheory.CategoryStruct.comp sq.left g.hom = CategoryTheory.CategoryStruct.comp f.hom sq.right

@[simp]

theorem CategoryTheory.Arrow.w_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) {Z : T} (h : g.right ⟶ Z) : CategoryTheory.CategoryStruct.comp sq.left (CategoryTheory.CategoryStruct.comp g.hom h) = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp sq.right h)

@[simp]

theorem CategoryTheory.Arrow.w_mk_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ CategoryTheory.Arrow.mk g) : CategoryTheory.CategoryStruct.comp sq.left g = CategoryTheory.CategoryStruct.comp f.hom sq.right

@[simp]

theorem CategoryTheory.Arrow.w_mk_right_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ CategoryTheory.Arrow.mk g) {Z : T} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp sq.left (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp sq.right h)

theorem CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (ff : f ⟶ g) [CategoryTheory.IsIso ff.left] [CategoryTheory.IsIso ff.right] : CategoryTheory.IsIso ff

def CategoryTheory.Arrow.isoMk {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat) : f ≅ g

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

Equations

• CategoryTheory.Arrow.isoMk l r h = CategoryTheory.Comma.isoMk l r h

@[simp]

theorem CategoryTheory.Arrow.isoMk_hom_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat) : (CategoryTheory.Arrow.isoMk l r h).hom.left = l.hom

@[simp]

theorem CategoryTheory.Arrow.isoMk_hom_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat) : (CategoryTheory.Arrow.isoMk l r h).hom.right = r.hom

@[simp]

theorem CategoryTheory.Arrow.isoMk_inv_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat) : (CategoryTheory.Arrow.isoMk l r h).inv.right = r.inv

@[simp]

theorem CategoryTheory.Arrow.isoMk_inv_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat) : (CategoryTheory.Arrow.isoMk l r h).inv.left = l.inv

@[reducible, inline]

abbrev CategoryTheory.Arrow.isoMk' {T : Type u} [CategoryTheory.Category.{v, u} T] {W X Y Z : T} (f : W ⟶ X) (g : Y ⟶ Z) (e₁ : W ≅ Y) (e₂ : X ≅ Z) (h : CategoryTheory.CategoryStruct.comp e₁.hom g = CategoryTheory.CategoryStruct.comp f e₂.hom := by aesop_cat) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g

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

Equations

• CategoryTheory.Arrow.isoMk' f g e₁ e₂ h = CategoryTheory.Arrow.isoMk e₁ e₂ h

theorem CategoryTheory.Arrow.hom.congr_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left

@[simp]

theorem CategoryTheory.Arrow.hom.congr_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right

theorem CategoryTheory.Arrow.iso_w {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) : g.hom = CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp f.hom e.hom.right)

theorem CategoryTheory.Arrow.iso_w' {T : Type u} [CategoryTheory.Category.{v, u} T] {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : g = CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp f e.hom.right)

theorem CategoryTheory.Arrow.isIso_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.IsIso sq.left

theorem CategoryTheory.Arrow.isIso_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.IsIso sq.right

@[simp]

theorem CategoryTheory.Arrow.inv_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (CategoryTheory.inv sq).left = CategoryTheory.inv sq.left

@[simp]

theorem CategoryTheory.Arrow.inv_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (CategoryTheory.inv sq).right = CategoryTheory.inv sq.right

theorem CategoryTheory.Arrow.left_hom_inv_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.CategoryStruct.comp sq.left (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.inv sq.right)) = f.hom

theorem CategoryTheory.Arrow.inv_left_hom_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) (CategoryTheory.CategoryStruct.comp f.hom sq.right) = g.hom

theorem CategoryTheory.Arrow.mono_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.Mono sq] : CategoryTheory.Mono sq.left

theorem CategoryTheory.Arrow.epi_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) [CategoryTheory.Epi sq] : CategoryTheory.Epi sq.right

@[simp]

theorem CategoryTheory.Arrow.hom_inv_id_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) : CategoryTheory.CategoryStruct.comp e.hom.left e.inv.left = CategoryTheory.CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.Arrow.hom_inv_id_left_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T} (h : f.left ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.left (CategoryTheory.CategoryStruct.comp e.inv.left h) = h

@[simp]

theorem CategoryTheory.Arrow.inv_hom_id_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) : CategoryTheory.CategoryStruct.comp e.inv.left e.hom.left = CategoryTheory.CategoryStruct.id g.left

@[simp]

theorem CategoryTheory.Arrow.inv_hom_id_left_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T} (h : g.left ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp e.hom.left h) = h

@[simp]

theorem CategoryTheory.Arrow.hom_inv_id_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) : CategoryTheory.CategoryStruct.comp e.hom.right e.inv.right = CategoryTheory.CategoryStruct.id f.right

@[simp]

theorem CategoryTheory.Arrow.hom_inv_id_right_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T} (h : f.right ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.right (CategoryTheory.CategoryStruct.comp e.inv.right h) = h

@[simp]

theorem CategoryTheory.Arrow.inv_hom_id_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) : CategoryTheory.CategoryStruct.comp e.inv.right e.hom.right = CategoryTheory.CategoryStruct.id g.right

@[simp]

theorem CategoryTheory.Arrow.inv_hom_id_right_assoc {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T} (h : g.right ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.right (CategoryTheory.CategoryStruct.comp e.hom.right h) = h

@[simp]

theorem CategoryTheory.Arrow.square_to_iso_invert {T : Type u} [CategoryTheory.Category.{v, u} T] (i : CategoryTheory.Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ CategoryTheory.Arrow.mk p.hom) : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.CategoryStruct.comp sq.right p.inv) = sq.left

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} [CategoryTheory.Category.{v, u} T] {X Y : T} (i : X ≅ Y) (p : CategoryTheory.Arrow T) (sq : CategoryTheory.Arrow.mk i.hom ⟶ p) : CategoryTheory.CategoryStruct.comp i.inv (CategoryTheory.CategoryStruct.comp sq.left p.hom) = sq.right

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

def CategoryTheory.Arrow.squareToSnd {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {i : CategoryTheory.Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)) : i ⟶ CategoryTheory.Arrow.mk g

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

• CategoryTheory.Arrow.squareToSnd sq = { left := CategoryTheory.CategoryStruct.comp sq.left f, right := sq.right, w := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.squareToSnd_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {i : CategoryTheory.Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)) : (CategoryTheory.Arrow.squareToSnd sq).left = CategoryTheory.CategoryStruct.comp sq.left f

@[simp]

theorem CategoryTheory.Arrow.squareToSnd_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {i : CategoryTheory.Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)) : (CategoryTheory.Arrow.squareToSnd sq).right = sq.right

def CategoryTheory.Arrow.leftFunc {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Arrow C) C

The functor sending an arrow to its source.

Equations

• CategoryTheory.Arrow.leftFunc = CategoryTheory.Comma.fst (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)

@[simp]

theorem CategoryTheory.Arrow.leftFunc_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X✝ ⟶ Y✝) : CategoryTheory.Arrow.leftFunc.map f = f.left

@[simp]

theorem CategoryTheory.Arrow.leftFunc_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.leftFunc.obj X = X.left

def CategoryTheory.Arrow.rightFunc {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Arrow C) C

The functor sending an arrow to its target.

Equations

• CategoryTheory.Arrow.rightFunc = CategoryTheory.Comma.snd (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)

@[simp]

theorem CategoryTheory.Arrow.rightFunc_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X✝ ⟶ Y✝) : CategoryTheory.Arrow.rightFunc.map f = f.right

@[simp]

theorem CategoryTheory.Arrow.rightFunc_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.rightFunc.obj X = X.right

def CategoryTheory.Arrow.leftToRight {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Arrow.leftFunc ⟶ CategoryTheory.Arrow.rightFunc

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

Equations

• CategoryTheory.Arrow.leftToRight = { app := fun (f : CategoryTheory.Arrow C) => f.hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.leftToRight_app {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) : CategoryTheory.Arrow.leftToRight.app f = f.hom

def CategoryTheory.Functor.mapArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow D)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapArrow_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C) : (F.mapArrow.obj a).left = F.obj a.left

@[simp]

theorem CategoryTheory.Functor.mapArrow_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Arrow C} (f : X✝ ⟶ Y✝) : (F.mapArrow.map f).left = F.map f.left

@[simp]

theorem CategoryTheory.Functor.mapArrow_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Arrow C} (f : X✝ ⟶ Y✝) : (F.mapArrow.map f).right = F.map f.right

@[simp]

theorem CategoryTheory.Functor.mapArrow_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C) : (F.mapArrow.obj a).right = F.obj a.right

@[simp]

theorem CategoryTheory.Functor.mapArrow_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C) : (F.mapArrow.obj a).hom = F.map a.hom

def CategoryTheory.Functor.mapArrowFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow D))

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapArrowFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.mapArrowFunctor C D).obj F = F.mapArrow

@[simp]

theorem CategoryTheory.Functor.mapArrowFunctor_map_app_left (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) (f : CategoryTheory.Arrow C) : (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).left = τ.app f.left

@[simp]

theorem CategoryTheory.Functor.mapArrowFunctor_map_app_right (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) (f : CategoryTheory.Arrow C) : (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).right = τ.app f.right

def CategoryTheory.Functor.mapArrowEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Arrow C ≌ CategoryTheory.Arrow D

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.isEquivalence_mapArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : F.mapArrow.IsEquivalence

def CategoryTheory.Arrow.isoOfNatIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (f : CategoryTheory.Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f

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

Equations

• CategoryTheory.Arrow.isoOfNatIso e f = CategoryTheory.Arrow.isoMk (e.app f.left) (e.app f.right) ⋯