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.
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
@[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)
@[instance]
Equations
- category_theory.arrow.inhabited T = {default := (λ (this : category_theory.comma (𝟭 T) (𝟭 T)), this) (default (category_theory.comma (𝟭 T) (𝟭 T)))}
@[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.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) :
def
category_theory.arrow.hom_mk
{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) :
f ⟶ g
A morphism in the arrow category is a commutative square connecting two objects of the arrow category.
@[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) :
theorem
category_theory.arrow.w
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g) :
theorem
category_theory.arrow.lift_struct.ext_iff
{T : Type u}
{_inst_1 : category_theory.category T}
{f g : category_theory.arrow T}
{sq : f ⟶ g}
(x y : category_theory.arrow.lift_struct sq) :
theorem
category_theory.arrow.lift_struct.ext
{T : Type u}
{_inst_1 : category_theory.category T}
{f g : category_theory.arrow T}
{sq : f ⟶ g}
(x y : category_theory.arrow.lift_struct sq)
(h : x.lift = y.lift) :
x = y
@[ext]
structure
category_theory.arrow.lift_struct
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g) :
Type v
A lift of a commutative square is a diagonal morphism making the two triangles commute.
@[instance]
@[class]
structure
category_theory.arrow.has_lift
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g) :
Prop
- exists_lift : nonempty (category_theory.arrow.lift_struct sq)
has_lift sq says that there is some lift_struct sq, i.e., that it is possible to find a
diagonal morphism making the two triangles commute.
Instances
theorem
category_theory.arrow.has_lift.mk
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
{sq : f ⟶ g}
(s : category_theory.arrow.lift_struct sq) :
def
category_theory.arrow.has_lift.struct
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.arrow.has_lift sq] :
Given has_lift sq, obtain a lift.
def
category_theory.arrow.lift
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.arrow.has_lift sq] :
If there is a lift of a commutative square sq, we can access it by saying lift sq.
theorem
category_theory.arrow.lift.fac_left
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.arrow.has_lift sq] :
f.hom ≫ category_theory.arrow.lift sq = sq.left
theorem
category_theory.arrow.lift.fac_right
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.arrow.has_lift sq] :
category_theory.arrow.lift sq ≫ g.hom = sq.right
@[simp]
theorem
category_theory.arrow.lift_mk'_left_assoc
{T : Type u}
[category_theory.category T]
{X Y P Q : T}
{f : X ⟶ Y}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(h : u ≫ g = f ≫ v)
[category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)]
{X' : T}
(f' : (category_theory.arrow.mk g).left ⟶ X') :
f ≫ category_theory.arrow.lift (category_theory.arrow.hom_mk' h) ≫ f' = u ≫ f'
@[simp]
theorem
category_theory.arrow.lift_mk'_left
{T : Type u}
[category_theory.category T]
{X Y P Q : T}
{f : X ⟶ Y}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(h : u ≫ g = f ≫ v)
[category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)] :
@[simp]
theorem
category_theory.arrow.lift_mk'_right
{T : Type u}
[category_theory.category T]
{X Y P Q : T}
{f : X ⟶ Y}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(h : u ≫ g = f ≫ v)
[category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)] :
@[simp]
theorem
category_theory.arrow.lift_mk'_right_assoc
{T : Type u}
[category_theory.category T]
{X Y P Q : T}
{f : X ⟶ Y}
{g : P ⟶ Q}
{u : X ⟶ P}
{v : Y ⟶ Q}
(h : u ≫ g = f ≫ v)
[category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)]
{X' : T . "obviously"}
(f' : Q ⟶ X') :
category_theory.arrow.lift (category_theory.arrow.hom_mk' h) ≫ g ≫ f' = v ≫ f'
@[instance]
def
category_theory.arrow.subsingleton_lift_struct_of_epi
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.epi f.hom] :
@[instance]
def
category_theory.arrow.subsingleton_lift_struct_of_mono
{T : Type u}
[category_theory.category T]
{f g : category_theory.arrow T}
(sq : f ⟶ g)
[category_theory.mono g.hom] :
@[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) :