Documentation

Mathlib.CategoryTheory.Comma.Basic

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

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

left : A
right : B
hom : L.obj self.left ⟶ R.obj self.right

Instances For

instance CategoryTheory.Comma.inhabited {T : Type u₃} [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 {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

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

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

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
right : X.right ⟶ Y.right
w : CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map self.right)

Instances For

@[simp]

theorem CategoryTheory.CommaMorphism.w {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) :

CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map self.right)

instance CategoryTheory.CommaMorphism.inhabited {A : Type u₁} [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

CategoryTheory.CommaMorphism.inhabited = { default := { left := CategoryTheory.CategoryStruct.id default.left, right := CategoryTheory.CategoryStruct.id default.right, w := ⋯ } }

@[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_iff {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} :

f = g ↔ f.left = g.left ∧ f.right = g.right

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 = { obj := fun (X : CategoryTheory.Comma L R) => X.left, map := fun {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y) => f.left, map_id := ⋯, map_comp := ⋯ }

Instances For

@[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 = { obj := fun (X : CategoryTheory.Comma L R) => X.right, map := fun {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y) => f.right, map_id := ⋯, map_comp := ⋯ }

Instances For

@[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.Comma.fst L R).comp L ⟶ (CategoryTheory.Comma.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.

Equations

CategoryTheory.Comma.natTrans L R = { app := fun (X : CategoryTheory.Comma L R) => X.hom, naturality := ⋯ }

Instances For

@[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 ⋯

@[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 ⋯

instance CategoryTheory.Comma.instIsIsoLeft {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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

CategoryTheory.IsIso e.left

Equations

⋯ = ⋯

instance CategoryTheory.Comma.instIsIsoRight {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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

CategoryTheory.IsIso e.right

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.Comma.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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

(CategoryTheory.inv e).left = CategoryTheory.inv e.left

@[simp]

theorem CategoryTheory.Comma.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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

(CategoryTheory.inv e).right = CategoryTheory.inv e.right

theorem CategoryTheory.Comma.left_hom_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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

CategoryTheory.CategoryStruct.comp (L.map e.left) (CategoryTheory.CategoryStruct.comp Y.hom (R.map (CategoryTheory.inv e.right))) = X.hom

theorem CategoryTheory.Comma.inv_left_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} (e : X ⟶ Y) [CategoryTheory.IsIso e] :

CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.inv e.left)) (CategoryTheory.CategoryStruct.comp X.hom (R.map e.right)) = Y.hom

@[simp]

theorem CategoryTheory.Comma.leftIso_inv {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₁} (α : X ≅ Y) :

(CategoryTheory.Comma.leftIso α).inv = α.inv.left

@[simp]

theorem CategoryTheory.Comma.leftIso_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} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) :

(CategoryTheory.Comma.leftIso α).hom = α.hom.left

def CategoryTheory.Comma.leftIso {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₁} (α : X ≅ Y) :

X.left ≅ Y.left

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

Equations

CategoryTheory.Comma.leftIso α = (CategoryTheory.Comma.fst L₁ R₁).mapIso α

Instances For

@[simp]

theorem CategoryTheory.Comma.rightIso_inv {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₁} (α : X ≅ Y) :

(CategoryTheory.Comma.rightIso α).inv = α.inv.right

@[simp]

theorem CategoryTheory.Comma.rightIso_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} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) :

(CategoryTheory.Comma.rightIso α).hom = α.hom.right

def CategoryTheory.Comma.rightIso {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₁} (α : X ≅ Y) :

X.right ≅ Y.right

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

Equations

CategoryTheory.Comma.rightIso α = (CategoryTheory.Comma.snd L₁ R₁).mapIso α

Instances For

@[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 h).inv.left = l.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 h).hom.left = l.hom

@[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 h).inv.right = r.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 h).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 h = { hom := { left := l.hom, right := r.hom, w := h }, inv := { left := l.inv, right := r.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) :

((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) :

((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))

def CategoryTheory.Comma.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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') :

CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.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'.

Equations

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

Instances For

instance CategoryTheory.Comma.faithful_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.Faithful] [F₂.Faithful] :

(CategoryTheory.Comma.map α β).Faithful

Equations

⋯ = ⋯

instance CategoryTheory.Comma.full_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :

(CategoryTheory.Comma.map α β).Full

Equations

⋯ = ⋯

instance CategoryTheory.Comma.essSurj_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :

(CategoryTheory.Comma.map α β).EssSurj

Equations

⋯ = ⋯

noncomputable instance CategoryTheory.Comma.isEquivalenceMap {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :

(CategoryTheory.Comma.map α β).IsEquivalence

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') :

(CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') = (CategoryTheory.Comma.fst L R).comp F₁

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

(CategoryTheory.Comma.mapFst α β).inv.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)

@[simp]

theorem CategoryTheory.Comma.mapFst_hom_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

(CategoryTheory.Comma.mapFst α β).hom.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)

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

(CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') ≅ (CategoryTheory.Comma.fst L R).comp F₁

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

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Comma.map_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') :

(CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.snd L' R') = (CategoryTheory.Comma.snd L R).comp F₂

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

@[simp]

theorem CategoryTheory.Comma.mapSnd_inv_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

(CategoryTheory.Comma.mapSnd α β).inv.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)

@[simp]

theorem CategoryTheory.Comma.mapSnd_hom_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] {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} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) :

(CategoryTheory.Comma.mapSnd α β).hom.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)

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

(CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.snd L' R') ≅ (CategoryTheory.Comma.snd L R).comp F₂

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

Equations

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

Instances For

@[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

@[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_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

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.

Instances For

@[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 X.left

@[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 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 X.right

@[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 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.

Instances For

@[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 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 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 X.left

@[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 X.right

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.Comma.mapLeft R l').comp (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.

Instances For

@[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_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

@[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

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.

Instances For

@[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_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_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_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_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_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_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_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_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_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_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_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_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_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

@[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_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

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.

Instances For

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

Instances For

@[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 X.right

@[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 X.left

@[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 X.left

@[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 X.right

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.

Instances For

@[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 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 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 X.left

@[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 X.right

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.Comma.mapRight L r).comp (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.

Instances For

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

Instances For

@[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_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_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_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_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

@[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_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_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_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_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_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_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_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_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_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_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

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.

Instances For

@[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 (F.comp L) R) :

((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right

@[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 (F.comp L) R) :

((CategoryTheory.Comma.preLeft F L R).obj X).hom = X.hom

@[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 (F.comp L) R) :

((CategoryTheory.Comma.preLeft F L R).obj X).left = F.obj X.left

@[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 (F.comp 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 (F.comp L) R} (f : X ⟶ Y), ((CategoryTheory.Comma.preLeft F L R).map f).right = f.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 (F.comp 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.

Instances For

def CategoryTheory.Comma.preLeftIso {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.Comma.preLeft F L R ≅ CategoryTheory.Comma.map (F.comp L).rightUnitor.inv (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)

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

Equations

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

Instances For

instance CategoryTheory.Comma.instFaithfulCompPreLeft {A : Type u₁} [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) [F.Faithful] :

(CategoryTheory.Comma.preLeft F L R).Faithful

Equations

⋯ = ⋯

instance CategoryTheory.Comma.instFullCompPreLeft {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) [F.Full] :

(CategoryTheory.Comma.preLeft F L R).Full

Equations

⋯ = ⋯

instance CategoryTheory.Comma.instEssSurjCompPreLeft {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) [F.EssSurj] :

(CategoryTheory.Comma.preLeft F L R).EssSurj

Equations

⋯ = ⋯

instance CategoryTheory.Comma.isEquivalence_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) [F.IsEquivalence] :

(CategoryTheory.Comma.preLeft F L R).IsEquivalence

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

Equations

⋯ = ⋯

@[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 (F.comp R)) :

((CategoryTheory.Comma.preRight L F R).obj X).left = X.left

@[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 (F.comp R)) :

((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom

@[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 (F.comp R)) :

((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right

@[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 (F.comp R)} (f : X ⟶ Y), ((CategoryTheory.Comma.preRight L F R).map f).right = F.map f.right

@[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 (F.comp R)} (f : X ⟶ Y), ((CategoryTheory.Comma.preRight L F R).map f).left = f.left

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 (F.comp 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.

Instances For

def CategoryTheory.Comma.preRightIso {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.Comma.preRight L F R ≅ CategoryTheory.Comma.map (CategoryTheory.CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv) (F.comp R).rightUnitor.hom

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

Equations

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

Instances For

instance CategoryTheory.Comma.instFaithfulCompPreRight {A : Type u₁} [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) [F.Faithful] :

(CategoryTheory.Comma.preRight L F R).Faithful

Equations

⋯ = ⋯

instance CategoryTheory.Comma.instFullCompPreRight {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) [F.Full] :

(CategoryTheory.Comma.preRight L F R).Full

Equations

⋯ = ⋯

instance CategoryTheory.Comma.instEssSurjCompPreRight {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) [F.EssSurj] :

(CategoryTheory.Comma.preRight L F R).EssSurj

Equations

⋯ = ⋯

instance CategoryTheory.Comma.isEquivalence_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) [F.IsEquivalence] :

(CategoryTheory.Comma.preRight L F R).IsEquivalence

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

Equations

⋯ = ⋯

@[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_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_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_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

@[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

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 (L.comp F) (R.comp F))

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

Equations

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

Instances For

@[simp]

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

((CategoryTheory.Comma.fromProd L R).map f).left = f.1

@[simp]

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

((CategoryTheory.Comma.fromProd L R).obj X).hom = CategoryTheory.Discrete.eqToHom ⋯

@[simp]

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

((CategoryTheory.Comma.fromProd L R).obj X).left = X.1

@[simp]

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

((CategoryTheory.Comma.fromProd L R).map f).right = f.2

@[simp]

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

((CategoryTheory.Comma.fromProd L R).obj X).right = X.2

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

CategoryTheory.Functor (A × B) (CategoryTheory.Comma L R)

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

Equations

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

Instances For

@[simp]

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

(CategoryTheory.Comma.equivProd L R).functor.obj a = (a.left, a.right)

@[simp]

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

(CategoryTheory.Comma.equivProd L R).counitIso.inv.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)

@[simp]

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

((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

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

((CategoryTheory.Comma.equivProd L R).inverse.obj X).right = X.2

@[simp]

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

((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

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

∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), (CategoryTheory.Comma.equivProd L R).functor.map f = (f.left, f.right)

@[simp]

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

((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

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

((CategoryTheory.Comma.equivProd L R).inverse.map f).left = f.1

@[simp]

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

((CategoryTheory.Comma.equivProd L R).inverse.obj X).left = X.1

@[simp]

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

⋯ = ⋯

@[simp]

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

((CategoryTheory.Comma.equivProd L R).inverse.map f).right = f.2

@[simp]

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

(CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)

@[simp]

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

((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left

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

CategoryTheory.Comma L R ≌ A × B

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

Equations

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

Instances For

@[simp]

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

∀ {X Y : A} (f : X ⟶ Y), ((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.map f).left = f

@[simp]

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

((CategoryTheory.Comma.toPUnitIdEquiv L R).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

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

(CategoryTheory.Comma.toPUnitIdEquiv L R).functor.obj X = X.left

@[simp]

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

∀ {X Y : A} (f : X ⟶ Y), ⋯ = ⋯

@[simp]

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

(CategoryTheory.Comma.toPUnitIdEquiv L R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

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

((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.obj X).left = X

@[simp]

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

⋯ = ⋯

@[simp]

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

⋯ = ⋯

@[simp]

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

∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), (CategoryTheory.Comma.toPUnitIdEquiv L R).functor.map f = f.left

@[simp]

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

⋯ = ⋯

@[simp]

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

(CategoryTheory.Comma.toPUnitIdEquiv L R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

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

((CategoryTheory.Comma.toPUnitIdEquiv L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

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

((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.obj X).right.as = PUnit.unit

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

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

Equations

CategoryTheory.Comma.toPUnitIdEquiv L R = (CategoryTheory.Comma.equivProd L R).trans (CategoryTheory.prod.rightUnitorEquivalence A)

Instances For

@[simp]

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

(CategoryTheory.Comma.toPUnitIdEquiv L R).functor = CategoryTheory.Comma.fst L R

@[simp]

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

(CategoryTheory.Comma.toIdPUnitEquiv L R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

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

((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.obj X).left.as = PUnit.unit

@[simp]

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

((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.obj X).right = X

@[simp]

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

∀ {X Y : B} (f : X ⟶ Y), ((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.map f).right = f

@[simp]

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

⋯ = ⋯

@[simp]

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

((CategoryTheory.Comma.toIdPUnitEquiv L R).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

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

((CategoryTheory.Comma.toIdPUnitEquiv L R).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

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

∀ {X Y : B} (f : X ⟶ Y), ⋯ = ⋯

@[simp]

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

⋯ = ⋯

@[simp]

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

⋯ = ⋯

@[simp]

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

(CategoryTheory.Comma.toIdPUnitEquiv L R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

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

(CategoryTheory.Comma.toIdPUnitEquiv L R).functor.obj X = X.right

@[simp]

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

∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), (CategoryTheory.Comma.toIdPUnitEquiv L R).functor.map f = f.right

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

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

Equations

CategoryTheory.Comma.toIdPUnitEquiv L R = (CategoryTheory.Comma.equivProd L R).trans (CategoryTheory.prod.leftUnitorEquivalence B)

Instances For

@[simp]

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

(CategoryTheory.Comma.toIdPUnitEquiv L R).functor = CategoryTheory.Comma.snd L R