# Documentation

Mathlib.CategoryTheory.Limits.Comma

# Limits and colimits in comma categories #

We build limits in the comma category Comma L R provided that the two source categories have limits and R preserves them. This is used to construct limits in the arrow category, structured arrow category and under category, and show that the appropriate forgetful functors create limits.

The duals of all the above are also given.

@[simp]
theorem CategoryTheory.Comma.limitAuxiliaryCone_π_app {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (X : J) :
.app X = CategoryTheory.CategoryStruct.comp (L.map (c₁.app X)) (F.obj X).hom
@[simp]
theorem CategoryTheory.Comma.limitAuxiliaryCone_pt {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :
().pt = L.obj c₁.pt
def CategoryTheory.Comma.limitAuxiliaryCone {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :

(Implementation). An auxiliary cone which is useful in order to construct limits in the comma category.

Instances For
@[simp]
theorem CategoryTheory.Comma.coneOfPreserves_π_app_left {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) (j : J) :
(().π.app j).left = c₁.app j
@[simp]
theorem CategoryTheory.Comma.coneOfPreserves_pt_hom {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) :
@[simp]
theorem CategoryTheory.Comma.coneOfPreserves_pt_left {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) :
().pt.left = c₁.pt
@[simp]
theorem CategoryTheory.Comma.coneOfPreserves_π_app_right {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) (j : J) :
(().π.app j).right = c₂.app j
@[simp]
theorem CategoryTheory.Comma.coneOfPreserves_pt_right {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) :
().pt.right = c₂.pt
def CategoryTheory.Comma.coneOfPreserves {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₂ : ) :

If R preserves the appropriate limit, then given a cone for F ⋙ fst L R : J ⥤ L and a limit cone for F ⋙ snd L R : J ⥤ R we can build a cone for F which will turn out to be a limit cone.

Instances For
def CategoryTheory.Comma.coneOfPreservesIsLimit {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) (t₂ : ) :

Provided that R preserves the appropriate limit, then the cone in coneOfPreserves is a limit.

Instances For
@[simp]
theorem CategoryTheory.Comma.colimitAuxiliaryCocone_pt {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :
= R.obj c₂.pt
@[simp]
theorem CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (X : J) :
.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.app X))
def CategoryTheory.Comma.colimitAuxiliaryCocone {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :

(Implementation). An auxiliary cocone which is useful in order to construct colimits in the comma category.

Instances For
@[simp]
theorem CategoryTheory.Comma.coconeOfPreserves_pt_left {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) :
().pt.left = c₁.pt
@[simp]
theorem CategoryTheory.Comma.coconeOfPreserves_ι_app_left {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) (j : J) :
(().ι.app j).left = c₁.app j
@[simp]
theorem CategoryTheory.Comma.coconeOfPreserves_pt_right {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) :
().pt.right = c₂.pt
@[simp]
theorem CategoryTheory.Comma.coconeOfPreserves_pt_hom {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) :
@[simp]
theorem CategoryTheory.Comma.coconeOfPreserves_ι_app_right {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) (j : J) :
(().ι.app j).right = c₂.app j
def CategoryTheory.Comma.coconeOfPreserves {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) :

If L preserves the appropriate colimit, then given a colimit cocone for F ⋙ fst L R : J ⥤ L and a cocone for F ⋙ snd L R : J ⥤ R we can build a cocone for F which will turn out to be a colimit cocone.

Instances For
def CategoryTheory.Comma.coconeOfPreservesIsColimit {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) (t₁ : ) (t₂ : ) :

Provided that L preserves the appropriate colimit, then the cocone in coconeOfPreserves is a colimit.

Instances For
instance CategoryTheory.Comma.hasLimit {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :
instance CategoryTheory.Comma.hasLimitsOfShape {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } :
instance CategoryTheory.Comma.hasLimitsOfSize {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } [] [] [] :
instance CategoryTheory.Comma.hasColimit {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } (F : ) :
instance CategoryTheory.Comma.hasColimitsOfShape {J : Type w} {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } :
instance CategoryTheory.Comma.hasColimitsOfSize {A : Type u₁} [] {B : Type u₂} [] {T : Type u₃} [] {L : } {R : } [] [] [] :
instance CategoryTheory.Arrow.hasLimit {J : Type w} {T : Type u₃} [] (F : ) [i₁ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.leftFunc)] [i₂ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.rightFunc)] :
instance CategoryTheory.Arrow.hasLimitsOfShape {J : Type w} {T : Type u₃} [] :
instance CategoryTheory.Arrow.hasColimit {J : Type w} {T : Type u₃} [] (F : ) [i₁ : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.leftFunc)] [i₂ : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.rightFunc)] :
instance CategoryTheory.StructuredArrow.hasLimit {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } (F : ) :
instance CategoryTheory.StructuredArrow.hasLimitsOfShape {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } :
instance CategoryTheory.StructuredArrow.hasLimitsOfSize {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } [] [] :
noncomputable instance CategoryTheory.StructuredArrow.createsLimit {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } (F : ) :
noncomputable instance CategoryTheory.StructuredArrow.createsLimitsOfShape {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } :
noncomputable instance CategoryTheory.StructuredArrow.createsLimitsOfSize {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } [] :
instance CategoryTheory.StructuredArrow.mono_right_of_mono {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } {Y : } {Z : } (f : Y Z) :
theorem CategoryTheory.StructuredArrow.mono_iff_mono_right {A : Type u₁} [] {T : Type u₃} [] {X : T} {G : } {Y : } {Z : } (f : Y Z) :
instance CategoryTheory.CostructuredArrow.hasColimit {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} (F : ) :
instance CategoryTheory.CostructuredArrow.hasColimitsOfShape {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} :
instance CategoryTheory.CostructuredArrow.hasColimitsOfSize {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} [] [] :
noncomputable instance CategoryTheory.CostructuredArrow.createsColimit {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} (F : ) :
noncomputable instance CategoryTheory.CostructuredArrow.createsColimitsOfShape {J : Type w} {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} :
noncomputable instance CategoryTheory.CostructuredArrow.createsColimitsOfSize {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} [] :
instance CategoryTheory.CostructuredArrow.epi_left_of_epi {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} {Y : } {Z : } (f : Y Z) :
theorem CategoryTheory.CostructuredArrow.epi_iff_epi_left {A : Type u₁} [] {T : Type u₃} [] {G : } {X : T} {Y : } {Z : } (f : Y Z) :