# Documentation

Mathlib.CategoryTheory.Comma

# 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 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 CategoryTheory.Comma {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) :
Type (max u₁ u₂ v₃)
• left : A
• right : B
• hom : L.obj s.left R.obj s.right

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
instance CategoryTheory.Comma.inhabited {T : Type u₃} [] [] :
theorem CategoryTheory.CommaMorphism.ext_iff {A : Type u₁} :
∀ {inst : } {B : Type u₂} {inst_1 : } {T : Type u₃} {inst_2 : } {L : } {R : } {X Y : } (x y : ), x = y x.left = y.left x.right = y.right
theorem CategoryTheory.CommaMorphism.ext {A : Type u₁} :
∀ {inst : } {B : Type u₂} {inst_1 : } {T : Type u₃} {inst_2 : } {L : } {R : } {X Y : } (x y : ), x.left = y.leftx.right = y.rightx = y
structure CategoryTheory.CommaMorphism {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (X : ) (Y : ) :
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
instance CategoryTheory.CommaMorphism.inhabited {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } [] :
@[simp]
theorem CategoryTheory.CommaMorphism.w_assoc {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } (self : ) {Z : T} (h : R.obj Y.right Z) :
instance CategoryTheory.commaCategory {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } :
theorem CategoryTheory.Comma.hom_ext {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g
@[simp]
theorem CategoryTheory.Comma.id_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } :
@[simp]
theorem CategoryTheory.Comma.id_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } :
().right =
@[simp]
theorem CategoryTheory.Comma.comp_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } {Z : } {f : X Y} {g : Y Z} :
@[simp]
theorem CategoryTheory.Comma.comp_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } {Z : } {f : X Y} {g : Y Z} :
().right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
theorem CategoryTheory.Comma.fst_obj {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
().obj X = X.left
@[simp]
theorem CategoryTheory.Comma.fst_map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) :
∀ {X Y : } (f : X Y), ().map f = f.left
def CategoryTheory.Comma.fst {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Comma.snd_map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) :
∀ {X Y : } (f : X Y), ().map f = f.right
@[simp]
theorem CategoryTheory.Comma.snd_obj {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
().obj X = X.right
def CategoryTheory.Comma.snd {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Comma.natTrans_app {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
().app X = X.hom
def CategoryTheory.Comma.natTrans {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (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.

Instances For
@[simp]
theorem CategoryTheory.Comma.eqToHom_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) (Y : ) (H : X = Y) :
().left = CategoryTheory.eqToHom (_ : X.left = Y.left)
@[simp]
theorem CategoryTheory.Comma.eqToHom_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) (Y : ) (H : X = Y) :
().right = CategoryTheory.eqToHom (_ : X.right = Y.right)
@[simp]
theorem CategoryTheory.Comma.isoMk_inv_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
().inv.right = r.inv
@[simp]
theorem CategoryTheory.Comma.isoMk_hom_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
().hom.left = l.hom
@[simp]
theorem CategoryTheory.Comma.isoMk_inv_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
().inv.left = l.inv
@[simp]
theorem CategoryTheory.Comma.isoMk_hom_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
().hom.right = r.hom
def CategoryTheory.Comma.isoMk {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
X Y

Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapLeft_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) :
∀ {X Y : } (f : X Y), (().map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapLeft_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (X : ) :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.mapLeft_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (X : ) :
(().obj X).hom = CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom
@[simp]
theorem CategoryTheory.Comma.mapLeft_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (X : ) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapLeft_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) :
∀ {X Y : } (f : X Y), (().map f).right = f.right
def CategoryTheory.Comma.mapLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) :

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

Instances For
@[simp]
theorem CategoryTheory.Comma.mapLeftId_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().inv.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
@[simp]
theorem CategoryTheory.Comma.mapLeftId_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().inv.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapLeftId_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftId_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().hom.app X).right = CategoryTheory.CategoryStruct.id ().right
def CategoryTheory.Comma.mapLeftId {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (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.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapLeftComp_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } {L₃ : } (l : L₁ L₂) (l' : L₂ L₃) (X : ) :
(().hom.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapLeftComp_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } {L₃ : } (l : L₁ L₂) (l' : L₂ L₃) (X : ) :
(().inv.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapLeftComp_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } {L₃ : } (l : L₁ L₂) (l' : L₂ L₃) (X : ) :
(().hom.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
@[simp]
theorem CategoryTheory.Comma.mapLeftComp_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } {L₃ : } (l : L₁ L₂) (l' : L₂ L₃) (X : ) :
(().inv.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
def CategoryTheory.Comma.mapLeftComp {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } {L₃ : } (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.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapLeftEq_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (l' : L₁ L₂) (h : l = l') (X : ) :
(().hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftEq_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (l' : L₁ L₂) (h : l = l') (X : ) :
(().inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftEq_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (l' : L₁ L₂) (h : l = l') (X : ) :
(().hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapLeftEq_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (l' : L₁ L₂) (h : l = l') (X : ) :
(().inv.app X).right =
def CategoryTheory.Comma.mapLeftEq {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (l : L₁ L₂) (l' : L₁ L₂) (h : l = l') :

Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors Comma L₁ R ⥤ Comma L₂ R.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().unitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_functor_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) :
∀ {X Y : } (f : X Y), (().functor.map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_functor_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().functor.obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().counitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().unitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().inverse.obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().inverse.obj X).hom = CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_functor_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) :
∀ {X Y : } (f : X Y), (().functor.map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_functor_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().functor.obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_inverse_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) :
∀ {X Y : } (f : X Y), (().inverse.map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().unitIso.hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_functor_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().counitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().counitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().unitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().inverse.obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_inverse_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) :
∀ {X Y : } (f : X Y), (().inverse.map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) (X : ) :
(().counitIso.hom.app X).right =
def CategoryTheory.Comma.mapLeftIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (R : ) {L₁ : } {L₂ : } (i : L₁ L₂) :

A natural isomorphism L₁ ≅ L₂ induces an equivalence of categories Comma L₁ R ≌ Comma L₂ R.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapRight_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (X : ) :
(().obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
@[simp]
theorem CategoryTheory.Comma.mapRight_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (X : ) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapRight_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) :
∀ {X Y : } (f : X Y), (().map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapRight_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) :
∀ {X Y : } (f : X Y), (().map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.mapRight_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (X : ) :
(().obj X).left = X.left
def CategoryTheory.Comma.mapRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) :

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

Instances For
@[simp]
theorem CategoryTheory.Comma.mapRightId_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().inv.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapRightId_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightId_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightId_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(().inv.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
def CategoryTheory.Comma.mapRightId {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (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.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapRightComp_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } {R₃ : } (r : R₁ R₂) (r' : R₂ R₃) (X : ) :
(().inv.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
@[simp]
theorem CategoryTheory.Comma.mapRightComp_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } {R₃ : } (r : R₁ R₂) (r' : R₂ R₃) (X : ) :
(().hom.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapRightComp_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } {R₃ : } (r : R₁ R₂) (r' : R₂ R₃) (X : ) :
(().inv.app X).right = CategoryTheory.CategoryStruct.id (().obj X).right
@[simp]
theorem CategoryTheory.Comma.mapRightComp_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } {R₃ : } (r : R₁ R₂) (r' : R₂ R₃) (X : ) :
(().hom.app X).left = CategoryTheory.CategoryStruct.id (().obj X).left
def CategoryTheory.Comma.mapRightComp {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } {R₃ : } (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.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapRightEq_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (r' : R₁ R₂) (h : r = r') (X : ) :
(().inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightEq_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (r' : R₁ R₂) (h : r = r') (X : ) :
(().hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightEq_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (r' : R₁ R₂) (h : r = r') (X : ) :
(().hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightEq_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (r' : R₁ R₂) (h : r = r') (X : ) :
(().inv.app X).right =
def CategoryTheory.Comma.mapRightEq {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (r : R₁ R₂) (r' : R₁ R₂) (h : r = r') :

Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors Comma L R₁ ⥤ Comma L R₂.

Instances For
@[simp]
theorem CategoryTheory.Comma.mapRightIso_unitIso_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().unitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_counitIso_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().counitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_counitIso_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().counitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_inverse_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().inverse.obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapRightIso_inverse_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().inverse.obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.mapRightIso_functor_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().functor.obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().unitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_inverse_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) :
∀ {X Y : } (f : X Y), (().inverse.map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapRightIso_unitIso_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().unitIso.hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_functor_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) :
∀ {X Y : } (f : X Y), (().functor.map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.mapRightIso_counitIso_hom_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().counitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().unitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_inverse_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().inverse.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
@[simp]
theorem CategoryTheory.Comma.mapRightIso_counitIso_hom_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().counitIso.hom.app X).right =
@[simp]
theorem CategoryTheory.Comma.mapRightIso_inverse_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) :
∀ {X Y : } (f : X Y), (().inverse.map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.mapRightIso_functor_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
@[simp]
theorem CategoryTheory.Comma.mapRightIso_functor_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) :
∀ {X Y : } (f : X Y), (().functor.map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.mapRightIso_functor_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) (X : ) :
(().functor.obj X).left = X.left
def CategoryTheory.Comma.mapRightIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) {R₁ : } {R₂ : } (i : R₁ R₂) :

A natural isomorphism R₁ ≅ R₂ induces an equivalence of categories Comma L R₁ ≌ Comma L R₂.

Instances For
@[simp]
theorem CategoryTheory.Comma.preLeft_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) (X : ) :
(().obj X).hom = X.hom
@[simp]
theorem CategoryTheory.Comma.preLeft_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
∀ {X Y : } (f : X Y), (().map f).left = F.map f.left
@[simp]
theorem CategoryTheory.Comma.preLeft_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
∀ {X Y : } (f : X Y), (().map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.preLeft_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) (X : ) :
(().obj X).left = F.obj X.left
@[simp]
theorem CategoryTheory.Comma.preLeft_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) (X : ) :
(().obj X).right = X.right
def CategoryTheory.Comma.preLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :

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

Instances For
instance CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
instance CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
instance CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
noncomputable def CategoryTheory.Comma.isEquivalencePreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :

If F is an equivalence, then so is preLeft F L R.

Instances For
@[simp]
theorem CategoryTheory.Comma.preRight_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
∀ {X Y : } (f : X Y), (().map f).left = f.left
@[simp]
theorem CategoryTheory.Comma.preRight_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) (X : ) :
(().obj X).right = F.obj X.right
@[simp]
theorem CategoryTheory.Comma.preRight_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) (X : ) :
(().obj X).hom = X.hom
@[simp]
theorem CategoryTheory.Comma.preRight_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) (X : ) :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.preRight_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
∀ {X Y : } (f : X Y), (().map f).right = F.map f.right
def CategoryTheory.Comma.preRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :

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

Instances For
instance CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
instance CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
instance CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
noncomputable def CategoryTheory.Comma.isEquivalencePreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :

If F is an equivalence, then so is preRight L F R.

Instances For
@[simp]
theorem CategoryTheory.Comma.post_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) (X : ) :
(().obj X).hom = F.map X.hom
@[simp]
theorem CategoryTheory.Comma.post_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) (X : ) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.Comma.post_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) :
∀ {X Y : } (f : X Y), (().map f).right = f.right
@[simp]
theorem CategoryTheory.Comma.post_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) (X : ) :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.post_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) :
∀ {X Y : } (f : X Y), (().map f).left = f.left
def CategoryTheory.Comma.post {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (R : ) (F : ) :

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

Instances For