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 } }
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 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
theorem
CategoryTheory.CommaMorphism.ext
{A : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} A}
{B : Type u₂}
{inst✝¹ : CategoryTheory.Category.{v₂, u₂} B}
{T : Type u₃}
{inst✝² : 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}
(left : x.left = y.left)
(right : x.right = y.right)
:
x = y
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 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
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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 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 Y 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 Y Z : CategoryTheory.Comma L R}
{f : X ⟶ Y}
{g : Y ⟶ Z}
:
(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
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.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.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.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
@[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
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.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
@[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 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 Y : CategoryTheory.Comma L R)
(H : X = Y)
:
(CategoryTheory.eqToHom H).right = CategoryTheory.eqToHom ⋯
instance
CategoryTheory.Comma.instIsIsoLeft
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
CategoryTheory.IsIso e.left
instance
CategoryTheory.Comma.instIsIsoRight
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
CategoryTheory.IsIso e.right
@[simp]
theorem
CategoryTheory.Comma.inv_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
(CategoryTheory.inv e).left = CategoryTheory.inv e.left
@[simp]
theorem
CategoryTheory.Comma.inv_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
(CategoryTheory.inv e).right = CategoryTheory.inv e.right
theorem
CategoryTheory.Comma.left_hom_inv_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
CategoryTheory.CategoryStruct.comp (L.map e.left)
(CategoryTheory.CategoryStruct.comp Y.hom (R.map (CategoryTheory.inv e.right))) = X.hom
theorem
CategoryTheory.Comma.inv_left_hom_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L R}
(e : X ⟶ Y)
[CategoryTheory.IsIso e]
:
CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.inv e.left))
(CategoryTheory.CategoryStruct.comp X.hom (R.map e.right)) = Y.hom
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 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.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 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 Y : CategoryTheory.Comma L₁ R₁}
(α : X ≅ Y)
:
(CategoryTheory.Comma.leftIso α).inv = α.inv.left
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 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.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 Y : CategoryTheory.Comma L₁ R₁}
(α : X ≅ Y)
:
(CategoryTheory.Comma.rightIso α).inv = α.inv.right
@[simp]
theorem
CategoryTheory.Comma.rightIso_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L₁ : CategoryTheory.Functor A T}
{R₁ : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L₁ R₁}
(α : X ≅ Y)
:
(CategoryTheory.Comma.rightIso α).hom = α.hom.right
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 Y : CategoryTheory.Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h :
CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by
aesop_cat)
:
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.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 Y : CategoryTheory.Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h :
CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by
aesop_cat)
:
(CategoryTheory.Comma.isoMk l r h).hom.left = l.hom
@[simp]
theorem
CategoryTheory.Comma.isoMk_inv_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{L₁ : CategoryTheory.Functor A T}
{R₁ : CategoryTheory.Functor B T}
{X Y : CategoryTheory.Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h :
CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by
aesop_cat)
:
(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 Y : CategoryTheory.Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h :
CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by
aesop_cat)
:
(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 Y : CategoryTheory.Comma L₁ R₁}
(l : X.left ≅ Y.left)
(r : X.right ≅ Y.right)
(h :
CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by
aesop_cat)
:
(CategoryTheory.Comma.isoMk l r h).inv.right = r.inv
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
@[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 Y : CategoryTheory.Comma L R}
(φ : X ⟶ Y)
:
((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right
@[simp]
theorem
CategoryTheory.Comma.map_obj_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{A' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} A']
{B' : Type u₅}
[CategoryTheory.Category.{v₅, u₅} B']
{T' : Type u₆}
[CategoryTheory.Category.{v₆, u₆} T']
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{L' : CategoryTheory.Functor A' T'}
{R' : CategoryTheory.Functor B' T'}
{F₁ : CategoryTheory.Functor A A'}
{F₂ : CategoryTheory.Functor B B'}
{F : CategoryTheory.Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
@[simp]
theorem
CategoryTheory.Comma.map_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{A' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} A']
{B' : Type u₅}
[CategoryTheory.Category.{v₅, u₅} B']
{T' : Type u₆}
[CategoryTheory.Category.{v₆, u₆} T']
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{L' : CategoryTheory.Functor A' T'}
{R' : CategoryTheory.Functor B' T'}
{F₁ : CategoryTheory.Functor A A'}
{F₂ : CategoryTheory.Functor B B'}
{F : CategoryTheory.Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
@[simp]
theorem
CategoryTheory.Comma.map_obj_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{A' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} A']
{B' : Type u₅}
[CategoryTheory.Category.{v₅, u₅} B']
{T' : Type u₆}
[CategoryTheory.Category.{v₆, u₆} T']
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{L' : CategoryTheory.Functor A' T'}
{R' : CategoryTheory.Functor B' T'}
{F₁ : CategoryTheory.Functor A A'}
{F₂ : CategoryTheory.Functor B B'}
{F : CategoryTheory.Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
@[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 Y : CategoryTheory.Comma L R}
(φ : X ⟶ Y)
:
((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left
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
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
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
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
@[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.
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.mapFst_inv_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{A' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} A']
{B' : Type u₅}
[CategoryTheory.Category.{v₅, u₅} B']
{T' : Type u₆}
[CategoryTheory.Category.{v₆, u₆} T']
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{L' : CategoryTheory.Functor A' T'}
{R' : CategoryTheory.Functor B' T'}
{F₁ : CategoryTheory.Functor A A'}
{F₂ : CategoryTheory.Functor B B'}
{F : CategoryTheory.Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : CategoryTheory.Comma L R)
:
(CategoryTheory.Comma.mapFst α β).inv.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
@[simp]
theorem
CategoryTheory.Comma.mapFst_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{A' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} A']
{B' : Type u₅}
[CategoryTheory.Category.{v₅, u₅} B']
{T' : Type u₆}
[CategoryTheory.Category.{v₆, u₆} T']
{L : CategoryTheory.Functor A T}
{R : CategoryTheory.Functor B T}
{L' : CategoryTheory.Functor A' T'}
{R' : CategoryTheory.Functor B' T'}
{F₁ : CategoryTheory.Functor A A'}
{F₂ : CategoryTheory.Functor B B'}
{F : CategoryTheory.Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
(X : CategoryTheory.Comma L R)
:
(CategoryTheory.Comma.mapFst α β).hom.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
@[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'.
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.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.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₁ 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.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₁ 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_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₁ 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_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₁ L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
{X✝ Y✝ : CategoryTheory.Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapLeft R l).map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapLeft_obj_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₁ 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_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₁ L₂ : CategoryTheory.Functor A T}
(l : L₁ ⟶ L₂)
{X✝ Y✝ : CategoryTheory.Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapLeft R l).map f).left = f.left
def
CategoryTheory.Comma.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.mapLeftId_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.mapLeftId L R).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_inv_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.mapLeftId L R).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftId_hom_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.mapLeftId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[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
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₁ L₂ 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.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₁ L₂ 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_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₁ L₂ 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_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₁ L₂ 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₁ L₂ 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.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₁ L₂ : CategoryTheory.Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
:
Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors
Comma L₁ R ⥤ Comma L₂ R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₁ L₂ : CategoryTheory.Functor A T}
(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_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₁ L₂ : CategoryTheory.Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftEq R l l' h).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_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₁ L₂ : CategoryTheory.Functor A T}
(l l' : L₁ ⟶ L₂)
(h : l = l')
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftEq R l l' h).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftEq_hom_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ L₂ : CategoryTheory.Functor A T}
(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
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₁ 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.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₁ 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_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₁ 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_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₁ 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_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₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_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₁ 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_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₁ 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_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₁ 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₁ 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_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₁ 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_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₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : CategoryTheory.Comma L₁ R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapLeftIso R i).functor.map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_map_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₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : CategoryTheory.Comma L₂ R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_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₁ 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_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₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_inverse_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ 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₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₂ R)
:
((CategoryTheory.Comma.mapLeftIso R i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_obj_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
(X : CategoryTheory.Comma L₁ R)
:
((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
@[simp]
theorem
CategoryTheory.Comma.mapLeftIso_functor_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(R : CategoryTheory.Functor B T)
{L₁ L₂ : CategoryTheory.Functor A T}
(i : L₁ ≅ L₂)
{X✝ Y✝ : CategoryTheory.Comma L₁ R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapLeftIso R i).functor.map f).left = f.left
def
CategoryTheory.Comma.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₁ 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.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₁ R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
{X✝ Y✝ : CategoryTheory.Comma L R₁}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapRight L r).map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_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₁ 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₁ 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_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₁ R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
{X✝ Y✝ : CategoryTheory.Comma L R₁}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapRight L r).map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapRight_obj_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₁ R₂ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRight L r).obj X).right = 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.mapRightId_hom_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.mapRightId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightId_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
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₁ R₂ 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.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₁ R₂ 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₁ R₂ R₃ : CategoryTheory.Functor B T}
(r : R₁ ⟶ R₂)
(r' : R₂ ⟶ R₃)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightComp L r r').hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapRightComp_inv_app_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ R₂ 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_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₁ R₂ 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.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₁ R₂ : CategoryTheory.Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
:
Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors
Comma L R₁ ⥤ Comma L R₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₁ R₂ : CategoryTheory.Functor B T}
(r r' : R₁ ⟶ R₂)
(h : r = r')
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightEq L r r' h).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightEq_inv_app_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₁ R₂ : CategoryTheory.Functor B T}
(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_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₁ R₂ : CategoryTheory.Functor B T}
(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₁ R₂ : CategoryTheory.Functor B T}
(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
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₁ 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.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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ 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_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₁ 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_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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_counitIso_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₁ 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_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₁ 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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : CategoryTheory.Comma L R₂}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapRightIso L i).inverse.map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_inverse_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₁ 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_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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₁)
:
((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_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₁ 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_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₁ 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_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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
(X : CategoryTheory.Comma L R₂)
:
((CategoryTheory.Comma.mapRightIso L i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ 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_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₁ 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_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₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : CategoryTheory.Comma L R₂}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapRightIso L i).inverse.map f).left = f.left
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_map_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
{R₁ R₂ : CategoryTheory.Functor B T}
(i : R₁ ≅ R₂)
{X✝ Y✝ : CategoryTheory.Comma L R₁}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.mapRightIso L i).functor.map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.mapRightIso_functor_obj_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₁ 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_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₁ 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
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
@[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_map_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(F : CategoryTheory.Functor C A)
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
{X✝ Y✝ : CategoryTheory.Comma (F.comp L) R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.preLeft F L R).map f).left = F.map f.left
@[simp]
theorem
CategoryTheory.Comma.preLeft_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(F : CategoryTheory.Functor C A)
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma (F.comp L) R)
:
((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right
@[simp]
theorem
CategoryTheory.Comma.preLeft_obj_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_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
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
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
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
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.
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
@[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_obj_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(F : CategoryTheory.Functor C B)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L (F.comp R))
:
((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right
@[simp]
theorem
CategoryTheory.Comma.preRight_map_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_hom
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(F : CategoryTheory.Functor C B)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L (F.comp R))
:
((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom
@[simp]
theorem
CategoryTheory.Comma.preRight_obj_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
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
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
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
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.
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.post_obj_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.post L R F).obj X).left = X.left
@[simp]
theorem
CategoryTheory.Comma.post_map_right
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
{C : Type u₄}
[CategoryTheory.Category.{v₄, u₄} C]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(F : CategoryTheory.Functor T C)
{X✝ Y✝ : CategoryTheory.Comma L R}
(f : X✝ ⟶ Y✝)
:
((CategoryTheory.Comma.post L R F).map f).right = f.right
@[simp]
theorem
CategoryTheory.Comma.post_obj_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_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.postIso
{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.Comma.post L R F ≅ CategoryTheory.Comma.map (L.comp F).leftUnitor.hom (R.comp F).leftUnitor.inv
Comma.post is a particular case of Comma.map, but with better definitional properties.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Comma.instFaithfulCompPost
{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.Comma.post L R F).Faithful
instance
CategoryTheory.Comma.instFullCompPostOfFaithful
{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)
[F.Faithful]
:
(CategoryTheory.Comma.post L R F).Full
instance
CategoryTheory.Comma.instEssSurjCompPostOfFull
{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)
[F.Full]
:
(CategoryTheory.Comma.post L R F).EssSurj
instance
CategoryTheory.Comma.isEquivalence_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)
[F.IsEquivalence]
:
(CategoryTheory.Comma.post L R F).IsEquivalence
If F is an equivalence, then so is post L R F.
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.fromProd_obj_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
((CategoryTheory.Comma.fromProd L R).obj X).left = X.1
@[simp]
theorem
CategoryTheory.Comma.fromProd_map_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 Y : A × B}
(f : X ⟶ Y)
:
((CategoryTheory.Comma.fromProd L R).map f).left = f.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_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 Y : A × B}
(f : X ⟶ Y)
:
((CategoryTheory.Comma.fromProd L R).map f).right = f.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 ⋯
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.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 Y : A × B}
(f : X ⟶ Y)
:
((CategoryTheory.Comma.equivProd L R).inverse.map f).left = f.1
@[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_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_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_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 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_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_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_functor_map
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : CategoryTheory.Comma L R}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Comma.equivProd L R).functor.map f = (f.left, f.right)
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_hom_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.equivProd_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_counitIso_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : A × B)
:
(CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
@[simp]
theorem
CategoryTheory.Comma.equivProd_unitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
def
CategoryTheory.Comma.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_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_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_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)
:
⋯ = ⋯
@[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_counitIso_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : A)
:
(CategoryTheory.Comma.toPUnitIdEquiv L R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.toPUnitIdEquiv L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_functor_map
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : CategoryTheory.Comma L R}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Comma.toPUnitIdEquiv L R).functor.map f = f.left
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_right_down_down
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : CategoryTheory.Comma L R)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_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_obj
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(X : CategoryTheory.Comma L R)
:
(CategoryTheory.Comma.toPUnitIdEquiv L R).functor.obj X = X.left
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_right_down_down
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
(L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
(R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1}))
{X✝ Y✝ : A}
(f : X✝ ⟶ Y✝)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comma.toPUnitIdEquiv_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
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_unitIso_inv_app_right
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.toIdPUnitEquiv L R).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : CategoryTheory.Comma L R)
:
((CategoryTheory.Comma.toIdPUnitEquiv L R).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_right
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : B)
:
((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.obj X).right = X
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_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_unitIso_inv_app_left_down_down
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : CategoryTheory.Comma L R)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_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_left_down_down
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : CategoryTheory.Comma L R)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_left_down_down
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
{X✝ Y✝ : B}
(f : X✝ ⟶ Y✝)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_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_counitIso_hom_app
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : B)
:
(CategoryTheory.Comma.toIdPUnitEquiv L R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_inverse_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_counitIso_inv_app
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : B)
:
(CategoryTheory.Comma.toIdPUnitEquiv L R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_functor_obj
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1}))
(X : CategoryTheory.Comma L R)
:
(CategoryTheory.Comma.toIdPUnitEquiv L R).functor.obj X = X.right
@[simp]
theorem
CategoryTheory.Comma.toIdPUnitEquiv_functor_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
def
CategoryTheory.Comma.opFunctor
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
:
CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma R.op L.op)ᵒᵖ
The canonical functor from Comma L R to (Comma R.op L.op)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Comma.opFunctor_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.opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
@[simp]
theorem
CategoryTheory.Comma.opFunctor_map
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opFunctor L R).map f = Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := ⋯ }
def
CategoryTheory.Comma.opFunctorCompFst
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opFunctor L R).leftOp.comp (CategoryTheory.Comma.fst R.op L.op) ≅ (CategoryTheory.Comma.snd L R).op
Composing the leftOp of opFunctor L R with fst L.op R.op is naturally isomorphic
to snd L R.
Equations
- CategoryTheory.Comma.opFunctorCompFst L R = CategoryTheory.Iso.refl ((CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.fst R.op L.op))
Instances For
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompFst_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : (CategoryTheory.Comma L R)ᵒᵖ)
:
(CategoryTheory.Comma.opFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompFst_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : (CategoryTheory.Comma L R)ᵒᵖ)
:
(CategoryTheory.Comma.opFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
def
CategoryTheory.Comma.opFunctorCompSnd
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opFunctor L R).leftOp.comp (CategoryTheory.Comma.snd R.op L.op) ≅ (CategoryTheory.Comma.fst L R).op
Composing the leftOp of opFunctor L R with snd L.op R.op is naturally isomorphic
to fst L R.
Equations
- CategoryTheory.Comma.opFunctorCompSnd L R = CategoryTheory.Iso.refl ((CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.snd R.op L.op))
Instances For
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompSnd_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : (CategoryTheory.Comma L R)ᵒᵖ)
:
(CategoryTheory.Comma.opFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
@[simp]
theorem
CategoryTheory.Comma.opFunctorCompSnd_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : (CategoryTheory.Comma L R)ᵒᵖ)
:
(CategoryTheory.Comma.opFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
def
CategoryTheory.Comma.unopFunctor
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{T : Type u₃}
[CategoryTheory.Category.{v₃, u₃} T]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
:
CategoryTheory.Functor (CategoryTheory.Comma L.op R.op) (CategoryTheory.Comma R L)ᵒᵖ
The canonical functor from Comma L.op R.op to (Comma R L)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Comma.unopFunctor_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.op R.op}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Comma.unopFunctor L R).map f = Opposite.op { left := f.right.unop, right := f.left.unop, w := ⋯ }
@[simp]
theorem
CategoryTheory.Comma.unopFunctor_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.op R.op)
:
(CategoryTheory.Comma.unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }
def
CategoryTheory.Comma.unopFunctorCompFst
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.unopFunctor L R).comp (CategoryTheory.Comma.fst R L).op ≅ CategoryTheory.Comma.snd L.op R.op
Composing unopFunctor L R with (fst L R).op is isomorphic to snd L.op R.op.
Equations
- CategoryTheory.Comma.unopFunctorCompFst L R = CategoryTheory.Iso.refl ((CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.fst R L).op)
Instances For
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompFst_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L.op R.op)
:
(CategoryTheory.Comma.unopFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id X.right
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompFst_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L.op R.op)
:
(CategoryTheory.Comma.unopFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id X.right
def
CategoryTheory.Comma.unopFunctorCompSnd
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.unopFunctor L R).comp (CategoryTheory.Comma.snd R L).op ≅ CategoryTheory.Comma.fst L.op R.op
Composing unopFunctor L R with (snd L R).op is isomorphic to fst L.op R.op.
Equations
- CategoryTheory.Comma.unopFunctorCompSnd L R = CategoryTheory.Iso.refl ((CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.snd R L).op)
Instances For
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompSnd_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L.op R.op)
:
(CategoryTheory.Comma.unopFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id X.left
@[simp]
theorem
CategoryTheory.Comma.unopFunctorCompSnd_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]
(L : CategoryTheory.Functor A T)
(R : CategoryTheory.Functor B T)
(X : CategoryTheory.Comma L.op R.op)
:
(CategoryTheory.Comma.unopFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id X.left
def
CategoryTheory.Comma.opEquiv
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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 L R ≌ (CategoryTheory.Comma R.op L.op)ᵒᵖ
The canonical equivalence between Comma L R and (Comma R.op L.op)ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Comma.opEquiv_inverse
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opEquiv L R).inverse = (CategoryTheory.Comma.unopFunctor R L).leftOp
@[simp]
theorem
CategoryTheory.Comma.opEquiv_unitIso
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opEquiv L R).unitIso = CategoryTheory.NatIso.ofComponents
(fun (X : CategoryTheory.Comma L R) =>
CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comma L R)).obj X))
⋯
@[simp]
theorem
CategoryTheory.Comma.opEquiv_counitIso
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opEquiv L R).counitIso = CategoryTheory.NatIso.ofComponents
(fun (X : (CategoryTheory.Comma R.op L.op)ᵒᵖ) =>
CategoryTheory.Iso.refl
(((CategoryTheory.Comma.unopFunctor R L).leftOp.comp (CategoryTheory.Comma.opFunctor L R)).obj X))
⋯
@[simp]
theorem
CategoryTheory.Comma.opEquiv_functor
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type 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.opEquiv L R).functor = CategoryTheory.Comma.opFunctor L R