Comma categories
A comma category is a construction in category theory, which builds a category out of two functors
with a common codomain. Specifically, for functors L : A ⥤ T and R : B ⥤ T, an object in
comma L R is a morphism hom : L.obj left ⟶ R.obj right for some objects left : A and
right : B, and a morphism in comma L R between hom : L.obj left ⟶ R.obj right and
hom' : L.obj left' ⟶ R.obj right' is a commutative square
L.obj left ⟶ L.obj left' | | hom | | hom' ↓ ↓ R.obj right ⟶ R.obj right',
where the top and bottom morphism come from morphisms left ⟶ left' and right ⟶ right',
respectively.
Main definitions
comma L R: the comma category of the functorsLandR.over X: the over category of the objectX(developed inover.lean).under X: the under category of the objectX(also developed inover.lean).arrow T: the arrow category of the categoryT(developed inarrow.lean).
References
- https://ncatlab.org/nlab/show/comma+category
Tags
comma, slice, coslice, over, under, arrow
structure
category_theory.comma
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T] :
The objects of the comma category are triples of an object left : A, an object
right : B and a morphism hom : L.obj left ⟶ R.obj right.
@[instance]
def
category_theory.comma.inhabited
{T : Type u₃}
[category_theory.category T]
[inhabited T] :
inhabited (category_theory.comma (𝟭 T) (𝟭 T))
Equations
- category_theory.comma.inhabited = {default := {left := inhabited.default T _inst_4, right := inhabited.default T _inst_4, hom := 𝟙 (inhabited.default T)}}
theorem
category_theory.comma_morphism.ext
{A : Type u₁}
{_inst_1 : category_theory.category A}
{B : Type u₂}
{_inst_2 : category_theory.category B}
{T : Type u₃}
{_inst_3 : category_theory.category T}
{L : A ⥤ T}
{R : B ⥤ T}
{X Y : category_theory.comma L R}
(x y : category_theory.comma_morphism X Y) :
theorem
category_theory.comma_morphism.ext_iff
{A : Type u₁}
{_inst_1 : category_theory.category A}
{B : Type u₂}
{_inst_2 : category_theory.category B}
{T : Type u₃}
{_inst_3 : category_theory.category T}
{L : A ⥤ T}
{R : B ⥤ T}
{X Y : category_theory.comma L R}
(x y : category_theory.comma_morphism X Y) :
@[ext]
structure
category_theory.comma_morphism
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T} :
category_theory.comma L R → category_theory.comma L R → Type (max v₁ v₂)
- left : (X.left ⟶ Y.left) . "obviously"
- right : (X.right ⟶ Y.right) . "obviously"
- w' : L.map c.left ≫ Y.hom = X.hom ≫ R.map c.right . "obviously"
A morphism between two objects in the comma category is a commutative square connecting the
morphisms coming from the two objects using morphisms in the image of the functors L and R.
@[instance]
def
category_theory.comma_morphism.inhabited
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
[inhabited (category_theory.comma L R)] :
Equations
- category_theory.comma_morphism.inhabited = {default := {left := 𝟙 (inhabited.default (category_theory.comma L R)).left, right := 𝟙 (inhabited.default (category_theory.comma L R)).right, w' := _}}
@[instance]
def
category_theory.comma_category
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T} :
Equations
- category_theory.comma_category = {to_category_struct := {to_has_hom := {hom := category_theory.comma_morphism R}, id := λ (X : category_theory.comma L R), {left := 𝟙 X.left, right := 𝟙 X.right, w' := _}, comp := λ (X Y Z : category_theory.comma L R) (f : X ⟶ Y) (g : Y ⟶ Z), {left := f.left ≫ g.left, right := f.right ≫ g.right, w' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.comma.id_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
{X : category_theory.comma L R} :
@[simp]
theorem
category_theory.comma.id_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
{X : category_theory.comma L R} :
@[simp]
theorem
category_theory.comma.comp_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
{X Y Z : category_theory.comma L R}
{f : X ⟶ Y}
{g : Y ⟶ Z} :
@[simp]
theorem
category_theory.comma.comp_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
{X Y Z : category_theory.comma L R}
{f : X ⟶ Y}
{g : Y ⟶ Z} :
def
category_theory.comma.fst
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma L R ⥤ A
The functor sending an object X in the comma category to X.left.
Equations
- category_theory.comma.fst L R = {obj := λ (X : category_theory.comma L R), X.left, map := λ (_x _x_1 : category_theory.comma L R) (f : _x ⟶ _x_1), f.left, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.comma.fst_map
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(_x _x_1 : category_theory.comma L R)
(f : _x ⟶ _x_1) :
(category_theory.comma.fst L R).map f = f.left
@[simp]
theorem
category_theory.comma.fst_obj
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
(category_theory.comma.fst L R).obj X = X.left
def
category_theory.comma.snd
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma L R ⥤ B
The functor sending an object X in the comma category to X.right.
Equations
- category_theory.comma.snd L R = {obj := λ (X : category_theory.comma L R), X.right, map := λ (_x _x_1 : category_theory.comma L R) (f : _x ⟶ _x_1), f.right, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.comma.snd_obj
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
(category_theory.comma.snd L R).obj X = X.right
@[simp]
theorem
category_theory.comma.snd_map
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(_x _x_1 : category_theory.comma L R)
(f : _x ⟶ _x_1) :
(category_theory.comma.snd L R).map f = f.right
@[simp]
theorem
category_theory.comma.nat_trans_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
(category_theory.comma.nat_trans L R).app X = X.hom
def
category_theory.comma.nat_trans
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma.fst L R ⋙ L ⟶ category_theory.comma.snd L R ⋙ R
We can interpret the commutative square constituting a morphism in the comma category as a
natural transformation between the functors fst ⋙ L and snd ⋙ R from the comma category
to T, where the components are given by the morphism that constitutes an object of the comma
category.
Equations
- category_theory.comma.nat_trans L R = {app := λ (X : category_theory.comma L R), X.hom, naturality' := _}
@[simp]
theorem
category_theory.comma.iso_mk_inv_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L₁ : A ⥤ T}
{R₁ : B ⥤ T}
{X Y : category_theory.comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) :
(category_theory.comma.iso_mk l r h).inv.left = l.inv
@[simp]
theorem
category_theory.comma.iso_mk_hom_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L₁ : A ⥤ T}
{R₁ : B ⥤ T}
{X Y : category_theory.comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) :
(category_theory.comma.iso_mk l r h).hom.left = l.hom
@[simp]
theorem
category_theory.comma.iso_mk_hom_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L₁ : A ⥤ T}
{R₁ : B ⥤ T}
{X Y : category_theory.comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) :
(category_theory.comma.iso_mk l r h).hom.right = r.hom
@[simp]
theorem
category_theory.comma.iso_mk_inv_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L₁ : A ⥤ T}
{R₁ : B ⥤ T}
{X Y : category_theory.comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) :
(category_theory.comma.iso_mk l r h).inv.right = r.inv
def
category_theory.comma.iso_mk
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L₁ : A ⥤ T}
{R₁ : B ⥤ T}
{X Y : category_theory.comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right) :
Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.
@[simp]
theorem
category_theory.comma.map_left_map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T}
(l : L₁ ⟶ L₂)
(X Y : category_theory.comma L₂ R)
(f : X ⟶ Y) :
((category_theory.comma.map_left R l).map f).left = f.left
@[simp]
theorem
category_theory.comma.map_left_obj_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T}
(l : L₁ ⟶ L₂)
(X : category_theory.comma L₂ R) :
((category_theory.comma.map_left R l).obj X).left = X.left
@[simp]
theorem
category_theory.comma.map_left_obj_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T}
(l : L₁ ⟶ L₂)
(X : category_theory.comma L₂ R) :
((category_theory.comma.map_left R l).obj X).right = X.right
def
category_theory.comma.map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T} :
(L₁ ⟶ L₂) → category_theory.comma L₂ R ⥤ category_theory.comma L₁ R
A natural transformation L₁ ⟶ L₂ induces a functor comma L₂ R ⥤ comma L₁ R.
@[simp]
theorem
category_theory.comma.map_left_obj_hom
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T}
(l : L₁ ⟶ L₂)
(X : category_theory.comma L₂ R) :
@[simp]
theorem
category_theory.comma.map_left_map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ : A ⥤ T}
(l : L₁ ⟶ L₂)
(X Y : category_theory.comma L₂ R)
(f : X ⟶ Y) :
((category_theory.comma.map_left R l).map f).right = f.right
@[simp]
theorem
category_theory.comma.map_left_id_hom_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_left_id L R).hom.app X).right = 𝟙 ((category_theory.comma.map_left R (𝟙 L)).obj X).right
@[simp]
theorem
category_theory.comma.map_left_id_hom_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_left_id L R).hom.app X).left = 𝟙 ((category_theory.comma.map_left R (𝟙 L)).obj X).left
def
category_theory.comma.map_left_id
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma.map_left R (𝟙 L) ≅ 𝟭 (category_theory.comma L R)
The functor comma L R ⥤ comma L R induced by the identity natural transformation on L is
naturally isomorphic to the identity functor.
Equations
- category_theory.comma.map_left_id L R = {hom := {app := λ (X : category_theory.comma L R), {left := 𝟙 ((category_theory.comma.map_left R (𝟙 L)).obj X).left, right := 𝟙 ((category_theory.comma.map_left R (𝟙 L)).obj X).right, w' := _}, naturality' := _}, inv := {app := λ (X : category_theory.comma L R), {left := 𝟙 ((𝟭 (category_theory.comma L R)).obj X).left, right := 𝟙 ((𝟭 (category_theory.comma L R)).obj X).right, w' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.comma.map_left_id_inv_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_left_id L R).inv.app X).left = 𝟙 ((𝟭 (category_theory.comma L R)).obj X).left
@[simp]
theorem
category_theory.comma.map_left_id_inv_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_left_id L R).inv.app X).right = 𝟙 ((𝟭 (category_theory.comma L R)).obj X).right
@[simp]
theorem
category_theory.comma.map_left_comp_hom_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ L₃ : A ⥤ T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : category_theory.comma L₃ R) :
((category_theory.comma.map_left_comp R l l').hom.app X).right = 𝟙 ((category_theory.comma.map_left R (l ≫ l')).obj X).right
@[simp]
theorem
category_theory.comma.map_left_comp_inv_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ L₃ : A ⥤ T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : category_theory.comma L₃ R) :
((category_theory.comma.map_left_comp R l l').inv.app X).left = 𝟙 ((category_theory.comma.map_left R l' ⋙ category_theory.comma.map_left R l).obj X).left
@[simp]
theorem
category_theory.comma.map_left_comp_inv_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ L₃ : A ⥤ T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : category_theory.comma L₃ R) :
((category_theory.comma.map_left_comp R l l').inv.app X).right = 𝟙 ((category_theory.comma.map_left R l' ⋙ category_theory.comma.map_left R l).obj X).right
def
category_theory.comma.map_left_comp
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ L₃ : A ⥤ T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃) :
The functor comma L₁ R ⥤ comma L₃ R induced by the composition of two natural transformations
l : L₁ ⟶ L₂ and l' : L₂ ⟶ L₃ is naturally isomorphic to the composition of the two functors
induced by these natural transformations.
Equations
- category_theory.comma.map_left_comp R l l' = {hom := {app := λ (X : category_theory.comma L₃ R), {left := 𝟙 ((category_theory.comma.map_left R (l ≫ l')).obj X).left, right := 𝟙 ((category_theory.comma.map_left R (l ≫ l')).obj X).right, w' := _}, naturality' := _}, inv := {app := λ (X : category_theory.comma L₃ R), {left := 𝟙 ((category_theory.comma.map_left R l' ⋙ category_theory.comma.map_left R l).obj X).left, right := 𝟙 ((category_theory.comma.map_left R l' ⋙ category_theory.comma.map_left R l).obj X).right, w' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.comma.map_left_comp_hom_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(R : B ⥤ T)
{L₁ L₂ L₃ : A ⥤ T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : category_theory.comma L₃ R) :
((category_theory.comma.map_left_comp R l l').hom.app X).left = 𝟙 ((category_theory.comma.map_left R (l ≫ l')).obj X).left
@[simp]
theorem
category_theory.comma.map_right_map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T}
(r : R₁ ⟶ R₂)
(X Y : category_theory.comma L R₁)
(f : X ⟶ Y) :
((category_theory.comma.map_right L r).map f).right = f.right
@[simp]
theorem
category_theory.comma.map_right_map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T}
(r : R₁ ⟶ R₂)
(X Y : category_theory.comma L R₁)
(f : X ⟶ Y) :
((category_theory.comma.map_right L r).map f).left = f.left
@[simp]
theorem
category_theory.comma.map_right_obj_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T}
(r : R₁ ⟶ R₂)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right L r).obj X).left = X.left
@[simp]
theorem
category_theory.comma.map_right_obj_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T}
(r : R₁ ⟶ R₂)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right L r).obj X).right = X.right
def
category_theory.comma.map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T} :
(R₁ ⟶ R₂) → category_theory.comma L R₁ ⥤ category_theory.comma L R₂
A natural transformation R₁ ⟶ R₂ induces a functor comma L R₁ ⥤ comma L R₂.
@[simp]
theorem
category_theory.comma.map_right_obj_hom
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ : B ⥤ T}
(r : R₁ ⟶ R₂)
(X : category_theory.comma L R₁) :
@[simp]
theorem
category_theory.comma.map_right_id_hom_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_right_id L R).hom.app X).right = 𝟙 ((category_theory.comma.map_right L (𝟙 R)).obj X).right
def
category_theory.comma.map_right_id
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma.map_right L (𝟙 R) ≅ 𝟭 (category_theory.comma L R)
The functor comma L R ⥤ comma L R induced by the identity natural transformation on R is
naturally isomorphic to the identity functor.
Equations
- category_theory.comma.map_right_id L R = {hom := {app := λ (X : category_theory.comma L R), {left := 𝟙 ((category_theory.comma.map_right L (𝟙 R)).obj X).left, right := 𝟙 ((category_theory.comma.map_right L (𝟙 R)).obj X).right, w' := _}, naturality' := _}, inv := {app := λ (X : category_theory.comma L R), {left := 𝟙 ((𝟭 (category_theory.comma L R)).obj X).left, right := 𝟙 ((𝟭 (category_theory.comma L R)).obj X).right, w' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.comma.map_right_id_inv_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_right_id L R).inv.app X).right = 𝟙 ((𝟭 (category_theory.comma L R)).obj X).right
@[simp]
theorem
category_theory.comma.map_right_id_inv_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_right_id L R).inv.app X).left = 𝟙 ((𝟭 (category_theory.comma L R)).obj X).left
@[simp]
theorem
category_theory.comma.map_right_id_hom_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma L R) :
((category_theory.comma.map_right_id L R).hom.app X).left = 𝟙 ((category_theory.comma.map_right L (𝟙 R)).obj X).left
@[simp]
theorem
category_theory.comma.map_right_comp_inv_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ R₃ : B ⥤ T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right_comp L r r').inv.app X).left = 𝟙 ((category_theory.comma.map_right L r ⋙ category_theory.comma.map_right L r').obj X).left
def
category_theory.comma.map_right_comp
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ R₃ : B ⥤ T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃) :
The functor comma L R₁ ⥤ comma L R₃ induced by the composition of the natural transformations
r : R₁ ⟶ R₂ and r' : R₂ ⟶ R₃ is naturally isomorphic to the composition of the functors
induced by these natural transformations.
Equations
- category_theory.comma.map_right_comp L r r' = {hom := {app := λ (X : category_theory.comma L R₁), {left := 𝟙 ((category_theory.comma.map_right L (r ≫ r')).obj X).left, right := 𝟙 ((category_theory.comma.map_right L (r ≫ r')).obj X).right, w' := _}, naturality' := _}, inv := {app := λ (X : category_theory.comma L R₁), {left := 𝟙 ((category_theory.comma.map_right L r ⋙ category_theory.comma.map_right L r').obj X).left, right := 𝟙 ((category_theory.comma.map_right L r ⋙ category_theory.comma.map_right L r').obj X).right, w' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.comma.map_right_comp_hom_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ R₃ : B ⥤ T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right_comp L r r').hom.app X).right = 𝟙 ((category_theory.comma.map_right L (r ≫ r')).obj X).right
@[simp]
theorem
category_theory.comma.map_right_comp_inv_app_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ R₃ : B ⥤ T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right_comp L r r').inv.app X).right = 𝟙 ((category_theory.comma.map_right L r ⋙ category_theory.comma.map_right L r').obj X).right
@[simp]
theorem
category_theory.comma.map_right_comp_hom_app_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
(L : A ⥤ T)
{R₁ R₂ R₃ : B ⥤ T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : category_theory.comma L R₁) :
((category_theory.comma.map_right_comp L r r').hom.app X).left = 𝟙 ((category_theory.comma.map_right L (r ≫ r')).obj X).left