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₁}
[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]
:
Equations
- CategoryTheory.Comma.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id default } }
theorem
CategoryTheory.CommaMorphism.ext_iff
{A : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃}
{inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R} {x y : CategoryTheory.CommaMorphism X Y}, x = y ↔ x.left = y.left ∧ x.right = y.right
theorem
CategoryTheory.CommaMorphism.ext
{A : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃}
{inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R} {x y : CategoryTheory.CommaMorphism X Y}, x.left = y.left → x.right = y.right → x = y
structure
CategoryTheory.CommaMorphism
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
(X : CategoryTheory.Comma L R)
(Y : CategoryTheory.Comma L R)
:
Type (max v₁ v₂)
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}
:
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}
:
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)
:
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)
:
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 ⋯
@[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
@[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
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_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
@[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
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_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
@[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_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
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_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_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_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_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)
@[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)
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_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_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
:
∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeft R l).map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapLeft_obj_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_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_map_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
:
∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeft R l).map f).right = f.right
def
CategoryTheory.Comma.mapLeft
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
:
CategoryTheory.Functor (CategoryTheory.Comma L₂ R) (CategoryTheory.Comma L₁ R)
A natural transformation L₁ ⟶ L₂ induces a functor Comma L₂ R ⥤ Comma L₁ R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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
@[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_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
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)
:
The functor Comma L R ⥤ Comma L R induced by the identity natural transformation on L is
naturally isomorphic to the identity functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Comma.mapLeftComp_inv_app_right
{A : Type u₁}
[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
@[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
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_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_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₁ ⟶ L₂)
(h : l = l')
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftEq R l l' h).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_hom_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₁ ⟶ L₂)
(h : l = l')
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftEq R l l' h).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_inv_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₁ ⟶ L₂)
(h : l = l')
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftEq R l l' h).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
def
CategoryTheory.Comma.mapLeftEq
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
(l' : L₁ ⟶ L₂)
(h : l = l')
:
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_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_counitIso_inv_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_obj_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).left = X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
:
∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_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_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_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_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_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_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
:
∀ {X Y : CategoryTheory.Comma L₁ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_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_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_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_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_obj_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ : CategoryTheory.Functor A T}
{L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
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_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRight L r).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_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
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRight L r).obj X).right = X.right
@[simp]
theorem
CategoryTheory.Comma.mapRight_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
:
∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRight L r).map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapRight_map_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
:
∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRight L r).map f).right = f.right
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_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_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_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
@[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
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)
:
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_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
@[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_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
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_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
@[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
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')
:
Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors
Comma L R₁ ⥤ Comma L R₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_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_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_inverse_map_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
:
∀ {X Y : CategoryTheory.Comma L R₂} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_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_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_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_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_unitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_obj_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_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_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_functor_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
:
∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).functor.map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_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_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_functor_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ : CategoryTheory.Functor B T}
{R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).functor.obj X).right = X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_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
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_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_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_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
@[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
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_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_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
@[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_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
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_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_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.post L R F).obj X).right = X.right
@[simp]
theorem
CategoryTheory.Comma.post_obj_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.post L R F).obj X).hom = F.map X.hom
@[simp]
theorem
CategoryTheory.Comma.post_obj_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.post L R F).obj X).left = X.left
@[simp]
theorem
CategoryTheory.Comma.post_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
:
∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), ((CategoryTheory.Comma.post L R F).map f).left = f.left
def
CategoryTheory.Comma.post
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
:
CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma (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_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_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
@[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_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_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
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_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_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_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_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_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_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_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_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_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_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_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
@[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)
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_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_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_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_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} ))
:
@[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_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_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_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_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_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_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
@[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)
:
⋯ = ⋯
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
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_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_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_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_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_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_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_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_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_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} ))
:
@[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_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_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
@[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
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
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