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)

def CategoryTheory.Arrow.Hom {T : Type u} [Category.{v, u} T] (f g : Arrow T) : Type v

The type of morphisms in the category Arrow T.

Equations

• f.Hom g = CategoryTheory.CommaMorphism f g

@[implicit_reducible]

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

Equations

• CategoryTheory.instQuiverArrow = { Hom := CategoryTheory.Arrow.Hom }

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Arrow.left {T : Type u} [Category.{v, u} T] (X : Arrow T) : T

The left object of an arrow.

Equations

• X.left = X.left

@[reducible, inline]

abbrev CategoryTheory.Arrow.right {T : Type u} [Category.{v, u} T] (X : Arrow T) : T

The right object of an arrow.

Equations

• X.right = X.right

@[reducible, inline]

abbrev CategoryTheory.Arrow.hom {T : Type u} [Category.{v, u} T] (X : Arrow T) : X.left ⟶ X.right

Given X : Arrow T, this is the morphism X.left ⟶ X.right.

Equations

• X.hom = X.hom

@[reducible, inline]

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

The left part of a morphism in the category of arrows.

Equations

• CategoryTheory.Arrow.Hom.left f = f.left

@[reducible, inline]

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

The right part of a morphism in the category of arrows.

Equations

• CategoryTheory.Arrow.Hom.right f = f.right

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

theorem CategoryTheory.Arrow.hom_ext_iff {T : Type u} [Category.{v, u} T] {X Y : Arrow T} {f g : X ⟶ Y} : f = g ↔ Hom.left f = Hom.left g ∧ Hom.right f = Hom.right g

@[simp]

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

@[simp]

theorem CategoryTheory.Arrow.id_right {T : Type u} [Category.{v, u} T] (f : Arrow T) : Hom.right (CategoryStruct.id f) = 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) : Hom.left (CategoryStruct.comp f g) = CategoryStruct.comp (Hom.left f) (Hom.left g)

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 (Hom.left (CategoryStruct.comp f g)) h = CategoryStruct.comp (Hom.left f) (CategoryStruct.comp (Hom.left g) 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) : Hom.right (CategoryStruct.comp f g) = CategoryStruct.comp (Hom.right f) (Hom.right g)

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 (Hom.right (CategoryStruct.comp f g)) h = CategoryStruct.comp (Hom.right f) (CategoryStruct.comp (Hom.right g) 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_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_right {T : Type u} [Category.{v, u} T] {X Y : T} (f : X ⟶ Y) : (mk f).right = Y

@[simp]

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

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

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

@[implicit_reducible]

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 }

@[simp]

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

@[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 (Hom.left sq) (CategoryStruct.comp g.hom h) = CategoryStruct.comp f.hom (CategoryStruct.comp (Hom.right sq) h)

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

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

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

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

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

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 (Hom.left e.inv) (CategoryStruct.comp f (Hom.right e.hom))

theorem CategoryTheory.Arrow.eqToHom_left {T : Type u} [Category.{v, u} T] {X Y : Arrow T} (h : X = Y) : Hom.left (eqToHom h) = eqToHom ⋯

theorem CategoryTheory.Arrow.eqToHom_right {T : Type u} [Category.{v, u} T] {X Y : Arrow T} (h : X = Y) : Hom.right (eqToHom h) = eqToHom ⋯

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 cat_disch) : 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_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 cat_disch) : (homMk u v w).right = v

@[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 cat_disch) : (homMk u v w).left = u

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 cat_disch) : 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 cat_disch) : (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 cat_disch) : (homMk' u v w).left = u

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

theorem CategoryTheory.Arrow.w_mk_left_assoc {T : Type u} [Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) {Z : T} (h : g.right ⟶ Z) : CategoryStruct.comp (Hom.left sq) (CategoryStruct.comp g.hom h) = CategoryStruct.comp f (CategoryStruct.comp (Hom.right sq) 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 (Hom.left sq) g = CategoryStruct.comp f.hom (Hom.right sq)

@[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 (Hom.left sq) (CategoryStruct.comp g h) = CategoryStruct.comp f.hom (CategoryStruct.comp (Hom.right sq) h)

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

theorem CategoryTheory.Arrow.w_mk_assoc {T : Type u} [Category.{v, u} T] {X Y X' Y' : T} {f : X ⟶ Y} {g : X' ⟶ Y'} (sq : mk f ⟶ mk g) {Z : T} (h : Y' ⟶ Z) : CategoryStruct.comp (Hom.left sq) (CategoryStruct.comp g h) = CategoryStruct.comp f (CategoryStruct.comp (Hom.right sq) 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 (Hom.left ff)] [IsIso (Hom.right ff)] : 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 cat_disch) : 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 cat_disch) : (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 cat_disch) : (isoMk l r h).hom.right = r.hom

@[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 cat_disch) : (isoMk l r h).inv.left = l.inv

@[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 cat_disch) : (isoMk l r h).inv.right = r.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 cat_disch) : 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

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

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

theorem CategoryTheory.Arrow.isIso_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_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] : Hom.left (inv sq) = inv (Hom.left sq)

@[simp]

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

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 (Hom.left sq) (CategoryStruct.comp g.hom (inv (Hom.right sq))) = 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 (Hom.left sq)) (CategoryStruct.comp f.hom (Hom.right sq)) = g.hom

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

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

@[simp]

theorem CategoryTheory.Arrow.hom_inv_id_left {T : Type u} [Category.{v, u} T] {f g : Arrow T} (e : f ≅ g) : CategoryStruct.comp (Hom.left e.hom) (Hom.left e.inv) = 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 (Hom.left e.hom) (CategoryStruct.comp (Hom.left e.inv) 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 (Hom.left e.inv) (Hom.left e.hom) = 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 (Hom.left e.inv) (CategoryStruct.comp (Hom.left e.hom) 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 (Hom.right e.hom) (Hom.right e.inv) = 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 (Hom.right e.hom) (CategoryStruct.comp (Hom.right e.inv) 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 (Hom.right e.inv) (Hom.right e.hom) = 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 (Hom.right e.inv) (CategoryStruct.comp (Hom.right e.hom) 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 (Hom.right sq) p.inv) = Hom.left sq

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 (Hom.left sq) p.hom) = Hom.right sq

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 = CategoryTheory.Arrow.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) f) (CategoryTheory.Arrow.Hom.right sq) ⋯

@[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 (Hom.left sq) f

@[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 = Hom.right sq

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

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

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 {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 = Arrow.homMk (F.map (Arrow.Hom.left f)) (F.map (Arrow.Hom.right f)) ⋯

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_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

@[simp]

theorem CategoryTheory.Functor.mapArrowFunctor_map_app (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 = Arrow.homMk (τ.app f.left) (τ.app f.right) ⋯

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.

@[simp]

theorem CategoryTheory.Functor.mapArrowEquivalence_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (mapArrowEquivalence e).inverse = e.inverse.mapArrow

@[simp]

theorem CategoryTheory.Functor.mapArrowEquivalence_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (mapArrowEquivalence e).counitIso = (mapArrowFunctor D D).mapIso e.counitIso

@[simp]

theorem CategoryTheory.Functor.mapArrowEquivalence_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (mapArrowEquivalence e).unitIso = (mapArrowFunctor C C).mapIso e.unitIso

@[simp]

theorem CategoryTheory.Functor.mapArrowEquivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (mapArrowEquivalence e).functor = e.functor.mapArrow

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.{v_1, u_1} C] [Category.{v_2, 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_apply_fst (T : Type u) [Category.{v, u} T] (f : Arrow T) : ((equivSigma T) f).fst = f.left

@[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_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

@[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_right (T : Type u) [Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((equivSigma T).symm x).right = x.snd.fst

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.{v_1, u_1} C] [Category.{v_2, 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.