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

• left : A
• right : B
• hom : L.obj s.left ⟶ R.obj s.right

The objects of the comma category are triples of an object left : A, an object right : B and a morphism hom : L.obj left ⟶ R.obj right.

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

Equations

• CategoryTheory.Comma.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id default } }

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

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

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

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

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.

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

Equations

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

@[simp]

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

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

Equations

• CategoryTheory.commaCategory = CategoryTheory.Category.mk

theorem CategoryTheory.Comma.hom_ext {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (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₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L R} : (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Comma.fst L R = CategoryTheory.Functor.mk { obj := fun X => X.left, map := fun {X Y} f => f.left }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Comma.snd L R = CategoryTheory.Functor.mk { obj := fun X => X.right, map := fun {X Y} f => f.right }

@[simp]

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

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

We can interpret the commutative square constituting a morphism in the comma category as a natural transformation between the functors fst ⋙ L and snd ⋙ R from the comma category to T, where the components are given by the morphism that constitutes an object of the comma category.

Equations

• CategoryTheory.Comma.natTrans L R = CategoryTheory.NatTrans.mk fun X => X.hom

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Comma.isoMk_inv_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (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✝) : (CategoryTheory.Comma.isoMk l r).inv.right = r.inv

@[simp]

theorem CategoryTheory.Comma.isoMk_hom_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (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✝) : (CategoryTheory.Comma.isoMk l r).hom.left = l.hom

@[simp]

theorem CategoryTheory.Comma.isoMk_inv_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (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✝) : (CategoryTheory.Comma.isoMk l r).inv.left = l.inv

@[simp]

theorem CategoryTheory.Comma.isoMk_hom_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (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✝) : (CategoryTheory.Comma.isoMk l r).hom.right = r.hom

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

• CategoryTheory.Comma.isoMk l r = CategoryTheory.Iso.mk (CategoryTheory.CommaMorphism.mk l.hom r.hom) (CategoryTheory.CommaMorphism.mk l.inv r.inv)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

• @CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreLeft = @CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreLeft.proof_1

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

Equations

• CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreLeft F L R = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.CommaMorphism.mk (F.preimage f.left) f.right

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

Equations

• @CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreLeft = @CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreLeft.proof_1

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

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

Equations

• CategoryTheory.Comma.isEquivalencePreLeft F L R = let_fun this := (_ : CategoryTheory.EssSurj F); CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj (CategoryTheory.Comma.preLeft F L R)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

• @CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreRight = @CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreRight.proof_1

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

Equations

• CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreRight L F R = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.CommaMorphism.mk f.left (F.preimage f.right)

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

Equations

• @CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreRight = @CategoryTheory.Comma.instEssSurjCommaCompCommaCommaCategoryCommaCategoryPreRight.proof_1

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

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

Equations

• CategoryTheory.Comma.isEquivalencePreRight L F R = let_fun this := (_ : CategoryTheory.EssSurj F); CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj (CategoryTheory.Comma.preRight L F R)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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