# mathlibdocumentation

category_theory.comma

# 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 functors `L` and `R`.
• `over X`: the over category of the object `X` (developed in `over.lean`).
• `under X`: the under category of the object `X` (also developed in `over.lean`).
• `arrow T`: the arrow category of the category `T` (developed in `arrow.lean`).

## Tags #

comma, slice, coslice, over, under, arrow

structure category_theory.comma {A : Type u₁} {B : Type u₂} {T : Type u₃} (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`
@[protected, instance]
Equations
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 : R} (x y : Y) (h : x.left = y.left) (h_1 : x.right = y.right) :
x = y
@[ext]
structure category_theory.comma_morphism {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} (X Y : R) :
Type (max v₁ v₂)

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`
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 : R} (x y : Y) :
x = y x.left = y.left x.right = y.right
@[protected, instance]
def category_theory.comma_morphism.inhabited {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} [inhabited ] :
Equations
@[simp]
theorem category_theory.comma_morphism.w {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X Y : R} (self : Y) :
L.map self.left Y.hom = X.hom R.map self.right
@[simp]
theorem category_theory.comma_morphism.w_assoc {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X Y : R} (self : Y) {X' : T} (f' : R.obj Y.right X') :
L.map self.left Y.hom f' = X.hom R.map self.right f'
@[protected, instance]
def category_theory.comma_category {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} :
Equations
@[simp]
theorem category_theory.comma.id_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X : R} :
@[simp]
theorem category_theory.comma.id_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X : R} :
@[simp]
theorem category_theory.comma.comp_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X Y Z : R} {f : X Y} {g : Y Z} :
(f g).left = f.left g.left
@[simp]
theorem category_theory.comma.comp_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {L : A T} {R : B T} {X Y Z : R} {f : X Y} {g : Y Z} :
(f g).right = f.right g.right
def category_theory.comma.fst {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) :

The functor sending an object `X` in the comma category to `X.left`.

Equations
@[simp]
theorem category_theory.comma.fst_map {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (_x _x_1 : R) (f : _x _x_1) :
.map f = f.left
@[simp]
theorem category_theory.comma.fst_obj {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
.obj X = X.left
def category_theory.comma.snd {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) :

The functor sending an object `X` in the comma category to `X.right`.

Equations
@[simp]
theorem category_theory.comma.snd_obj {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
.obj X = X.right
@[simp]
theorem category_theory.comma.snd_map {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (_x _x_1 : R) (f : _x _x_1) :
.map f = f.right
@[simp]
theorem category_theory.comma.nat_trans_app {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
= X.hom
def category_theory.comma.nat_trans {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) :

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
@[simp]
theorem category_theory.comma.eq_to_hom_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X Y : R) (H : X = Y) :
@[simp]
theorem category_theory.comma.eq_to_hom_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X Y : R) (H : X = Y) :
@[simp]
theorem category_theory.comma.iso_mk_inv_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {L₁ : A T} {R₁ : B T} {X Y : R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
h).inv.right = r.inv
@[simp]
theorem category_theory.comma.iso_mk_hom_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {L₁ : A T} {R₁ : B T} {X Y : R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
h).hom.left = l.hom
def category_theory.comma.iso_mk {A : Type u₁} {B : Type u₂} {T : Type u₃} {L₁ : A T} {R₁ : B T} {X Y : 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.

Equations
@[simp]
theorem category_theory.comma.iso_mk_hom_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {L₁ : A T} {R₁ : B T} {X Y : R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
h).hom.right = r.hom
@[simp]
theorem category_theory.comma.iso_mk_inv_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {L₁ : A T} {R₁ : B T} {X Y : R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
h).inv.left = l.inv
@[simp]
theorem category_theory.comma.map_left_obj_hom {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : R) :
X).hom = l.app X.left X.hom
@[simp]
theorem category_theory.comma.map_left_obj_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : R) :
X).right = X.right
@[simp]
theorem category_theory.comma.map_left_map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X Y : R) (f : X Y) :
f).right = f.right
@[simp]
theorem category_theory.comma.map_left_obj_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : R) :
X).left = X.left
@[simp]
theorem category_theory.comma.map_left_map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X Y : R) (f : X Y) :
f).left = f.left
def category_theory.comma.map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) :

A natural transformation `L₁ ⟶ L₂` induces a functor `comma L₂ R ⥤ comma L₁ R`.

Equations
@[simp]
theorem category_theory.comma.map_left_id_inv_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).left = 𝟙 ((𝟭 R)).obj X).left
@[simp]
theorem category_theory.comma.map_left_id_hom_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).left = 𝟙 (𝟙 L)).obj X).left
def category_theory.comma.map_left_id {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) :

The functor `comma L R ⥤ comma L R` induced by the identity natural transformation on `L` is naturally isomorphic to the identity functor.

Equations
@[simp]
theorem category_theory.comma.map_left_id_hom_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).right = 𝟙 (𝟙 L)).obj X).right
@[simp]
theorem category_theory.comma.map_left_id_inv_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).right = 𝟙 ((𝟭 R)).obj X).right
@[simp]
theorem category_theory.comma.map_left_comp_inv_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : R) :
l').inv.app X).right = 𝟙 X).right
@[simp]
theorem category_theory.comma.map_left_comp_hom_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : R) :
l').hom.app X).right = 𝟙 (l l')).obj X).right
def category_theory.comma.map_left_comp {A : Type u₁} {B : Type u₂} {T : Type u₃} (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
@[simp]
theorem category_theory.comma.map_left_comp_hom_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : R) :
l').hom.app X).left = 𝟙 (l l')).obj X).left
@[simp]
theorem category_theory.comma.map_left_comp_inv_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : R) :
l').inv.app X).left = 𝟙 X).left
@[simp]
theorem category_theory.comma.map_right_map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X Y : R₁) (f : X Y) :
f).left = f.left
@[simp]
theorem category_theory.comma.map_right_obj_hom {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : R₁) :
X).hom = X.hom r.app X.right
def category_theory.comma.map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) :

A natural transformation `R₁ ⟶ R₂` induces a functor `comma L R₁ ⥤ comma L R₂`.

Equations
@[simp]
theorem category_theory.comma.map_right_obj_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : R₁) :
X).right = X.right
@[simp]
theorem category_theory.comma.map_right_obj_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : R₁) :
X).left = X.left
@[simp]
theorem category_theory.comma.map_right_map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X Y : R₁) (f : X Y) :
f).right = f.right
@[simp]
theorem category_theory.comma.map_right_id_hom_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).right = 𝟙 (𝟙 R)).obj X).right
@[simp]
theorem category_theory.comma.map_right_id_inv_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).right = 𝟙 ((𝟭 R)).obj X).right
@[simp]
theorem category_theory.comma.map_right_id_inv_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).left = 𝟙 ((𝟭 R)).obj X).left
@[simp]
theorem category_theory.comma.map_right_id_hom_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) (X : R) :
X).left = 𝟙 (𝟙 R)).obj X).left
def category_theory.comma.map_right_id {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) (R : B T) :

The functor `comma L R ⥤ comma L R` induced by the identity natural transformation on `R` is naturally isomorphic to the identity functor.

Equations
@[simp]
theorem category_theory.comma.map_right_comp_hom_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : R₁) :
r').hom.app X).left = 𝟙 (r r')).obj X).left
@[simp]
theorem category_theory.comma.map_right_comp_inv_app_left {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : R₁) :
r').inv.app X).left = 𝟙 X).left
@[simp]
theorem category_theory.comma.map_right_comp_inv_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : R₁) :
r').inv.app X).right = 𝟙 X).right
def category_theory.comma.map_right_comp {A : Type u₁} {B : Type u₂} {T : Type u₃} (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
@[simp]
theorem category_theory.comma.map_right_comp_hom_app_right {A : Type u₁} {B : Type u₂} {T : Type u₃} (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : R₁) :
r').hom.app X).right = 𝟙 (r r')).obj X).right
@[simp]
theorem category_theory.comma.pre_left_obj_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
R).obj X).left = F.obj X.left
@[simp]
theorem category_theory.comma.pre_left_obj_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
R).obj X).right = X.right
def category_theory.comma.pre_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) :

The functor `(F ⋙ L, R) ⥤ (L, R)`

Equations
@[simp]
theorem category_theory.comma.pre_left_map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) (X Y : category_theory.comma (F L) R) (f : X Y) :
R).map f).left = F.map f.left
@[simp]
theorem category_theory.comma.pre_left_map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) (X Y : category_theory.comma (F L) R) (f : X Y) :
R).map f).right = f.right
@[simp]
theorem category_theory.comma.pre_left_obj_hom {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
R).obj X).hom = X.hom
@[simp]
theorem category_theory.comma.pre_right_obj_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) (X : (F R)) :
R).obj X).right = F.obj X.right
@[simp]
theorem category_theory.comma.pre_right_obj_hom {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) (X : (F R)) :
R).obj X).hom = X.hom
@[simp]
theorem category_theory.comma.pre_right_map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) (X Y : (F R)) (f : X Y) :
R).map f).right = F.map f.right
@[simp]
theorem category_theory.comma.pre_right_obj_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) (X : (F R)) :
R).obj X).left = X.left
def category_theory.comma.pre_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) :
(F R)

The functor `(F ⋙ L, R) ⥤ (L, R)`

Equations
@[simp]
theorem category_theory.comma.pre_right_map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (F : C B) (R : B T) (X Y : (F R)) (f : X Y) :
R).map f).left = f.left
@[simp]
theorem category_theory.comma.post_obj_hom {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) (X : R) :
F).obj X).hom = F.map X.hom
@[simp]
theorem category_theory.comma.post_obj_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) (X : R) :
F).obj X).right = X.right
def category_theory.comma.post {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) :

The functor `(L, R) ⥤ (L ⋙ F, R ⋙ F)`

Equations
@[simp]
theorem category_theory.comma.post_obj_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) (X : R) :
F).obj X).left = X.left
@[simp]
theorem category_theory.comma.post_map_right {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) (X Y : R) (f : X Y) :
F).map f).right = f.right
@[simp]
theorem category_theory.comma.post_map_left {A : Type u₁} {B : Type u₂} {T : Type u₃} {C : Type u₄} (L : A T) (R : B T) (F : T C) (X Y : R) (f : X Y) :
F).map f).left = f.left