# 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₃)

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.

• left : A
• right : B
• hom : L.obj self.left R.obj self.right
Instances For
instance CategoryTheory.Comma.inhabited {T : Type u₃} [] [] :
Equations
• CategoryTheory.Comma.inhabited = { default := { left := default, right := default, hom := } }
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
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
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
@[simp]
theorem CategoryTheory.CommaMorphism.w {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } (self : ) :
CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map self.right)
instance CategoryTheory.CommaMorphism.inhabited {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } [] :
Equations
@[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 : } :
Equations
• CategoryTheory.commaCategory =
theorem CategoryTheory.Comma.hom_ext_iff {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } {X : } {Y : } {f : X Y} {g : X Y} :
f = g f.left = g.left f.right = g.right
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.

Equations
• = { obj := fun (X : ) => X.left, map := fun {X Y : } (f : X Y) => f.left, map_id := , map_comp := }
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.

Equations
• = { obj := fun (X : ) => X.right, map := fun {X Y : } (f : X Y) => f.right, map_id := , map_comp := }
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 : ) :
.comp L .comp 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
• = { app := fun (X : ) => X.hom, naturality := }
Instances For
@[simp]
theorem CategoryTheory.Comma.eqToHom_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) (Y : ) (H : X = Y) :
@[simp]
theorem CategoryTheory.Comma.eqToHom_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) (Y : ) (H : X = Y) :
.right =
@[simp]
theorem CategoryTheory.Comma.leftIso_inv {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
.inv = α.inv.left
@[simp]
theorem CategoryTheory.Comma.leftIso_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
.hom = α.hom.left
def CategoryTheory.Comma.leftIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
X.left Y.left

Extract the isomorphism between the left objects from an isomorphism in the comma category.

Equations
Instances For
@[simp]
theorem CategoryTheory.Comma.rightIso_inv {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
.inv = α.inv.right
@[simp]
theorem CategoryTheory.Comma.rightIso_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
.hom = α.hom.right
def CategoryTheory.Comma.rightIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L₁ : } {R₁ : } {X : } {Y : } (α : X Y) :
X.right Y.right

Extract the isomorphism between the right objects from an isomorphism in the comma category.

Equations
Instances For
@[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_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_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
@[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
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.

Equations
• = { hom := { left := l.hom, right := r.hom, w := h }, inv := { left := l.inv, right := r.inv, w := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Comma.map_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : ) :
(.obj X).right = F₂.obj X.right
@[simp]
theorem CategoryTheory.Comma.map_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : ) :
(.obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
@[simp]
theorem CategoryTheory.Comma.map_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X : } {Y : } (φ : X Y) :
(.map φ).left = F₁.map φ.left
@[simp]
theorem CategoryTheory.Comma.map_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X : } {Y : } (φ : X Y) :
(.map φ).right = F₂.map φ.right
@[simp]
theorem CategoryTheory.Comma.map_obj_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : ) :
(.obj X).left = F₁.obj X.left
def CategoryTheory.Comma.map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') :

The functor Comma L R ⥤ Comma L' R' induced by three functors F₁, F₂, F and two natural transformations F₁ ⋙ L' ⟶ L ⋙ F and R ⋙ F ⟶ F₂ ⋙ R'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Comma.faithful_map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.Faithful] [F₂.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.Comma.full_map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] :
.Full
Equations
• =
instance CategoryTheory.Comma.essSurj_map {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] :
.EssSurj
Equations
• =
noncomputable instance CategoryTheory.Comma.isEquivalenceMap {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [] [] [] {L : } {R : } {L' : } {R' : } {F₁ : } {F₂ : } {F : } (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] :
.IsEquivalence
Equations
• =
@[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_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
@[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_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
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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 =
@[simp]
theorem CategoryTheory.Comma.mapLeftId_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(.inv.app 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 =
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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 =
@[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 =
@[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 =
@[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 =
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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_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 =
@[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_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 =
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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_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_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_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_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_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_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_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_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 =
@[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_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_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_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_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_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_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_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_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
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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
@[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_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_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
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₂.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Comma.mapRightId_inv_app_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(.inv.app X).left =
@[simp]
theorem CategoryTheory.Comma.mapRightId_inv_app_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] (L : ) (R : ) (X : ) :
(.inv.app 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 =
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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 =
@[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 =
@[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 =
@[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 =
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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_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_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_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₂.

Equations
• One or more equations did not get rendered due to their size.
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_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_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_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_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_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_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_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_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_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_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_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
@[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_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_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_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_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 =
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₂.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Comma.preLeft_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
∀ {X Y : CategoryTheory.Comma (F.comp L) R} (f : X Y), (.map f).left = F.map f.left
@[simp]
theorem CategoryTheory.Comma.preLeft_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) (X : CategoryTheory.Comma (F.comp L) R) :
(.obj X).hom = X.hom
@[simp]
theorem CategoryTheory.Comma.preLeft_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
∀ {X Y : CategoryTheory.Comma (F.comp L) R} (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 : CategoryTheory.Comma (F.comp L) R) :
(.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 : CategoryTheory.Comma (F.comp L) R) :
(.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)

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Comma.preLeftIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) :
CategoryTheory.Comma.map (F.comp L).rightUnitor.inv (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)

Comma.preLeft is a particular case of Comma.map, but with better definitional properties.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Comma.instFaithfulCompPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.Comma.instFullCompPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) [F.Full] :
.Full
Equations
• =
instance CategoryTheory.Comma.instEssSurjCompPreLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) [F.EssSurj] :
.EssSurj
Equations
• =
instance CategoryTheory.Comma.isEquivalence_preLeft {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (F : ) (L : ) (R : ) [F.IsEquivalence] :
.IsEquivalence

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

Equations
• =
@[simp]
theorem CategoryTheory.Comma.preRight_map_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
∀ {X Y : CategoryTheory.Comma L (F.comp R)} (f : X Y), (.map f).right = F.map f.right
@[simp]
theorem CategoryTheory.Comma.preRight_obj_hom {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) (X : CategoryTheory.Comma L (F.comp R)) :
(.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 : CategoryTheory.Comma L (F.comp R)) :
(.obj X).left = X.left
@[simp]
theorem CategoryTheory.Comma.preRight_obj_right {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) (X : CategoryTheory.Comma L (F.comp R)) :
(.obj X).right = F.obj X.right
@[simp]
theorem CategoryTheory.Comma.preRight_map_left {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
∀ {X Y : CategoryTheory.Comma L (F.comp R)} (f : X Y), (.map f).left = f.left
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)

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Comma.preRightIso {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) :
CategoryTheory.Comma.map (CategoryTheory.CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv) (F.comp R).rightUnitor.hom

Comma.preRight is a particular case of Comma.map, but with better definitional properties.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Comma.instFaithfulCompPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.Comma.instFullCompPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) [F.Full] :
.Full
Equations
• =
instance CategoryTheory.Comma.instEssSurjCompPreRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) [F.EssSurj] :
.EssSurj
Equations
• =
instance CategoryTheory.Comma.isEquivalence_preRight {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {C : Type u₄} [] (L : ) (F : ) (R : ) [F.IsEquivalence] :
.IsEquivalence

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

Equations
• =
@[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_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_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
@[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
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)

Equations
• One or more equations did not get rendered due to their size.
Instances For