mathlib documentation

category_theory.comma

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 #

References #

Tags #

comma, slice, coslice, over, under, arrow

structure category_theory.comma {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : 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.

Instances for category_theory.comma
theorem category_theory.comma_morphism.ext {A : Type u₁} {_inst_1 : category_theory.category A} {B : Type u₂} {_inst_2 : category_theory.category B} {T : Type u₃} {_inst_3 : category_theory.category T} {L : A T} {R : B T} {X Y : category_theory.comma L R} (x y : category_theory.comma_morphism X Y) (h : x.left = y.left) (h_1 : x.right = y.right) :
x = y
@[ext]
structure category_theory.comma_morphism {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} (X Y : category_theory.comma L R) :
Type (max v₁ v₂)

A morphism between two objects in the comma category is a commutative square connecting the morphisms coming from the two objects using morphisms in the image of the functors L and R.

Instances for category_theory.comma_morphism
theorem category_theory.comma_morphism.ext_iff {A : Type u₁} {_inst_1 : category_theory.category A} {B : Type u₂} {_inst_2 : category_theory.category B} {T : Type u₃} {_inst_3 : category_theory.category T} {L : A T} {R : B T} {X Y : category_theory.comma L R} (x y : category_theory.comma_morphism X Y) :
x = y x.left = y.left x.right = y.right
@[simp]
theorem category_theory.comma_morphism.w {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X Y : category_theory.comma L R} (self : category_theory.comma_morphism X Y) :
L.map self.left Y.hom = X.hom R.map self.right
@[simp]
theorem category_theory.comma_morphism.w_assoc {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X Y : category_theory.comma L R} (self : category_theory.comma_morphism X Y) {X' : T} (f' : R.obj Y.right X') :
L.map self.left Y.hom f' = X.hom R.map self.right f'
@[protected, instance]
def category_theory.comma_category {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} :
Equations
@[simp]
theorem category_theory.comma.id_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X : category_theory.comma L R} :
@[simp]
theorem category_theory.comma.id_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X : category_theory.comma L R} :
@[simp]
theorem category_theory.comma.comp_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X Y Z : category_theory.comma L R} {f : X Y} {g : Y Z} :
(f g).left = f.left g.left
@[simp]
theorem category_theory.comma.comp_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L : A T} {R : B T} {X Y Z : category_theory.comma L R} {f : X Y} {g : Y Z} :
(f g).right = f.right g.right
def category_theory.comma.fst {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) :

The functor sending an object X in the comma category to X.left.

Equations
@[simp]
theorem category_theory.comma.fst_map {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (_x _x_1 : category_theory.comma L R) (f : _x _x_1) :
@[simp]
theorem category_theory.comma.fst_obj {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (X : category_theory.comma L R) :
def category_theory.comma.snd {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) :

The functor sending an object X in the comma category to X.right.

Equations
@[simp]
theorem category_theory.comma.snd_obj {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (X : category_theory.comma L R) :
@[simp]
theorem category_theory.comma.snd_map {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (_x _x_1 : category_theory.comma L R) (f : _x _x_1) :
@[simp]
theorem category_theory.comma.nat_trans_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (X : category_theory.comma L 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
@[simp]
theorem category_theory.comma.eq_to_hom_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (X Y : category_theory.comma L R) (H : X = Y) :
@[simp]
theorem category_theory.comma.eq_to_hom_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) (R : B T) (X Y : category_theory.comma L R) (H : X = Y) :
@[simp]
theorem category_theory.comma.iso_mk_inv_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L₁ : A T} {R₁ : B T} {X Y : category_theory.comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
@[simp]
theorem category_theory.comma.iso_mk_hom_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L₁ : A T} {R₁ : B T} {X Y : category_theory.comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
def category_theory.comma.iso_mk {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L₁ : A T} {R₁ : B T} {X Y : category_theory.comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
X Y

Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.

Equations
@[simp]
theorem category_theory.comma.iso_mk_hom_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L₁ : A T} {R₁ : B T} {X Y : category_theory.comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
@[simp]
theorem category_theory.comma.iso_mk_inv_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {L₁ : A T} {R₁ : B T} {X Y : category_theory.comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : L₁.map l.hom Y.hom = X.hom R₁.map r.hom) :
@[simp]
theorem category_theory.comma.map_left_obj_hom {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : category_theory.comma L₂ R) :
@[simp]
theorem category_theory.comma.map_left_obj_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : category_theory.comma L₂ R) :
@[simp]
theorem category_theory.comma.map_left_map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X Y : category_theory.comma L₂ R) (f : X Y) :
@[simp]
theorem category_theory.comma.map_left_obj_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X : category_theory.comma L₂ R) :
@[simp]
theorem category_theory.comma.map_left_map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) (X Y : category_theory.comma L₂ R) (f : X Y) :
def category_theory.comma.map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ : A T} (l : L₁ L₂) :

A natural transformation L₁ ⟶ L₂ induces a functor comma L₂ R ⥤ comma L₁ R.

Equations

The functor comma L R ⥤ comma L R induced by the identity natural transformation on L is naturally isomorphic to the identity functor.

Equations
@[simp]
theorem category_theory.comma.map_left_comp_inv_app_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : category_theory.comma L₃ R) :
@[simp]
theorem category_theory.comma.map_left_comp_hom_app_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : category_theory.comma L₃ R) :
def category_theory.comma.map_left_comp {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) :

The functor comma L₁ R ⥤ comma L₃ R induced by the composition of two natural transformations l : L₁ ⟶ L₂ and l' : L₂ ⟶ L₃ is naturally isomorphic to the composition of the two functors induced by these natural transformations.

Equations
@[simp]
theorem category_theory.comma.map_left_comp_hom_app_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : category_theory.comma L₃ R) :
@[simp]
theorem category_theory.comma.map_left_comp_inv_app_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (R : B T) {L₁ L₂ L₃ : A T} (l : L₁ L₂) (l' : L₂ L₃) (X : category_theory.comma L₃ R) :
@[simp]
theorem category_theory.comma.map_right_map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X Y : category_theory.comma L R₁) (f : X Y) :
@[simp]
theorem category_theory.comma.map_right_obj_hom {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : category_theory.comma L R₁) :
def category_theory.comma.map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) :

A natural transformation R₁ ⟶ R₂ induces a functor comma L R₁ ⥤ comma L R₂.

Equations
@[simp]
theorem category_theory.comma.map_right_obj_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : category_theory.comma L R₁) :
@[simp]
theorem category_theory.comma.map_right_obj_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X : category_theory.comma L R₁) :
@[simp]
theorem category_theory.comma.map_right_map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ : B T} (r : R₁ R₂) (X Y : category_theory.comma L R₁) (f : X Y) :

The functor comma L R ⥤ comma L R induced by the identity natural transformation on R is naturally isomorphic to the identity functor.

Equations
@[simp]
theorem category_theory.comma.map_right_comp_hom_app_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : category_theory.comma L R₁) :
@[simp]
theorem category_theory.comma.map_right_comp_inv_app_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : category_theory.comma L R₁) :
@[simp]
theorem category_theory.comma.map_right_comp_inv_app_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : category_theory.comma L R₁) :
def category_theory.comma.map_right_comp {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) :

The functor comma L R₁ ⥤ comma L R₃ induced by the composition of the natural transformations r : R₁ ⟶ R₂ and r' : R₂ ⟶ R₃ is naturally isomorphic to the composition of the functors induced by these natural transformations.

Equations
@[simp]
theorem category_theory.comma.map_right_comp_hom_app_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] (L : A T) {R₁ R₂ R₃ : B T} (r : R₁ R₂) (r' : R₂ R₃) (X : category_theory.comma L R₁) :
@[simp]
theorem category_theory.comma.pre_left_obj_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
@[simp]
theorem category_theory.comma.pre_left_obj_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
def category_theory.comma.pre_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) :

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

Equations
@[simp]
theorem category_theory.comma.pre_left_map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) (X Y : category_theory.comma (F L) R) (f : X Y) :
@[simp]
theorem category_theory.comma.pre_left_map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) (X Y : category_theory.comma (F L) R) (f : X Y) :
@[simp]
theorem category_theory.comma.pre_left_obj_hom {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (F : C A) (L : A T) (R : B T) (X : category_theory.comma (F L) R) :
@[simp]
theorem category_theory.comma.pre_right_obj_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) (X : category_theory.comma L (F R)) :
@[simp]
theorem category_theory.comma.pre_right_obj_hom {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) (X : category_theory.comma L (F R)) :
@[simp]
theorem category_theory.comma.pre_right_map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) (X Y : category_theory.comma L (F R)) (f : X Y) :
@[simp]
theorem category_theory.comma.pre_right_obj_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) (X : category_theory.comma L (F R)) :
def category_theory.comma.pre_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) :

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

Equations
@[simp]
theorem category_theory.comma.pre_right_map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (F : C B) (R : B T) (X Y : category_theory.comma L (F R)) (f : X Y) :
@[simp]
theorem category_theory.comma.post_obj_hom {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) (X : category_theory.comma L R) :
@[simp]
theorem category_theory.comma.post_obj_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) (X : category_theory.comma L R) :
def category_theory.comma.post {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) :

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

Equations
@[simp]
theorem category_theory.comma.post_obj_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) (X : category_theory.comma L R) :
@[simp]
theorem category_theory.comma.post_map_right {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) (X Y : category_theory.comma L R) (f : X Y) :
@[simp]
theorem category_theory.comma.post_map_left {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {T : Type u₃} [category_theory.category T] {C : Type u₄} [category_theory.category C] (L : A T) (R : B T) (F : T C) (X Y : category_theory.comma L R) (f : X Y) :