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 functorsLandR.Over X: the over category of the objectX(developed inOver.lean).Under X: the under category of the objectX(also developed inOver.lean).Arrow T: the arrow category of the categoryT(developed inArrow.lean).
References #
Tags #
comma, slice, coslice, over, under, arrow
structure
CategoryTheory.Comma
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
Type (max u₁ u₂ v₃)
The objects of the comma category are triples of an object left : A, an object
right : B and a morphism hom : L.obj left ⟶ R.obj right.
- left : A
- right : B
instance
CategoryTheory.Comma.inhabited
{T : Type u₃}
[Category.{v₃, u₃} T]
[Inhabited T]
:
Inhabited (Comma (Functor.id T) (Functor.id T))
Equations
- CategoryTheory.Comma.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id default } }
structure
CategoryTheory.CommaMorphism
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
(X Y : Comma L R)
:
Type (max v₁ v₂)
A morphism between two objects in the comma category is a commutative square connecting the
morphisms coming from the two objects using morphisms in the image of the functors L and R.
Instances For
theorem
CategoryTheory.CommaMorphism.ext
{A : Type u₁}
{inst✝ : Category.{v₁, u₁} A}
{B : Type u₂}
{inst✝¹ : Category.{v₂, u₂} B}
{T : Type u₃}
{inst✝² : Category.{v₃, u₃} T}
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
{x y : CommaMorphism X Y}
(left : x.left = y.left)
(right : x.right = y.right)
:
instance
CategoryTheory.CommaMorphism.inhabited
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
[Inhabited (Comma L R)]
:
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₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(self : CommaMorphism X Y)
{Z : T}
(h : R.obj Y.right ⟶ Z)
:
CategoryStruct.comp (L.map self.left) (CategoryStruct.comp Y.hom h) = CategoryStruct.comp X.hom (CategoryStruct.comp (R.map self.right) h)
instance
CategoryTheory.commaCategory
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
:
Equations
theorem
CategoryTheory.Comma.hom_ext
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(f g : X ⟶ Y)
(h₁ : f.left = g.left)
(h₂ : f.right = g.right)
:
@[simp]
theorem
CategoryTheory.Comma.id_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X : Comma L R}
:
@[simp]
theorem
CategoryTheory.Comma.id_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X : Comma L R}
:
@[simp]
theorem
CategoryTheory.Comma.comp_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y Z : Comma L R}
{f : X ⟶ Y}
{g : Y ⟶ Z}
:
@[simp]
theorem
CategoryTheory.Comma.comp_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y Z : Comma L R}
{f : X ⟶ Y}
{g : Y ⟶ Z}
:
def
CategoryTheory.Comma.fst
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
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 := ⋯ }
@[simp]
theorem
CategoryTheory.Comma.fst_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.fst_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.snd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
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 := ⋯ }
@[simp]
theorem
CategoryTheory.Comma.snd_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.snd_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.natTrans
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
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 := ⋯ }
@[simp]
theorem
CategoryTheory.Comma.natTrans_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.eqToHom_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X Y : Comma L R)
(H : X = Y)
:
@[simp]
theorem
CategoryTheory.Comma.eqToHom_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X Y : Comma L R)
(H : X = Y)
:
instance
CategoryTheory.Comma.instIsIsoLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
instance
CategoryTheory.Comma.instIsIsoRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
@[simp]
theorem
CategoryTheory.Comma.inv_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
@[simp]
theorem
CategoryTheory.Comma.inv_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
theorem
CategoryTheory.Comma.left_hom_inv_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
theorem
CategoryTheory.Comma.inv_left_hom_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor A T}
{R : Functor B T}
{X Y : Comma L R}
(e : X ⟶ Y)
[IsIso e]
:
def
CategoryTheory.Comma.leftIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
Extract the isomorphism between the left objects from an isomorphism in the comma category.
Equations
- CategoryTheory.Comma.leftIso α = (CategoryTheory.Comma.fst L₁ R₁).mapIso α
@[simp]
theorem
CategoryTheory.Comma.leftIso_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
@[simp]
theorem
CategoryTheory.Comma.leftIso_inv
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
def
CategoryTheory.Comma.rightIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
Extract the isomorphism between the right objects from an isomorphism in the comma category.
Equations
- CategoryTheory.Comma.rightIso α = (CategoryTheory.Comma.snd L₁ R₁).mapIso α
@[simp]
theorem
CategoryTheory.Comma.rightIso_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
@[simp]
theorem
CategoryTheory.Comma.rightIso_inv
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(α : X ≅ Y)
:
def
CategoryTheory.Comma.isoMk
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat)
:
Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.
@[simp]
theorem
CategoryTheory.Comma.isoMk_hom_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat)
:
@[simp]
theorem
CategoryTheory.Comma.isoMk_hom_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat)
:
@[simp]
theorem
CategoryTheory.Comma.isoMk_inv_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat)
:
@[simp]
theorem
CategoryTheory.Comma.isoMk_inv_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L₁ : Functor A T}
{R₁ : Functor B T}
{X Y : Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat)
:
def
CategoryTheory.Comma.map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
:
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.
@[simp]
theorem
CategoryTheory.Comma.map_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.map_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
{X Y : Comma L R}
(φ : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Comma.map_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.map_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.map_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
{X Y : Comma L R}
(φ : X ⟶ Y)
:
instance
CategoryTheory.Comma.faithful_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[F₁.Faithful]
[F₂.Faithful]
:
instance
CategoryTheory.Comma.full_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[F.Faithful]
[F₁.Full]
[F₂.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.Comma.essSurj_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[F₁.EssSurj]
[F₂.EssSurj]
[F.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.Comma.isEquivalenceMap
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[F₁.IsEquivalence]
[F₂.IsEquivalence]
[F.Faithful]
[F.Full]
[IsIso α]
[IsIso β]
:
(map α β).IsEquivalence
@[simp]
theorem
CategoryTheory.Comma.map_fst
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
:
The equality between map α β ⋙ fst L' R' and fst L R ⋙ F₁,
where α : F₁ ⋙ L' ⟶ L ⋙ F.
def
CategoryTheory.Comma.mapFst
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
:
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.
@[simp]
theorem
CategoryTheory.Comma.mapFst_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapFst_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.map_snd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
:
The equality between map α β ⋙ snd L' R' and snd L R ⋙ F₂,
where β : R ⋙ F ⟶ F₂ ⋙ R'.
def
CategoryTheory.Comma.mapSnd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
:
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.
@[simp]
theorem
CategoryTheory.Comma.mapSnd_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapSnd_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{A' : Type u₄}
[Category.{v₄, u₄} A']
{B' : Type u₅}
[Category.{v₅, u₅} B']
{T' : Type u₆}
[Category.{v₆, u₆} T']
{L : Functor A T}
{R : Functor B T}
{L' : Functor A' T'}
{R' : Functor B' T'}
{F₁ : Functor A A'}
{F₂ : Functor B B'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : Comma L R)
:
def
CategoryTheory.Comma.mapLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
:
A natural transformation L₁ ⟶ L₂ induces a functor Comma L₂ R ⥤ Comma L₁ R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapLeft_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeft_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
{X✝ Y✝ : Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeft_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeft_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeft_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l : L₁ ⟶ L₂)
{X✝ Y✝ : Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.mapLeftId
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
The functor Comma L R ⥤ Comma L R induced by the identity natural transformation on L is
naturally isomorphic to the identity functor.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
def
CategoryTheory.Comma.mapLeftComp
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ L₃ : Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
:
The functor Comma L₁ R ⥤ Comma L₃ R induced by the composition of two natural transformations
l : L₁ ⟶ L₂ and l' : L₂ ⟶ L₃ is naturally isomorphic to the composition of the two functors
induced by these natural transformations.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapLeftComp_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ L₃ : Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : Comma L₃ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftComp_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ L₃ : Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : Comma L₃ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftComp_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ L₃ : Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : Comma L₃ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftComp_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ L₃ : Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₂ ⟶ L₃)
(X : Comma L₃ R)
:
def
CategoryTheory.Comma.mapLeftEq
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
:
Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors
Comma L₁ R ⥤ Comma L₂ R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : Comma L₂ R)
:
def
CategoryTheory.Comma.mapLeftIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
:
A natural isomorphism L₁ ≅ L₂ induces an equivalence of categories
Comma L₁ R ≌ Comma L₂ R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₂ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : Comma L₁ R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : Comma L₁ R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(R : Functor B T)
{L₁ L₂ : Functor A T}
(i : L₁ ≅ L₂)
(X : Comma L₁ R)
:
def
CategoryTheory.Comma.mapRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
:
A natural transformation R₁ ⟶ R₂ induces a functor Comma L R₁ ⥤ Comma L R₂.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapRight_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
{X✝ Y✝ : Comma L R₁}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRight_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r : R₁ ⟶ R₂)
{X✝ Y✝ : Comma L R₁}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.mapRightId
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
The functor Comma L R ⥤ Comma L R induced by the identity natural transformation on R is
naturally isomorphic to the identity functor.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapRightId_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightId_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightId_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightId_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
def
CategoryTheory.Comma.mapRightComp
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ R₃ : Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
:
The functor Comma L R₁ ⥤ Comma L R₃ induced by the composition of the natural transformations
r : R₁ ⟶ R₂ and r' : R₂ ⟶ R₃ is naturally isomorphic to the composition of the functors
induced by these natural transformations.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapRightComp_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ R₃ : Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightComp_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ R₃ : Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightComp_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ R₃ : Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightComp_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ R₃ : Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : Comma L R₁)
:
def
CategoryTheory.Comma.mapRightEq
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
:
Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors
Comma L R₁ ⥤ Comma L R₂.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapRightEq_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightEq_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightEq_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightEq_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
(X : Comma L R₁)
:
def
CategoryTheory.Comma.mapRightIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
:
A natural isomorphism R₁ ≅ R₂ induces an equivalence of categories
Comma L R₁ ≌ Comma L R₂.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : Comma L R₁}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : Comma L R₂}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : Comma L R₂}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : Comma L R₁}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₂)
:
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
{R₁ R₂ : Functor B T}
(i : R₁ ≅ R₂)
(X : Comma L R₁)
:
def
CategoryTheory.Comma.preLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
:
The functor (F ⋙ L, R) ⥤ (L, R)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.preLeft_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma (F.comp L) R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.preLeft_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
(X : Comma (F.comp L) R)
:
@[simp]
theorem
CategoryTheory.Comma.preLeft_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma (F.comp L) R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.preLeft_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
(X : Comma (F.comp L) R)
:
@[simp]
theorem
CategoryTheory.Comma.preLeft_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
(X : Comma (F.comp L) R)
:
def
CategoryTheory.Comma.preLeftIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
:
preLeft F L R ≅ map (F.comp L).rightUnitor.inv (CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
Comma.preLeft is a particular case of Comma.map,
but with better definitional properties.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Comma.instFaithfulCompPreLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
[F.Faithful]
:
instance
CategoryTheory.Comma.instFullCompPreLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
[F.Full]
:
instance
CategoryTheory.Comma.instEssSurjCompPreLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
[F.EssSurj]
:
instance
CategoryTheory.Comma.isEquivalence_preLeft
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(F : Functor C A)
(L : Functor A T)
(R : Functor B T)
[F.IsEquivalence]
:
(preLeft F L R).IsEquivalence
If F is an equivalence, then so is preLeft F L R.
def
CategoryTheory.Comma.preRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
:
The functor (F ⋙ L, R) ⥤ (L, R)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.preRight_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
(X : Comma L (F.comp R))
:
@[simp]
theorem
CategoryTheory.Comma.preRight_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
(X : Comma L (F.comp R))
:
@[simp]
theorem
CategoryTheory.Comma.preRight_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
(X : Comma L (F.comp R))
:
@[simp]
theorem
CategoryTheory.Comma.preRight_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
{X✝ Y✝ : Comma L (F.comp R)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.preRight_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
{X✝ Y✝ : Comma L (F.comp R)}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.preRightIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
:
preRight L F R ≅ map (CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv) (F.comp R).rightUnitor.hom
Comma.preRight is a particular case of Comma.map,
but with better definitional properties.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Comma.instFaithfulCompPreRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
[F.Faithful]
:
instance
CategoryTheory.Comma.instFullCompPreRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
[F.Full]
:
instance
CategoryTheory.Comma.instEssSurjCompPreRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
[F.EssSurj]
:
instance
CategoryTheory.Comma.isEquivalence_preRight
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(F : Functor C B)
(R : Functor B T)
[F.IsEquivalence]
:
(preRight L F R).IsEquivalence
If F is an equivalence, then so is preRight L F R.
def
CategoryTheory.Comma.post
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
:
The functor (L, R) ⥤ (L ⋙ F, R ⋙ F)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.post_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.post_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.post_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.post_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.post_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
(X : Comma L R)
:
def
CategoryTheory.Comma.postIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
:
Comma.post 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.
instance
CategoryTheory.Comma.instFaithfulCompPost
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
:
instance
CategoryTheory.Comma.instFullCompPostOfFaithful
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
[F.Faithful]
:
instance
CategoryTheory.Comma.instEssSurjCompPostOfFull
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
[F.Full]
:
instance
CategoryTheory.Comma.isEquivalence_post
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
{C : Type u₄}
[Category.{v₄, u₄} C]
(L : Functor A T)
(R : Functor B T)
(F : Functor T C)
[F.IsEquivalence]
:
(post L R F).IsEquivalence
If F is an equivalence, then so is post L R F.
def
CategoryTheory.Comma.fromProd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
:
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.
@[simp]
theorem
CategoryTheory.Comma.fromProd_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
{X Y : A × B}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Comma.fromProd_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.fromProd_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.fromProd_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
{X Y : A × B}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Comma.fromProd_obj_hom
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
def
CategoryTheory.Comma.equivProd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
:
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.
@[simp]
theorem
CategoryTheory.Comma.equivProd_inverse_map_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
{X Y : A × B}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_functor_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(a : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_inverse_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_functor_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_hom_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_counitIso_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_inv_app_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_inverse_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
{X Y : A × B}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_inverse_obj_right
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_counitIso_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor B (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
def
CategoryTheory.Comma.toPUnitIdEquiv
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
:
Taking the comma category of a functor into A ⥤ Discrete PUnit and the identity
Discrete PUnit ⥤ Discrete PUnit results in a category equivalent to A.
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_left
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : A}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_functor_map
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_counitIso_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : A)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_left
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : A)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_counitIso_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : A)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_right_as
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : A)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_functor_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
(L : Functor A (Discrete PUnit.{u_1 + 1}))
(R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_functor_iso
{A : Type u₁}
[Category.{v₁, u₁} A]
{L : Functor A (Discrete PUnit.{u_1 + 1})}
{R : Functor (Discrete PUnit.{u_2 + 1}) (Discrete PUnit.{u_1 + 1})}
:
def
CategoryTheory.Comma.toIdPUnitEquiv
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
:
Taking the comma category of the identity Discrete PUnit ⥤ Discrete PUnit
and a functor B ⥤ Discrete PUnit results in a category equivalent to B.
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_right
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
{X✝ Y✝ : B}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_right
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : B)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_right
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_left_as
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : B)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_counitIso_hom_app
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : B)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_counitIso_inv_app
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : B)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_functor_map
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_functor_obj
{B : Type u₂}
[Category.{v₂, u₂} B]
(L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1}))
(R : Functor B (Discrete PUnit.{u_2 + 1}))
(X : Comma L R)
:
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_functor_iso
{B : Type u₂}
[Category.{v₂, u₂} B]
{L : Functor (Discrete PUnit.{u_1 + 1}) (Discrete PUnit.{u_2 + 1})}
{R : Functor B (Discrete PUnit.{u_2 + 1})}
:
def
CategoryTheory.Comma.opFunctor
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
The canonical functor from Comma L R to (Comma R.op L.op)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.opFunctor_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma L R}
(f : X✝ ⟶ Y✝)
:
(opFunctor L R).map f = Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := ⋯ }
@[simp]
theorem
CategoryTheory.Comma.opFunctor_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L R)
:
(opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
def
CategoryTheory.Comma.opFunctorCompFst
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
Composing the leftOp of opFunctor L R with fst L.op R.op is naturally isomorphic
to snd L R.
Equations
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompFst_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : (Comma L R)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompFst_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : (Comma L R)ᵒᵖ)
:
def
CategoryTheory.Comma.opFunctorCompSnd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
Composing the leftOp of opFunctor L R with snd L.op R.op is naturally isomorphic
to fst L R.
Equations
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompSnd_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : (Comma L R)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompSnd_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : (Comma L R)ᵒᵖ)
:
def
CategoryTheory.Comma.unopFunctor
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
The canonical functor from Comma L.op R.op to (Comma R L)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.unopFunctor_obj
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L.op R.op)
:
(unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }
@[simp]
theorem
CategoryTheory.Comma.unopFunctor_map
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
{X✝ Y✝ : Comma L.op R.op}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comma.unopFunctorCompFst
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
Composing unopFunctor L R with (fst L R).op is isomorphic to snd L.op R.op.
Equations
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompFst_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L.op R.op)
:
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompFst_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L.op R.op)
:
def
CategoryTheory.Comma.unopFunctorCompSnd
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
Composing unopFunctor L R with (snd L R).op is isomorphic to fst L.op R.op.
Equations
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompSnd_hom_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L.op R.op)
:
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompSnd_inv_app
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
(X : Comma L.op R.op)
:
def
CategoryTheory.Comma.opEquiv
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
The canonical equivalence between Comma L R and (Comma R.op L.op)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Comma.opEquiv_counitIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
@[simp]
theorem
CategoryTheory.Comma.opEquiv_unitIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
(opEquiv L R).unitIso = NatIso.ofComponents (fun (X : Comma L R) => Iso.refl ((Functor.id (Comma L R)).obj X)) ⋯
@[simp]
theorem
CategoryTheory.Comma.opEquiv_inverse
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
:
@[simp]
theorem
CategoryTheory.Comma.opEquiv_functor
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{T : Type u₃}
[Category.{v₃, u₃} T]
(L : Functor A T)
(R : Functor B T)
: