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).

References

• https://ncatlab.org/nlab/show/comma+category

Tags

comma, slice, coslice, over, under, arrow

structure CategoryTheory.Comma {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor 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.

• left : A

  The left subobject

• right : B

  The right subobject

• hom : L.obj self.left ⟶ R.obj self.right

  A morphism from L.obj left to R.obj right

@[implicit_reducible]

instance CategoryTheory.Comma.inhabited {T : Type u₃} [Category.{v₃, u₃} T] [Inhabited T] : Inhabited (Comma (Functor.id T) (Functor.id T))

structure CategoryTheory.CommaMorphism {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} (X Y : Comma L 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.

• left : X.left ⟶ Y.left

  Morphism on left objects

• right : X.right ⟶ Y.right

  Morphism on right objects

• w : CategoryStruct.comp (L.map self.left) Y.hom = CategoryStruct.comp X.hom (R.map self.right)

theorem CategoryTheory.CommaMorphism.ext {A : Type u₁} {inst✝ : Category.{v₁, u₁} A} {B : Type u₂} {inst✝¹ : Category.{v₂, u₂} B} {T : Type u₃} {inst✝² : Category.{v₃, u₃} T} {L : Functor A T} {R : Functor B T} {X Y : Comma L R} {x y : CommaMorphism X Y} (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem CategoryTheory.CommaMorphism.ext_iff {A : Type u₁} {inst✝ : Category.{v₁, u₁} A} {B : Type u₂} {inst✝¹ : Category.{v₂, u₂} B} {T : Type u₃} {inst✝² : Category.{v₃, u₃} T} {L : Functor A T} {R : Functor B T} {X Y : Comma L R} {x y : CommaMorphism X Y} : x = y ↔ x.left = y.left ∧ x.right = y.right

@[implicit_reducible]

instance CategoryTheory.CommaMorphism.inhabited {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} [Inhabited (Comma L R)] : Inhabited (CommaMorphism default default)

@[simp]

theorem CategoryTheory.CommaMorphism.w_assoc {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (self : CommaMorphism X Y) {Z : T} (h : R.obj Y.right ⟶ Z) : CategoryStruct.comp (L.map self.left) (CategoryStruct.comp Y.hom h) = CategoryStruct.comp X.hom (CategoryStruct.comp (R.map self.right) h)

@[implicit_reducible]

instance CategoryTheory.commaCategory {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} : Category.{max v₂ v₁, max (max u₂ u₁) v₃} (Comma L R)

theorem CategoryTheory.Comma.hom_ext {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

theorem CategoryTheory.Comma.hom_ext_iff {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} {f g : X ⟶ Y} : f = g ↔ f.left = g.left ∧ f.right = g.right

@[simp]

theorem CategoryTheory.Comma.id_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X : Comma L R} : (CategoryStruct.id X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.id_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X : Comma L R} : (CategoryStruct.id X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.comp_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y Z : Comma L R} {f : X ⟶ Y} {g : Y ⟶ Z} : (CategoryStruct.comp f g).left = CategoryStruct.comp f.left g.left

@[simp]

theorem CategoryTheory.Comma.comp_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y Z : Comma L R} {f : X ⟶ Y} {g : Y ⟶ Z} : (CategoryStruct.comp f g).right = CategoryStruct.comp f.right g.right

def CategoryTheory.Comma.fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : Functor (Comma L R) A

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

@[simp]

theorem CategoryTheory.Comma.fst_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (fst L R).map f = f.left

@[simp]

theorem CategoryTheory.Comma.fst_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : (fst L R).obj X = X.left

def CategoryTheory.Comma.snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : Functor (Comma L R) B

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

@[simp]

theorem CategoryTheory.Comma.snd_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (snd L R).map f = f.right

@[simp]

theorem CategoryTheory.Comma.snd_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : (snd L R).obj X = X.right

def CategoryTheory.Comma.natTrans {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (fst L R).comp L ⟶ (snd L R).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.

@[simp]

theorem CategoryTheory.Comma.natTrans_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : (natTrans L R).app X = X.hom

@[simp]

theorem CategoryTheory.Comma.eqToHom_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X Y : Comma L R) (H : X = Y) : (eqToHom H).left = eqToHom ⋯

@[simp]

theorem CategoryTheory.Comma.eqToHom_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X Y : Comma L R) (H : X = Y) : (eqToHom H).right = eqToHom ⋯

instance CategoryTheory.Comma.instIsIsoLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : IsIso e.left

instance CategoryTheory.Comma.instIsIsoRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : IsIso e.right

@[simp]

theorem CategoryTheory.Comma.inv_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : (inv e).left = inv e.left

@[simp]

theorem CategoryTheory.Comma.inv_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : (inv e).right = inv e.right

theorem CategoryTheory.Comma.left_hom_inv_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : CategoryStruct.comp (L.map e.left) (CategoryStruct.comp Y.hom (R.map (inv e.right))) = X.hom

theorem CategoryTheory.Comma.inv_left_hom_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X ⟶ Y) [IsIso e] : CategoryStruct.comp (L.map (inv e.left)) (CategoryStruct.comp X.hom (R.map e.right)) = Y.hom

def CategoryTheory.Comma.leftIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : X.left ≅ Y.left

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

@[simp]

theorem CategoryTheory.Comma.leftIso_inv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : (leftIso α).inv = α.inv.left

@[simp]

theorem CategoryTheory.Comma.leftIso_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : (leftIso α).hom = α.hom.left

def CategoryTheory.Comma.rightIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : X.right ≅ Y.right

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

@[simp]

theorem CategoryTheory.Comma.rightIso_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : (rightIso α).hom = α.hom.right

@[simp]

theorem CategoryTheory.Comma.rightIso_inv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X ≅ Y) : (rightIso α).inv = α.inv.right

def CategoryTheory.Comma.isoMk {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by cat_disch) : X ≅ Y

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

@[simp]

theorem CategoryTheory.Comma.isoMk_inv_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by cat_disch) : (isoMk l r h).inv.left = l.inv

@[simp]

theorem CategoryTheory.Comma.isoMk_hom_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by cat_disch) : (isoMk l r h).hom.left = l.hom

@[simp]

theorem CategoryTheory.Comma.isoMk_inv_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by cat_disch) : (isoMk l r h).inv.right = r.inv

@[simp]

theorem CategoryTheory.Comma.isoMk_hom_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by cat_disch) : (isoMk l r h).hom.right = r.hom

def CategoryTheory.Comma.map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : Functor (Comma L R) (Comma L' 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'.

@[simp]

theorem CategoryTheory.Comma.map_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : Comma L R} (φ : X ⟶ Y) : ((map α β).map φ).left = F₁.map φ.left

@[simp]

theorem CategoryTheory.Comma.map_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : ((map α β).obj X).right = F₂.obj X.right

@[simp]

theorem CategoryTheory.Comma.map_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : ((map α β).obj X).hom = CategoryStruct.comp (α.app X.left) (CategoryStruct.comp (F.map X.hom) (β.app X.right))

@[simp]

theorem CategoryTheory.Comma.map_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : Comma L R} (φ : X ⟶ Y) : ((map α β).map φ).right = F₂.map φ.right

@[simp]

theorem CategoryTheory.Comma.map_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : ((map α β).obj X).left = F₁.obj X.left

instance CategoryTheory.Comma.faithful_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.Faithful] [F₂.Faithful] : (map α β).Faithful

instance CategoryTheory.Comma.full_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (map α β).Full

instance CategoryTheory.Comma.essSurj_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] : (map α β).EssSurj

instance CategoryTheory.Comma.isEquivalenceMap {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [IsIso α] [IsIso β] : (map α β).IsEquivalence

@[simp]

theorem CategoryTheory.Comma.map_fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (map α β).comp (fst L' R') = (fst L R).comp F₁

The equality between map α β ⋙ fst L' R' and fst L R ⋙ F₁, where α : F₁ ⋙ L' ⟶ L ⋙ F.

def CategoryTheory.Comma.mapFst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (map α β).comp (fst L' R') ≅ (fst L R).comp F₁

The isomorphism between map α β ⋙ fst L' R' and fst L R ⋙ F₁, where α : F₁ ⋙ L' ⟶ L ⋙ F.

@[simp]

theorem CategoryTheory.Comma.mapFst_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : (mapFst α β).inv.app X = CategoryStruct.id (F₁.obj X.left)

@[simp]

theorem CategoryTheory.Comma.mapFst_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : (mapFst α β).hom.app X = CategoryStruct.id (F₁.obj X.left)

@[simp]

theorem CategoryTheory.Comma.map_snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (map α β).comp (snd L' R') = (snd L R).comp F₂

The equality between map α β ⋙ snd L' R' and snd L R ⋙ F₂, where β : R ⋙ F ⟶ F₂ ⋙ R'.

def CategoryTheory.Comma.mapSnd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (map α β).comp (snd L' R') ≅ (snd L R).comp F₂

The isomorphism between map α β ⋙ snd L' R' and snd L R ⋙ F₂, where β : R ⋙ F ⟶ F₂ ⋙ R'.

@[simp]

theorem CategoryTheory.Comma.mapSnd_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : (mapSnd α β).hom.app X = CategoryStruct.id (F₂.obj X.right)

@[simp]

theorem CategoryTheory.Comma.mapSnd_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : Comma L R) : (mapSnd α β).inv.app X = CategoryStruct.id (F₂.obj X.right)

def CategoryTheory.Comma.mapLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) : Functor (Comma L₂ R) (Comma L₁ R)

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

@[simp]

theorem CategoryTheory.Comma.mapLeft_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (X : Comma L₂ R) : ((mapLeft R l).obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapLeft_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ ⟶ Y✝) : ((mapLeft R l).map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.mapLeft_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (X : Comma L₂ R) : ((mapLeft R l).obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.mapLeft_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ ⟶ Y✝) : ((mapLeft R l).map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapLeft_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (X : Comma L₂ R) : ((mapLeft R l).obj X).hom = CategoryStruct.comp (l.app X.left) X.hom

def CategoryTheory.Comma.mapLeftId {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : mapLeft R (CategoryStruct.id L) ≅ Functor.id (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.

@[simp]

theorem CategoryTheory.Comma.mapLeftId_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapLeftId L R).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftId_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapLeftId L R).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftId_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapLeftId L R).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftId_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapLeftId L R).inv.app X).right = CategoryStruct.id X.right

def CategoryTheory.Comma.mapLeftComp {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) : mapLeft R (CategoryStruct.comp l l') ≅ (mapLeft R l').comp (mapLeft R 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.

@[simp]

theorem CategoryTheory.Comma.mapLeftComp_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : Comma L₃ R) : ((mapLeftComp R l l').inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftComp_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : Comma L₃ R) : ((mapLeftComp R l l').hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftComp_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : Comma L₃ R) : ((mapLeftComp R l l').hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftComp_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : Comma L₃ R) : ((mapLeftComp R l l').inv.app X).left = CategoryStruct.id X.left

def CategoryTheory.Comma.mapLeftEq {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') : mapLeft R l ≅ mapLeft R l'

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

@[simp]

theorem CategoryTheory.Comma.mapLeftEq_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : Comma L₂ R) : ((mapLeftEq R l l' h).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftEq_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : Comma L₂ R) : ((mapLeftEq R l l' h).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftEq_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : Comma L₂ R) : ((mapLeftEq R l l' h).inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftEq_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : Comma L₂ R) : ((mapLeftEq R l l' h).inv.app X).left = CategoryStruct.id X.left

def CategoryTheory.Comma.mapLeftIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) : Comma L₁ R ≌ Comma L₂ R

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

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_functor_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) {X✝ Y✝ : Comma L₁ R} (f : X✝ ⟶ Y✝) : ((mapLeftIso R i).functor.map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ ⟶ Y✝) : ((mapLeftIso R i).inverse.map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).counitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_functor_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) {X✝ Y✝ : Comma L₁ R} (f : X✝ ⟶ Y✝) : ((mapLeftIso R i).functor.map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).counitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).counitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).counitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).inverse.obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_functor_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).functor.obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).inverse.obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₂ R) : ((mapLeftIso R i).inverse.obj X).hom = CategoryStruct.comp (i.hom.app X.left) X.hom

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_functor_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).functor.obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_inverse_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ ⟶ Y✝) : ((mapLeftIso R i).inverse.map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapLeftIso_functor_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ ≅ L₂) (X : Comma L₁ R) : ((mapLeftIso R i).functor.obj X).hom = CategoryStruct.comp (i.inv.app X.left) X.hom

def CategoryTheory.Comma.mapRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) : Functor (Comma L R₁) (Comma L R₂)

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

@[simp]

theorem CategoryTheory.Comma.mapRight_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ ⟶ Y✝) : ((mapRight L r).map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.mapRight_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (X : Comma L R₁) : ((mapRight L r).obj X).hom = CategoryStruct.comp X.hom (r.app X.right)

@[simp]

theorem CategoryTheory.Comma.mapRight_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (X : Comma L R₁) : ((mapRight L r).obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapRight_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ ⟶ Y✝) : ((mapRight L r).map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapRight_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (X : Comma L R₁) : ((mapRight L r).obj X).left = X.left

def CategoryTheory.Comma.mapRightId {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : mapRight L (CategoryStruct.id R) ≅ Functor.id (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.

@[simp]

theorem CategoryTheory.Comma.mapRightId_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapRightId L R).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightId_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapRightId L R).inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightId_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapRightId L R).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightId_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : ((mapRightId L R).hom.app X).left = CategoryStruct.id X.left

def CategoryTheory.Comma.mapRightComp {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) : mapRight L (CategoryStruct.comp r r') ≅ (mapRight L r).comp (mapRight L 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.

@[simp]

theorem CategoryTheory.Comma.mapRightComp_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (X : Comma L R₁) : ((mapRightComp L r r').inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightComp_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (X : Comma L R₁) : ((mapRightComp L r r').hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightComp_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (X : Comma L R₁) : ((mapRightComp L r r').hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightComp_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (X : Comma L R₁) : ((mapRightComp L r r').inv.app X).right = CategoryStruct.id X.right

def CategoryTheory.Comma.mapRightEq {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ ⟶ R₂) (h : r = r') : mapRight L r ≅ mapRight L r'

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

@[simp]

theorem CategoryTheory.Comma.mapRightEq_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ ⟶ R₂) (h : r = r') (X : Comma L R₁) : ((mapRightEq L r r' h).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightEq_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ ⟶ R₂) (h : r = r') (X : Comma L R₁) : ((mapRightEq L r r' h).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightEq_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ ⟶ R₂) (h : r = r') (X : Comma L R₁) : ((mapRightEq L r r' h).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightEq_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ ⟶ R₂) (h : r = r') (X : Comma L R₁) : ((mapRightEq L r r' h).inv.app X).right = CategoryStruct.id X.right

def CategoryTheory.Comma.mapRightIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) : Comma L R₁ ≌ Comma L R₂

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

@[simp]

theorem CategoryTheory.Comma.mapRightIso_counitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).counitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_counitIso_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).counitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_counitIso_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).counitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_functor_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).functor.obj X).hom = CategoryStruct.comp X.hom (i.hom.app X.right)

@[simp]

theorem CategoryTheory.Comma.mapRightIso_unitIso_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).inverse.obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_inverse_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : Comma L R₂} (f : X✝ ⟶ Y✝) : ((mapRightIso L i).inverse.map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_inverse_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).inverse.obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_functor_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ ⟶ Y✝) : ((mapRightIso L i).functor.map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_counitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).counitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_functor_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).functor.obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_inverse_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₂) : ((mapRightIso L i).inverse.obj X).hom = CategoryStruct.comp X.hom (i.inv.app X.right)

@[simp]

theorem CategoryTheory.Comma.mapRightIso_functor_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).functor.obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_unitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) (X : Comma L R₁) : ((mapRightIso L i).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.mapRightIso_functor_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ ⟶ Y✝) : ((mapRightIso L i).functor.map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.mapRightIso_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : Comma L R₂} (f : X✝ ⟶ Y✝) : ((mapRightIso L i).inverse.map f).left = f.left

def CategoryTheory.Comma.preLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) : Functor (Comma (F.comp L) R) (Comma L R)

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

@[simp]

theorem CategoryTheory.Comma.preLeft_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) : ((preLeft F L R).obj X).left = F.obj X.left

@[simp]

theorem CategoryTheory.Comma.preLeft_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) : ((preLeft F L R).obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.preLeft_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma (F.comp L) R} (f : X✝ ⟶ Y✝) : ((preLeft F L R).map f).left = F.map f.left

@[simp]

theorem CategoryTheory.Comma.preLeft_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) : ((preLeft F L R).obj X).hom = X.hom

@[simp]

theorem CategoryTheory.Comma.preLeft_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma (F.comp L) R} (f : X✝ ⟶ Y✝) : ((preLeft F L R).map f).right = f.right

def CategoryTheory.Comma.preLeftIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) : preLeft F L R ≅ map (F.comp L).rightUnitor.inv (CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)

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

instance CategoryTheory.Comma.instFaithfulCompPreLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) [F.Faithful] : (preLeft F L R).Faithful

instance CategoryTheory.Comma.instFullCompPreLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) [F.Full] : (preLeft F L R).Full

instance CategoryTheory.Comma.instEssSurjCompPreLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) [F.EssSurj] : (preLeft F L R).EssSurj

instance CategoryTheory.Comma.isEquivalence_preLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) [F.IsEquivalence] : (preLeft F L R).IsEquivalence

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

def CategoryTheory.Comma.preRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) : Functor (Comma L (F.comp R)) (Comma L R)

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

@[simp]

theorem CategoryTheory.Comma.preRight_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) : ((preRight L F R).obj X).hom = X.hom

@[simp]

theorem CategoryTheory.Comma.preRight_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) : ((preRight L F R).obj X).right = F.obj X.right

@[simp]

theorem CategoryTheory.Comma.preRight_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) : ((preRight L F R).obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.preRight_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) {X✝ Y✝ : Comma L (F.comp R)} (f : X✝ ⟶ Y✝) : ((preRight L F R).map f).left = f.left

@[simp]

theorem CategoryTheory.Comma.preRight_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) {X✝ Y✝ : Comma L (F.comp R)} (f : X✝ ⟶ Y✝) : ((preRight L F R).map f).right = F.map f.right

def CategoryTheory.Comma.preRightIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) : preRight L F R ≅ map (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.

instance CategoryTheory.Comma.instFaithfulCompPreRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) [F.Faithful] : (preRight L F R).Faithful

instance CategoryTheory.Comma.instFullCompPreRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) [F.Full] : (preRight L F R).Full

instance CategoryTheory.Comma.instEssSurjCompPreRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) [F.EssSurj] : (preRight L F R).EssSurj

instance CategoryTheory.Comma.isEquivalence_preRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) [F.IsEquivalence] : (preRight L F R).IsEquivalence

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

def CategoryTheory.Comma.post {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) : Functor (Comma L R) (Comma (L.comp F) (R.comp F))

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

@[simp]

theorem CategoryTheory.Comma.post_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) : ((post L R F).obj X).right = X.right

@[simp]

theorem CategoryTheory.Comma.post_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) : ((post L R F).obj X).hom = F.map X.hom

@[simp]

theorem CategoryTheory.Comma.post_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) : ((post L R F).obj X).left = X.left

@[simp]

theorem CategoryTheory.Comma.post_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : ((post L R F).map f).right = f.right

@[simp]

theorem CategoryTheory.Comma.post_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : ((post L R F).map f).left = f.left

def CategoryTheory.Comma.postIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) : post L R F ≅ map (L.comp F).leftUnitor.hom (R.comp F).leftUnitor.inv

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

instance CategoryTheory.Comma.instFaithfulCompPost {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) : (post L R F).Faithful

instance CategoryTheory.Comma.instFullCompPostOfFaithful {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) [F.Faithful] : (post L R F).Full

instance CategoryTheory.Comma.instEssSurjCompPostOfFull {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) [F.Full] : (post L R F).EssSurj

instance CategoryTheory.Comma.isEquivalence_post {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) [F.IsEquivalence] : (post L R F).IsEquivalence

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

def CategoryTheory.Comma.fromProd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) : Functor (A × B) (Comma L R)

The canonical functor from the product of two categories to the comma category of their respective functors into Discrete PUnit.

@[simp]

theorem CategoryTheory.Comma.fromProd_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((fromProd L R).map f).right = f.2

@[simp]

theorem CategoryTheory.Comma.fromProd_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : ((fromProd L R).obj X).left = X.1

@[simp]

theorem CategoryTheory.Comma.fromProd_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((fromProd L R).map f).left = f.1

@[simp]

theorem CategoryTheory.Comma.fromProd_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : ((fromProd L R).obj X).right = X.2

@[simp]

theorem CategoryTheory.Comma.fromProd_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : ((fromProd L R).obj X).hom = Discrete.eqToHom ⋯

def CategoryTheory.Comma.equivProd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) : Comma L R ≌ A × B

Taking the comma category of two functors into Discrete PUnit results in something is equivalent to their product.

@[simp]

theorem CategoryTheory.Comma.equivProd_functor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (a : Comma L R) : (equivProd L R).functor.obj a = (a.left, a.right)

@[simp]

theorem CategoryTheory.Comma.equivProd_unitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((equivProd L R).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.equivProd_unitIso_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((equivProd L R).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.equivProd_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((equivProd L R).inverse.map f).left = f.1

@[simp]

theorem CategoryTheory.Comma.equivProd_counitIso_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : (equivProd L R).counitIso.inv.app X = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.2)

@[simp]

theorem CategoryTheory.Comma.equivProd_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : ((equivProd L R).inverse.obj X).left = X.1

@[simp]

theorem CategoryTheory.Comma.equivProd_inverse_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((equivProd L R).inverse.map f).right = f.2

@[simp]

theorem CategoryTheory.Comma.equivProd_inverse_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : ((equivProd L R).inverse.obj X).right = X.2

@[simp]

theorem CategoryTheory.Comma.equivProd_unitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((equivProd L R).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.equivProd_functor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (equivProd L R).functor.map f = Prod.mkHom f.left f.right

@[simp]

theorem CategoryTheory.Comma.equivProd_unitIso_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((equivProd L R).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.equivProd_counitIso_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor B (Discrete PUnit.{u_1 + 1})) (X : A × B) : (equivProd L R).counitIso.hom.app X = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.2)

def CategoryTheory.Comma.toPUnitIdEquiv {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) : Comma L R ≌ A

Taking the comma category of a functor into A ⥤ Discrete PUnit and the identity Discrete PUnit ⥤ Discrete PUnit results in a category equivalent to A.

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((toPUnitIdEquiv L R).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : ((toPUnitIdEquiv L R).inverse.map f).left = f

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : A) : ((toPUnitIdEquiv L R).inverse.obj X).left = X

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_functor_obj {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : (toPUnitIdEquiv L R).functor.obj X = X.left

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_counitIso_hom_app {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : A) : (toPUnitIdEquiv L R).counitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : Comma L R) : ((toPUnitIdEquiv L R).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_counitIso_inv_app {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : A) : (toPUnitIdEquiv L R).counitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_right_as {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) (X : A) : ((toPUnitIdEquiv L R).inverse.obj X).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_functor_map {A : Type u₁} [Category.{v₁, u₁} A] (L : Functor A (Discrete PUnit.{u_1 + 1})) (R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (toPUnitIdEquiv L R).functor.map f = f.left

@[simp]

theorem CategoryTheory.Comma.toPUnitIdEquiv_functor_iso {A : Type u₁} [Category.{v₁, u₁} A] {L : Functor A (Discrete PUnit.{u_1 + 1})} {R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})} : (toPUnitIdEquiv L R).functor = fst L R

def CategoryTheory.Comma.toIdPUnitEquiv {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) : Comma L R ≌ B

Taking the comma category of the identity Discrete PUnit ⥤ Discrete PUnit and a functor B ⥤ Discrete PUnit results in a category equivalent to B.

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_right {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : B) : ((toIdPUnitEquiv L R).inverse.obj X).right = X

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_counitIso_hom_app {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : B) : (toIdPUnitEquiv L R).counitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_counitIso_inv_app {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : B) : (toIdPUnitEquiv L R).counitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_functor_map {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (toIdPUnitEquiv L R).functor.map f = f.right

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_functor_obj {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : Comma L R) : (toIdPUnitEquiv L R).functor.obj X = X.right

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_right {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : ((toIdPUnitEquiv L R).inverse.map f).right = f

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : Comma L R) : ((toIdPUnitEquiv L R).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_right {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : Comma L R) : ((toIdPUnitEquiv L R).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_left_as {B : Type u₂} [Category.{v₂, u₂} B] (L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})) (R : Functor B (Discrete PUnit.{u_2 + 1})) (X : B) : ((toIdPUnitEquiv L R).inverse.obj X).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.Comma.toIdPUnitEquiv_functor_iso {B : Type u₂} [Category.{v₂, u₂} B] {L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})} {R : Functor B (Discrete PUnit.{u_2 + 1})} : (toIdPUnitEquiv L R).functor = snd L R

def CategoryTheory.Comma.opFunctor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : Functor (Comma L R) (Comma R.op L.op)ᵒᵖ

The canonical functor from Comma L R to (Comma R.op L.op)ᵒᵖ.

@[simp]

theorem CategoryTheory.Comma.opFunctor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) : (opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }

@[simp]

theorem CategoryTheory.Comma.opFunctor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) : (opFunctor L R).map f = Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := ⋯ }

def CategoryTheory.Comma.opFunctorCompFst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opFunctor L R).leftOp.comp (fst R.op L.op) ≅ (snd L R).op

Composing the leftOp of opFunctor L R with fst L.op R.op is naturally isomorphic to snd L R.

@[simp]

theorem CategoryTheory.Comma.opFunctorCompFst_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : (Comma L R)ᵒᵖ) : (opFunctorCompFst L R).inv.app X = CategoryStruct.id (Opposite.op (Opposite.unop X).right)

@[simp]

theorem CategoryTheory.Comma.opFunctorCompFst_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : (Comma L R)ᵒᵖ) : (opFunctorCompFst L R).hom.app X = CategoryStruct.id (Opposite.op (Opposite.unop X).right)

def CategoryTheory.Comma.opFunctorCompSnd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opFunctor L R).leftOp.comp (snd R.op L.op) ≅ (fst L R).op

Composing the leftOp of opFunctor L R with snd L.op R.op is naturally isomorphic to fst L R.

@[simp]

theorem CategoryTheory.Comma.opFunctorCompSnd_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : (Comma L R)ᵒᵖ) : (opFunctorCompSnd L R).inv.app X = CategoryStruct.id (Opposite.op (Opposite.unop X).left)

@[simp]

theorem CategoryTheory.Comma.opFunctorCompSnd_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : (Comma L R)ᵒᵖ) : (opFunctorCompSnd L R).hom.app X = CategoryStruct.id (Opposite.op (Opposite.unop X).left)

def CategoryTheory.Comma.unopFunctor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : Functor (Comma L.op R.op) (Comma R L)ᵒᵖ

The canonical functor from Comma L.op R.op to (Comma R L)ᵒᵖ.

@[simp]

theorem CategoryTheory.Comma.unopFunctor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) : (unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }

@[simp]

theorem CategoryTheory.Comma.unopFunctor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L.op R.op} (f : X✝ ⟶ Y✝) : (unopFunctor L R).map f = Opposite.op { left := f.right.unop, right := f.left.unop, w := ⋯ }

def CategoryTheory.Comma.unopFunctorCompFst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (unopFunctor L R).comp (fst R L).op ≅ snd L.op R.op

Composing unopFunctor L R with (fst L R).op is isomorphic to snd L.op R.op.

@[simp]

theorem CategoryTheory.Comma.unopFunctorCompFst_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) : (unopFunctorCompFst L R).inv.app X = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Comma.unopFunctorCompFst_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) : (unopFunctorCompFst L R).hom.app X = CategoryStruct.id X.right

def CategoryTheory.Comma.unopFunctorCompSnd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (unopFunctor L R).comp (snd R L).op ≅ fst L.op R.op

Composing unopFunctor L R with (snd L R).op is isomorphic to fst L.op R.op.

@[simp]

theorem CategoryTheory.Comma.unopFunctorCompSnd_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) : (unopFunctorCompSnd L R).hom.app X = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Comma.unopFunctorCompSnd_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) : (unopFunctorCompSnd L R).inv.app X = CategoryStruct.id X.left

def CategoryTheory.Comma.opEquiv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : Comma L R ≌ (Comma R.op L.op)ᵒᵖ

The canonical equivalence between Comma L R and (Comma R.op L.op)ᵒᵖ.

@[simp]

theorem CategoryTheory.Comma.opEquiv_unitIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opEquiv L R).unitIso = NatIso.ofComponents (fun (X : Comma L R) => Iso.refl ((Functor.id (Comma L R)).obj X)) ⋯

@[simp]

theorem CategoryTheory.Comma.opEquiv_functor {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opEquiv L R).functor = opFunctor L R

@[simp]

theorem CategoryTheory.Comma.opEquiv_counitIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opEquiv L R).counitIso = NatIso.ofComponents (fun (X : (Comma R.op L.op)ᵒᵖ) => Iso.refl (((unopFunctor R L).leftOp.comp (opFunctor L R)).obj X)) ⋯

@[simp]

theorem CategoryTheory.Comma.opEquiv_inverse {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) : (opEquiv L R).inverse = (unopFunctor R L).leftOp