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 functorsL
andR
.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
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
Equations
- CategoryTheory.Comma.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id default } }
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
Equations
- CategoryTheory.CommaMorphism.inhabited = { default := { left := CategoryTheory.CategoryStruct.id default.left, right := CategoryTheory.CategoryStruct.id default.right, w := ⋯ } }
Equations
- CategoryTheory.commaCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
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
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
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
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
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
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
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The equality between map α β ⋙ fst L' R'
and fst L R ⋙ F₁
,
where α : F₁ ⋙ L' ⟶ L ⋙ 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
The equality between map α β ⋙ snd L' R'
and snd L R ⋙ F₂
,
where β : R ⋙ F ⟶ F₂ ⋙ R'
.
The isomorphism between map α β ⋙ snd L' R'
and snd L R ⋙ F₂
,
where β : R ⋙ F ⟶ F₂ ⋙ R'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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
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
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
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
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
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
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
The functor (F ⋙ L, R) ⥤ (L, R)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If F
is an equivalence, then so is preLeft F L R
.
Equations
- ⋯ = ⋯
The functor (F ⋙ L, R) ⥤ (L, R)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If F
is an equivalence, then so is preRight L F R
.
Equations
- ⋯ = ⋯
The functor (L, R) ⥤ (L ⋙ F, R ⋙ F)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
Taking the comma category of the identity Discrete PUnit ⥤ Discrete PUnit
and a functor B ⥤ Discrete PUnit
results in a category equivalent to B
.