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) [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) [Category.{v, u} T] : Category.{v, max u v} (Arrow T)

Equations

• CategoryTheory.instCategoryArrow T = CategoryTheory.commaCategory

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

Equations

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

theorem CategoryTheory.Arrow.hom_ext {T : Type u} [Category.{v, u} T] {X Y : 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} [Category.{v, u} T] (f : Arrow T) : (CategoryStruct.id f).left = CategoryStruct.id f.left

@[simp]

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

@[simp]

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

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

@[simp]

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

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

def CategoryTheory.Arrow.mk {T : Type u} [Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : 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} [Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : (mk f).right = Y

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

theorem CategoryTheory.Arrow.mk_eq_mk_iff {T : Type u} [Category.{v, u} T] {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y') : mk f = mk f' ↔ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = CategoryStruct.comp (eqToHom hX) (CategoryStruct.comp f' (eqToHom ⋯))

theorem CategoryTheory.Arrow.ext {T : Type u} [Category.{v, u} T] {f g : Arrow T} (h₁ : f.left = g.left) (h₂ : f.right = g.right) (h₃ : f.hom = CategoryStruct.comp (eqToHom h₁) (CategoryStruct.comp g.hom (eqToHom ⋯))) : f = g

@[simp]

theorem CategoryTheory.Arrow.arrow_mk_comp_eqToHom {T : Type u} [Category.{v, u} T] {X Y Y' : T} (f : X ⟶ Y) (h : Y = Y') : mk (CategoryStruct.comp f (eqToHom h)) = mk f

@[simp]

theorem CategoryTheory.Arrow.arrow_mk_eqToHom_comp {T : Type u} [Category.{v, u} T] {X' X Y : T} (f : X ⟶ Y) (h : X' = X) : mk (CategoryStruct.comp (eqToHom h) f) = mk f

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.Arrow.isoMk' {T : Type u} [Category.{v, u} T] {W X Y Z : T} (f : W ⟶ X) (g : Y ⟶ Z) (e₁ : W ≅ Y) (e₂ : X ≅ Z) (h : CategoryStruct.comp e₁.hom g = CategoryStruct.comp f e₂.hom := by aesop_cat) : mk f ≅ 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} [Category.{v, u} T] {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left

@[simp]

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

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

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

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

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

theorem CategoryTheory.Arrow.isIso_of_isIso {T : Type u} [Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) [IsIso sq] [IsIso f] : IsIso g.hom

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

theorem CategoryTheory.Arrow.isIso_iff_isIso_of_isIso {T : Type u} [Category.{v, u} T] {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (sq : mk f ⟶ mk g) [IsIso sq] : IsIso f ↔ IsIso g

theorem CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIso {T : Type u} [Category.{v, u} T] {Y Z : T} {f : Arrow T} {g : Y ⟶ Z} (sq : f ⟶ mk g) [IsIso sq] : IsIso f.hom ↔ IsIso g

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Arrow.square_to_iso_invert {T : Type u} [Category.{v, u} T] (i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ mk p.hom) : CategoryStruct.comp i.hom (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} [Category.{v, u} T] {X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : mk i.hom ⟶ p) : CategoryStruct.comp i.inv (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} [Category.{v, u} C] {X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ mk (CategoryStruct.comp f g)) : i ⟶ 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_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ mk (CategoryStruct.comp f g)) : (squareToSnd sq).right = sq.right

@[simp]

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

def CategoryTheory.Arrow.leftFunc {C : Type u} [Category.{v, u} C] : Functor (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_obj {C : Type u} [Category.{v, u} C] (X : Comma (Functor.id C) (Functor.id C)) : leftFunc.obj X = X.left

@[simp]

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

def CategoryTheory.Arrow.rightFunc {C : Type u} [Category.{v, u} C] : Functor (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} [Category.{v, u} C] {X✝ Y✝ : Comma (Functor.id C) (Functor.id C)} (f : X✝ ⟶ Y✝) : rightFunc.map f = f.right

@[simp]

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

def CategoryTheory.Arrow.leftToRight {C : Type u} [Category.{v, u} C] : leftFunc ⟶ 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} [Category.{v, u} C] (f : Arrow C) : leftToRight.app f = f.hom

def CategoryTheory.Functor.mapArrow {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Functor (Arrow C) (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 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (a : Arrow C) : F.mapArrow.obj a = Arrow.mk (F.map a.hom)

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.mapArrowFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (Functor C D) (Functor (Arrow C) (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_map_app_left (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Functor C D} (τ : X✝ ⟶ Y✝) (f : Arrow C) : (((mapArrowFunctor C D).map τ).app f).left = τ.app ((Functor.id C).obj f.left)

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.mapArrowEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Arrow C ≌ 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.

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

def CategoryTheory.Arrow.isoOfNatIso {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F G : Functor C D} (e : F ≅ G) (f : 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) ⋯

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

Arrow T is equivalent to a sigma type.

Equations

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

@[simp]

theorem CategoryTheory.Arrow.equivSigma_symm_apply_right (T : Type u) [Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((equivSigma T).symm x).right = x.snd.fst

@[simp]

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

@[simp]

theorem CategoryTheory.Arrow.equivSigma_apply_fst (T : Type u) [Category.{v, u} T] (f : Arrow T) : ((equivSigma T) f).fst = f.left

@[simp]

theorem CategoryTheory.Arrow.equivSigma_symm_apply_left (T : Type u) [Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((equivSigma T).symm x).left = x.fst

@[simp]

theorem CategoryTheory.Arrow.equivSigma_apply_snd_fst (T : Type u) [Category.{v, u} T] (f : Arrow T) : ((equivSigma T) f).snd.fst = f.right

@[simp]

theorem CategoryTheory.Arrow.equivSigma_symm_apply_hom (T : Type u) [Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((equivSigma T).symm x).hom = x.snd.snd

def CategoryTheory.Arrow.discreteEquiv (S : Type u) : Arrow (Discrete S) ≃ S

The equivalence Arrow (Discrete S) ≃ S.

Equations

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

theorem CategoryTheory.Arrow.functor_ext {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F G : Functor C D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)) : F = G

Extensionality lemma for functors C ⥤ D which uses as an assumption that the induced maps Arrow C → Arrow D coincide.