The category of arrows #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
We also define the typeclass has_lift, representing a choice of a lift
of a commutative square (that is, a diagonal morphism making the two triangles commute).
Tags #
comma, arrow
@[protected, instance]
The arrow category of T has as objects all morphisms in T and as morphisms commutative
squares in T.
Equations
- category_theory.arrow T = category_theory.comma (𝟭 T) (𝟭 T)
@[protected, instance]
Equations
- category_theory.arrow.inhabited T = {default := (λ (this : category_theory.comma (𝟭 T) (𝟭 T)), this) inhabited.default}
@[simp]
theorem
category_theory.arrow.id_left
{T : Type u}
[category_theory.category T]
(f : category_theory.arrow T) :
@[simp]
theorem
category_theory.arrow.id_right
{T : Type u}
[category_theory.category T]
(f : category_theory.arrow T) :
@[simp]
theorem
category_theory.arrow.mk_right
{T : Type u}
[category_theory.category T]
{X Y : T}
(f : X ⟶ Y) :
(category_theory.arrow.mk f).right = Y
An object in the arrow category is simply a morphism in T.
@[simp]
theorem
category_theory.arrow.mk_hom
{T : Type u}
[category_theory.category T]
{X Y : T}
(f : X ⟶ Y) :
(category_theory.arrow.mk f).hom = f
@[simp]
theorem
category_theory.arrow.mk_left
{T : Type u}
[category_theory.category T]
{X Y : T}
(f : X ⟶ Y) :
(category_theory.arrow.mk f).left = X
@[simp]
theorem
category_theory.arrow.mk_eq
{T : Type u}
[category_theory.category T]
(f : category_theory.arrow T) :
theorem
category_theory.arrow.mk_inj
{T : Type u}
[category_theory.category T]
(A B : T)
{f g : A ⟶ B} :
@[protected, instance]
def
category_theory.arrow.has_coe
{T : Type u}
[category_theory.category T]
{X Y : T} :
has_coe (X ⟶ Y) (category_theory.arrow T)
Equations
@[simp]
theorem
category_theory.arrow.hom_mk_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
{u : f.left ⟶ g.left}
{v : f.right ⟶ g.right}
(w : u ≫ g.hom = f.hom ≫ v) :
@[simp]
theorem
category_theory.arrow.hom_mk_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
{u : f.left ⟶ g.left}
{v : f.right ⟶ g.right}
(w : u ≫ g.hom = f.hom ≫ v) :
def
category_theory.arrow.hom_mk'
{T : Type u}
[category_theory.category T]
{X Y : T}
{f : X ⟶ Y}
{P Q : T}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(w : u ≫ g = f ≫ v) :
We can also build a morphism in the arrow category out of any commutative square in T.
@[simp]
theorem
category_theory.arrow.hom_mk'_right
{T : Type u}
[category_theory.category T]
{X Y : T}
{f : X ⟶ Y}
{P Q : T}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(w : u ≫ g = f ≫ v) :
@[simp]
theorem
category_theory.arrow.hom_mk'_left
{T : Type u}
[category_theory.category T]
{X Y : T}
{f : X ⟶ Y}
{P Q : T}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(w : u ≫ g = f ≫ v) :
@[simp]
theorem
category_theory.arrow.w
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g) :
@[simp]
theorem
category_theory.arrow.w_mk_right
{T : Type u}
[category_theory.category T]
{f : category_theory.arrow T}
{X Y : T}
{g : X ⟶ Y}
(sq : f ⟶ category_theory.arrow.mk g) :
@[simp]
theorem
category_theory.arrow.w_mk_right_assoc
{T : Type u}
[category_theory.category T]
{f : category_theory.arrow T}
{X Y : T}
{g : X ⟶ Y}
(sq : f ⟶ category_theory.arrow.mk g)
{X' : T}
(f' : Y ⟶ X') :
theorem
category_theory.arrow.is_iso_of_iso_left_of_is_iso_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(ff : f ⟶ g)
[category_theory.is_iso ff.left]
[category_theory.is_iso ff.right] :
def
category_theory.arrow.iso_mk
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(l : f.left ≅ g.left)
(r : f.right ≅ g.right)
(h : l.hom ≫ g.hom = f.hom ≫ r.hom) :
f ≅ g
Create an isomorphism between arrows, by providing isomorphisms between the domains and codomains, and a proof that the square commutes.
Equations
theorem
category_theory.arrow.hom.congr_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
{φ₁ φ₂ : f ⟶ g}
(h : φ₁ = φ₂) :
theorem
category_theory.arrow.hom.congr_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
{φ₁ φ₂ : f ⟶ g}
(h : φ₁ = φ₂) :
theorem
category_theory.arrow.iso_w
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(e : f ≅ g) :
theorem
category_theory.arrow.iso_w'
{T : Type u}
[category_theory.category T]
{W X Y Z : T}
{f : W ⟶ X}
{g : Y ⟶ Z}
(e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) :
@[protected, instance]
def
category_theory.arrow.is_iso_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
@[protected, instance]
def
category_theory.arrow.is_iso_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
@[simp]
theorem
category_theory.arrow.inv_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
(category_theory.inv sq).left = category_theory.inv sq.left
@[simp]
theorem
category_theory.arrow.inv_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
@[simp]
theorem
category_theory.arrow.left_hom_inv_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
theorem
category_theory.arrow.inv_left_hom_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.is_iso sq] :
@[protected, instance]
def
category_theory.arrow.mono_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.mono sq] :
@[protected, instance]
def
category_theory.arrow.epi_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.epi sq] :
@[simp]
theorem
category_theory.arrow.square_to_iso_invert
{T : Type u}
[category_theory.category T]
(i : category_theory.arrow T)
{X Y : T}
(p : X ≅ Y)
(sq : i ⟶ category_theory.arrow.mk p.hom) :
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
category_theory.arrow.square_from_iso_invert
{T : Type u}
[category_theory.category T]
{X Y : T}
(i : X ≅ Y)
(p : category_theory.arrow T)
(sq : category_theory.arrow.mk i.hom ⟶ p) :
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
category_theory.arrow.square_to_snd_right
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{i : category_theory.arrow C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(sq : i ⟶ category_theory.arrow.mk (f ≫ g)) :
@[simp]
theorem
category_theory.arrow.square_to_snd_left
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{i : category_theory.arrow C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(sq : i ⟶ category_theory.arrow.mk (f ≫ g)) :
(category_theory.arrow.square_to_snd sq).left = sq.left ≫ f
def
category_theory.arrow.square_to_snd
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{i : category_theory.arrow C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(sq : i ⟶ category_theory.arrow.mk (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
@[simp]
theorem
category_theory.arrow.left_func_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (𝟭 C) (𝟭 C))
(f : _x ⟶ _x_1) :
The functor sending an arrow to its source.
Equations
@[simp]
theorem
category_theory.arrow.left_func_obj
{C : Type u}
[category_theory.category C]
(X : category_theory.comma (𝟭 C) (𝟭 C)) :
The functor sending an arrow to its target.
Equations
@[simp]
theorem
category_theory.arrow.right_func_obj
{C : Type u}
[category_theory.category C]
(X : category_theory.comma (𝟭 C) (𝟭 C)) :
@[simp]
theorem
category_theory.arrow.right_func_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (𝟭 C) (𝟭 C))
(f : _x ⟶ _x_1) :
The natural transformation from left_func to right_func, given by the arrow itself.
Equations
- category_theory.arrow.left_to_right = {app := λ (f : category_theory.arrow C), f.hom, naturality' := _}
@[simp]
theorem
category_theory.arrow.left_to_right_app
{C : Type u}
[category_theory.category C]
(f : category_theory.arrow C) :
@[simp]
theorem
category_theory.functor.map_arrow_obj_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a : category_theory.arrow C) :
@[simp]
theorem
category_theory.functor.map_arrow_map_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a b : category_theory.arrow C)
(f : a ⟶ b) :
def
category_theory.functor.map_arrow
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
A functor C ⥤ D induces a functor between the corresponding arrow categories.
@[simp]
theorem
category_theory.functor.map_arrow_map_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a b : category_theory.arrow C)
(f : a ⟶ b) :
@[simp]
theorem
category_theory.functor.map_arrow_obj_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a : category_theory.arrow C) :
@[simp]
theorem
category_theory.functor.map_arrow_obj_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(a : category_theory.arrow C) :
def
category_theory.arrow.iso_of_nat_iso
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
{F G : C ⥤ D}
(e : F ≅ G)
(f : category_theory.arrow C) :
The images of f : arrow C by two isomorphic functors F : C ⥤ D are
isomorphic arrows in D.
Equations
- category_theory.arrow.iso_of_nat_iso e f = category_theory.arrow.iso_mk (e.app f.left) (e.app f.right) _