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
The arrow category of T has as objects all morphisms in T and as morphisms commutative
squares in T.
Equations
Equations
- CategoryTheory.instCategoryArrow T = CategoryTheory.commaCategory
instance
CategoryTheory.Arrow.inhabited
(T : Type u)
[CategoryTheory.Category.{v, u} T]
[Inhabited 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 : CategoryTheory.Arrow T}
{Y : CategoryTheory.Arrow T}
(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}
[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
theorem
CategoryTheory.Arrow.comp_left_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : CategoryTheory.Arrow T}
{Y : CategoryTheory.Arrow T}
{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_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : CategoryTheory.Arrow T}
{Y : CategoryTheory.Arrow T}
{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_right_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : CategoryTheory.Arrow T}
{Y : CategoryTheory.Arrow T}
{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)
@[simp]
theorem
CategoryTheory.Arrow.comp_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : CategoryTheory.Arrow T}
{Y : CategoryTheory.Arrow T}
{Z : CategoryTheory.Arrow T}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
theorem
CategoryTheory.Arrow.mk_hom
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{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 : T}
{Y : T}
(f : X ⟶ Y)
:
(CategoryTheory.Arrow.mk f).left = X
@[simp]
theorem
CategoryTheory.Arrow.mk_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{Y : T}
(f : X ⟶ Y)
:
(CategoryTheory.Arrow.mk f).right = Y
def
CategoryTheory.Arrow.mk
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{Y : T}
(f : X ⟶ Y)
:
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_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 : T)
(B : T)
:
Function.Injective CategoryTheory.Arrow.mk
theorem
CategoryTheory.Arrow.mk_inj
{T : Type u}
[CategoryTheory.Category.{v, u} T]
(A : T)
(B : T)
{f : A ⟶ B}
{g : A ⟶ B}
:
instance
CategoryTheory.Arrow.instCoeOutHomToQuiverToCategoryStructArrow
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{Y : T}
:
CoeOut (X ⟶ Y) (CategoryTheory.Arrow T)
Equations
- CategoryTheory.Arrow.instCoeOutHomToQuiverToCategoryStructArrow = { coe := CategoryTheory.Arrow.mk }
@[simp]
theorem
CategoryTheory.Arrow.homMk_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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 : CategoryTheory.Arrow T}
{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]
{f : CategoryTheory.Arrow T}
{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]
{X : T}
{Y : T}
{f : X ⟶ Y}
{P : T}
{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.homMk'_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{Y : T}
{f : X ⟶ Y}
{P : T}
{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
def
CategoryTheory.Arrow.homMk'
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{X : T}
{Y : T}
{f : X ⟶ Y}
{P : T}
{Q : T}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v)
:
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.w_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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_mk_right_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{X : T}
{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)
@[simp]
theorem
CategoryTheory.Arrow.w_mk_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{X : T}
{Y : T}
{g : X ⟶ Y}
(sq : f ⟶ CategoryTheory.Arrow.mk g)
:
CategoryTheory.CategoryStruct.comp sq.left g = CategoryTheory.CategoryStruct.comp f.hom sq.right
theorem
CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(ff : f ⟶ g)
[CategoryTheory.IsIso ff.left]
[CategoryTheory.IsIso ff.right]
:
@[simp]
theorem
CategoryTheory.Arrow.isoMk_inv_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(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✝)
:
(CategoryTheory.Arrow.isoMk l r h).inv.left = l.inv
@[simp]
theorem
CategoryTheory.Arrow.isoMk_hom_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(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✝)
:
(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 : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(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✝)
:
(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 : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(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✝)
:
(CategoryTheory.Arrow.isoMk l r h).inv.right = r.inv
def
CategoryTheory.Arrow.isoMk
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(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.
Equations
- CategoryTheory.Arrow.isoMk l r h = CategoryTheory.Comma.isoMk l r h
@[inline, reducible]
abbrev
CategoryTheory.Arrow.isoMk'
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{W : T}
{X : T}
{Y : T}
{Z : T}
(f : W ⟶ X)
(g : Y ⟶ Z)
(e₁ : W ≅ Y)
(e₂ : X ≅ Z)
(h : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom g = CategoryTheory.CategoryStruct.comp f e₂.hom) _auto✝)
:
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 : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
{φ₁ : f ⟶ g}
{φ₂ : f ⟶ g}
(h : φ₁ = φ₂)
:
φ₁.left = φ₂.left
@[simp]
theorem
CategoryTheory.Arrow.hom.congr_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
{φ₁ : f ⟶ g}
{φ₂ : f ⟶ g}
(h : φ₁ = φ₂)
:
φ₁.right = φ₂.right
theorem
CategoryTheory.Arrow.iso_w
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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 : T}
{X : T}
{Y : T}
{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)
instance
CategoryTheory.Arrow.isIso_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
CategoryTheory.IsIso sq.left
Equations
- ⋯ = ⋯
instance
CategoryTheory.Arrow.isIso_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
CategoryTheory.IsIso sq.right
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Arrow.inv_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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 : CategoryTheory.Arrow T}
{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 : CategoryTheory.Arrow T}
{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 : CategoryTheory.Arrow T}
{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
instance
CategoryTheory.Arrow.mono_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(sq : f ⟶ g)
[CategoryTheory.Mono sq]
:
CategoryTheory.Mono sq.left
Equations
- ⋯ = ⋯
instance
CategoryTheory.Arrow.epi_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{g : CategoryTheory.Arrow T}
(sq : f ⟶ g)
[CategoryTheory.Epi sq]
:
CategoryTheory.Epi sq.right
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Arrow.hom_inv_id_left_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.hom_inv_id_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.inv_hom_id_left_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.inv_hom_id_left
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.hom_inv_id_right_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.hom_inv_id_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.inv_hom_id_right_assoc
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.inv_hom_id_right
{T : Type u}
[CategoryTheory.Category.{v, u} T]
{f : CategoryTheory.Arrow T}
{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.square_to_iso_invert
{T : Type u}
[CategoryTheory.Category.{v, u} T]
(i : CategoryTheory.Arrow T)
{X : T}
{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 : T}
{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.
@[simp]
theorem
CategoryTheory.Arrow.squareToSnd_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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
@[simp]
theorem
CategoryTheory.Arrow.squareToSnd_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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
def
CategoryTheory.Arrow.squareToSnd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{i : CategoryTheory.Arrow C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f 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.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
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.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
@[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
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.leftToRight_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : CategoryTheory.Arrow C)
:
CategoryTheory.Arrow.leftToRight.app f = f.hom
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.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)
:
((CategoryTheory.Functor.mapArrow F).obj a).right = F.obj a.right
@[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)
:
((CategoryTheory.Functor.mapArrow F).obj a).left = F.obj a.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), ((CategoryTheory.Functor.mapArrow F).map f).right = F.map f.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)
:
((CategoryTheory.Functor.mapArrow F).obj a).hom = F.map a.hom
@[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), ((CategoryTheory.Functor.mapArrow F).map f).left = F.map f.left
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)
:
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.
Instances For
@[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)
:
@[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.mapArrowFunctor
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} 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.
def
CategoryTheory.Functor.mapArrowEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ 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.isEquivalenceMapArrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence F]
:
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 : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(e : F ≅ G)
(f : CategoryTheory.Arrow C)
:
(CategoryTheory.Functor.mapArrow F).obj f ≅ (CategoryTheory.Functor.mapArrow G).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) ⋯