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] :
A TB TType (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.

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) :
x.left = y.leftx.right = y.rightx = 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} :
category_theory.comma L Rcategory_theory.comma L RType (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.

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

@[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.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) :
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₂)category_theory.comma L₂ R category_theory.comma L₁ R

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₂)category_theory.comma L R₁ category_theory.comma L 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₁) :