Comma categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
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]
(L : A ⥤ T)
(R : B ⥤ T) :
Type (max u₁ u₂ v₃)
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.
Instances for category_theory.comma
- category_theory.comma.has_sizeof_inst
- category_theory.comma.inhabited
- category_theory.comma_category
@[protected, 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 _inst_4, right := inhabited.default _inst_4, hom := 𝟙 inhabited.default}}
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)
(h : x.left = y.left)
(h_1 : x.right = y.right) :
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}
(X Y : category_theory.comma L R) :
Type (max v₁ v₂)
- left : X.left ⟶ Y.left
- right : X.right ⟶ Y.right
- w' : L.map self.left ≫ Y.hom = X.hom ≫ R.map self.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.
Instances for category_theory.comma_morphism
- category_theory.comma_morphism.has_sizeof_inst
- category_theory.comma_morphism.inhabited
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) :
@[protected, 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.left, right := 𝟙 inhabited.default.right, w' := _}}
@[simp]
theorem
category_theory.comma_morphism.w
{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}
(self : category_theory.comma_morphism X Y) :
@[simp]
theorem
category_theory.comma_morphism.w_assoc
{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}
(self : category_theory.comma_morphism X Y)
{X' : T}
(f' : R.obj Y.right ⟶ X') :
@[protected, 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_quiver := {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.eq_to_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)
(H : X = Y) :
@[simp]
theorem
category_theory.comma.eq_to_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)
(H : X = Y) :
@[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
@[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
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)
(h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) :
X ≅ Y
Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.
@[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_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.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_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
@[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_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_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
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₁ ⟶ 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_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_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_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_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_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
@[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
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_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_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_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₁) :
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₁ ⟶ 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_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
@[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_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_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
@[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
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_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
@[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
@[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
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.pre_left_obj_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma (F ⋙ L) R) :
@[simp]
theorem
category_theory.comma.pre_left_obj_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma (F ⋙ L) R) :
((category_theory.comma.pre_left F L R).obj X).right = X.right
def
category_theory.comma.pre_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T) :
category_theory.comma (F ⋙ L) R ⥤ category_theory.comma L R
The functor (F ⋙ L, R) ⥤ (L, R)
@[simp]
theorem
category_theory.comma.pre_left_map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T)
(X Y : category_theory.comma (F ⋙ L) R)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.comma.pre_left_map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T)
(X Y : category_theory.comma (F ⋙ L) R)
(f : X ⟶ Y) :
((category_theory.comma.pre_left F L R).map f).right = f.right
@[simp]
theorem
category_theory.comma.pre_left_obj_hom
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(F : C ⥤ A)
(L : A ⥤ T)
(R : B ⥤ T)
(X : category_theory.comma (F ⋙ L) R) :
((category_theory.comma.pre_left F L R).obj X).hom = X.hom
@[simp]
theorem
category_theory.comma.pre_right_obj_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T)
(X : category_theory.comma L (F ⋙ R)) :
@[simp]
theorem
category_theory.comma.pre_right_obj_hom
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T)
(X : category_theory.comma L (F ⋙ R)) :
((category_theory.comma.pre_right L F R).obj X).hom = X.hom
@[simp]
theorem
category_theory.comma.pre_right_map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T)
(X Y : category_theory.comma L (F ⋙ R))
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.comma.pre_right_obj_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T)
(X : category_theory.comma L (F ⋙ R)) :
((category_theory.comma.pre_right L F R).obj X).left = X.left
def
category_theory.comma.pre_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T) :
category_theory.comma L (F ⋙ R) ⥤ category_theory.comma L R
The functor (F ⋙ L, R) ⥤ (L, R)
@[simp]
theorem
category_theory.comma.pre_right_map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(F : C ⥤ B)
(R : B ⥤ T)
(X Y : category_theory.comma L (F ⋙ R))
(f : X ⟶ Y) :
((category_theory.comma.pre_right L F R).map f).left = f.left
@[simp]
theorem
category_theory.comma.post_obj_hom
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C)
(X : category_theory.comma L R) :
@[simp]
theorem
category_theory.comma.post_obj_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C)
(X : category_theory.comma L R) :
((category_theory.comma.post L R F).obj X).right = X.right
def
category_theory.comma.post
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C) :
category_theory.comma L R ⥤ category_theory.comma (L ⋙ F) (R ⋙ F)
The functor (L, R) ⥤ (L ⋙ F, R ⋙ F)
@[simp]
theorem
category_theory.comma.post_obj_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C)
(X : category_theory.comma L R) :
((category_theory.comma.post L R F).obj X).left = X.left
@[simp]
theorem
category_theory.comma.post_map_right
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C)
(X Y : category_theory.comma L R)
(f : X ⟶ Y) :
((category_theory.comma.post L R F).map f).right = f.right
@[simp]
theorem
category_theory.comma.post_map_left
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{C : Type u₄}
[category_theory.category C]
(L : A ⥤ T)
(R : B ⥤ T)
(F : T ⥤ C)
(X Y : category_theory.comma L R)
(f : X ⟶ Y) :
((category_theory.comma.post L R F).map f).left = f.left