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

source

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

Instances For

source

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

Category.{v, max u v} (Arrow T)

Equations

source

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

Inhabited (Arrow T)

Equations

source

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

source

theorem CategoryTheory.Arrow.hom_ext_iff {T : Type u} [Category.{v, u} T] {X Y : Arrow T} {f g : X ⟶ Y} :

f = g ↔ f.left = g.left ∧ f.right = g.right

source

@[simp]

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

(CategoryStruct.id f).left = CategoryStruct.id f.left

source

@[simp]

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

(CategoryStruct.id f).right = CategoryStruct.id f.right

source

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

source

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)

source

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

source

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)

source

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

Instances For

source

@[simp]

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

(mk f).left = X

source

@[simp]

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

(mk f).hom = f

source

@[simp]

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

(mk f).right = Y

source

@[simp]

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

mk f.hom = f

source

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

Function.Injective mk

source

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

source

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

CoeOut (X ⟶ Y) (Arrow T)

Equations

source

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 ⋯))

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

φ₁.left = φ₂.left

source

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

φ₁.right = φ₂.right

source

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)

source

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)

source

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

IsIso sq.left

source

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

IsIso sq.right

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Mono sq.left

source

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

Epi sq.right

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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

Instances For

source

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

source

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

source

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

Functor (Arrow C) C

The functor sending an arrow to its source.

Equations

Instances For

source

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

source

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

source

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

Functor (Arrow C) C

The functor sending an arrow to its target.

Equations

Instances For

source

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

source

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

source

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

Instances For

source

@[simp]

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

leftToRight.app f = f.hom

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

Instances For

source

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

Instances For

source

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

source

@[simp]

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

((equivSigma T) f).fst = f.left

source

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

source

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

source

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

source

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

source

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

Arrow (Discrete S) ≃ S

The equivalence Arrow (Discrete S) ≃ S.

Equations

Instances For

source

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.

Documentation

Mathlib.CategoryTheory.Comma.Arrow

The category of arrows #

Tags #