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.

source
@[simp]
theorem CategoryTheory.Comma.limitAuxiliaryCone_π_app {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) (X : J) :
(CategoryTheory.Comma.limitAuxiliaryCone F c₁).π.app X = CategoryTheory.CategoryStruct.comp (L.map (c₁.π.app X)) (F.obj X).hom
source
@[simp]
theorem CategoryTheory.Comma.limitAuxiliaryCone_pt {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) :
(CategoryTheory.Comma.limitAuxiliaryCone F c₁).pt = L.obj c₁.pt
source
def CategoryTheory.Comma.limitAuxiliaryCone {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) :
CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R)

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

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Comma.coneOfPreserves_π_app_left {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) :
    ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).left = c₁.π.app j
    source
    @[simp]
    theorem CategoryTheory.Comma.coneOfPreserves_pt_hom {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) :
    (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.hom = (CategoryTheory.Limits.isLimitOfPreserves R t₂).lift (CategoryTheory.Comma.limitAuxiliaryCone F c₁)
    source
    @[simp]
    theorem CategoryTheory.Comma.coneOfPreserves_pt_left {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) :
    (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.left = c₁.pt
    source
    @[simp]
    theorem CategoryTheory.Comma.coneOfPreserves_π_app_right {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) :
    ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).right = c₂.π.app j
    source
    @[simp]
    theorem CategoryTheory.Comma.coneOfPreserves_pt_right {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) :
    (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.right = c₂.pt
    source
    def CategoryTheory.Comma.coneOfPreserves {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) :
    CategoryTheory.Limits.Cone F

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Comma.coneOfPreservesIsLimit {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] {c₁ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) :
      CategoryTheory.Limits.IsLimit (CategoryTheory.Comma.coneOfPreserves F c₁ t₂)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Comma.colimitAuxiliaryCocone_pt {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
        (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).pt = R.obj c₂.pt
        source
        @[simp]
        theorem CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) (X : J) :
        (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
        source
        def CategoryTheory.Comma.colimitAuxiliaryCocone {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
        CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L)

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

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Comma.coconeOfPreserves_pt_left {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
          (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.left = c₁.pt
          source
          @[simp]
          theorem CategoryTheory.Comma.coconeOfPreserves_ι_app_left {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) (j : J) :
          ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
          source
          @[simp]
          theorem CategoryTheory.Comma.coconeOfPreserves_pt_right {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
          (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.right = c₂.pt
          source
          @[simp]
          theorem CategoryTheory.Comma.coconeOfPreserves_pt_hom {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
          (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
          source
          @[simp]
          theorem CategoryTheory.Comma.coconeOfPreserves_ι_app_right {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) (j : J) :
          ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
          source
          def CategoryTheory.Comma.coconeOfPreserves {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))) :
          CategoryTheory.Limits.Cocone F

          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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CategoryTheory.Comma.coconeOfPreservesIsColimit {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsColimit c₂) :
            CategoryTheory.Limits.IsColimit (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂)

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance CategoryTheory.Comma.hasLimit {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R)) R] :
              CategoryTheory.Limits.HasLimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Comma.hasLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {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.Limits.HasLimitsOfShape J A] [CategoryTheory.Limits.HasLimitsOfShape J B] [CategoryTheory.Limits.PreservesLimitsOfShape J R] :
              CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Comma L R)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Comma.hasLimitsOfSize {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.Limits.HasLimitsOfSize.{w, w', v₁, u₁} A] [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} B] [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} R] :
              CategoryTheory.Limits.HasLimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Comma.hasColimit {J : Type w} [CategoryTheory.Category.{w', w} J] {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} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.Comma.fst L R)) L] :
              CategoryTheory.Limits.HasColimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Comma.hasColimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {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.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B] [CategoryTheory.Limits.PreservesColimitsOfShape J L] :
              CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Comma L R)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Comma.hasColimitsOfSize {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.Limits.HasColimitsOfSize.{w, w', v₁, u₁} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} B] [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} L] :
              CategoryTheory.Limits.HasColimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasLimit {J : Type w} [CategoryTheory.Category.{w', w} J] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (F : CategoryTheory.Functor J (CategoryTheory.Arrow T)) [i₁ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.leftFunc)] [i₂ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.rightFunc)] :
              CategoryTheory.Limits.HasLimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasLimitsOfShape J T] :
              CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Arrow T)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasLimits {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasLimits T] :
              CategoryTheory.Limits.HasLimits (CategoryTheory.Arrow T)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasColimit {J : Type w} [CategoryTheory.Category.{w', w} J] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (F : CategoryTheory.Functor J (CategoryTheory.Arrow T)) [i₁ : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.leftFunc)] [i₂ : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Arrow.rightFunc)] :
              CategoryTheory.Limits.HasColimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasColimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasColimitsOfShape J T] :
              CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Arrow T)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Arrow.hasColimits {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasColimits T] :
              CategoryTheory.Limits.HasColimits (CategoryTheory.Arrow T)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.StructuredArrow.hasLimit {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)) [i₁ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.StructuredArrow.proj X G))] [i₂ : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.StructuredArrow.proj X G)) G] :
              CategoryTheory.Limits.HasLimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.StructuredArrow.hasLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.Limits.PreservesLimitsOfShape J G] :
              CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.StructuredArrow X G)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.StructuredArrow.hasLimitsOfSize {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} A] [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] :
              CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₃} (CategoryTheory.StructuredArrow X G)
              Equations
              • ⋯ = ⋯
              source
              noncomputable instance CategoryTheory.StructuredArrow.createsLimit {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)) [i : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp F (CategoryTheory.StructuredArrow.proj X G)) G] :
              CategoryTheory.CreatesLimit F (CategoryTheory.StructuredArrow.proj X G)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              noncomputable instance CategoryTheory.StructuredArrow.createsLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.PreservesLimitsOfShape J G] :
              CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.StructuredArrow.proj X G)
              Equations
              source
              noncomputable instance CategoryTheory.StructuredArrow.createsLimitsOfSize {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] :
              CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₁, max u₁ v₃, u₁} (CategoryTheory.StructuredArrow.proj X G)
              Equations
              source
              instance CategoryTheory.StructuredArrow.mono_right_of_mono {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasPullbacks A] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] {Y : CategoryTheory.StructuredArrow X G} {Z : CategoryTheory.StructuredArrow X G} (f : Y ⟶ Z) [CategoryTheory.Mono f] :
              CategoryTheory.Mono f.right
              Equations
              • ⋯ = ⋯
              source
              theorem CategoryTheory.StructuredArrow.mono_iff_mono_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasPullbacks A] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] {Y : CategoryTheory.StructuredArrow X G} {Z : CategoryTheory.StructuredArrow X G} (f : Y ⟶ Z) :
              CategoryTheory.Mono f ↔ CategoryTheory.Mono f.right
              source
              instance CategoryTheory.CostructuredArrow.hasColimit {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow G X)) [i₁ : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.CostructuredArrow.proj G X))] [i₂ : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.CostructuredArrow.proj G X)) G] :
              CategoryTheory.Limits.HasColimit F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.CostructuredArrow.hasColimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.PreservesColimitsOfShape J G] :
              CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CostructuredArrow G X)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.CostructuredArrow.hasColimitsOfSize {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} A] [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] :
              CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, max u₁ v₃} (CategoryTheory.CostructuredArrow G X)
              Equations
              • ⋯ = ⋯
              source
              noncomputable instance CategoryTheory.CostructuredArrow.createsColimit {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow G X)) [i : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp F (CategoryTheory.CostructuredArrow.proj G X)) G] :
              CategoryTheory.CreatesColimit F (CategoryTheory.CostructuredArrow.proj G X)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              noncomputable instance CategoryTheory.CostructuredArrow.createsColimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.PreservesColimitsOfShape J G] :
              CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.CostructuredArrow.proj G X)
              Equations
              source
              noncomputable instance CategoryTheory.CostructuredArrow.createsColimitsOfSize {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] :
              CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₁, max u₁ v₃, u₁} (CategoryTheory.CostructuredArrow.proj G X)
              Equations
              source
              instance CategoryTheory.CostructuredArrow.epi_left_of_epi {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasPushouts A] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] {Y : CategoryTheory.CostructuredArrow G X} {Z : CategoryTheory.CostructuredArrow G X} (f : Y ⟶ Z) [CategoryTheory.Epi f] :
              CategoryTheory.Epi f.left
              Equations
              • ⋯ = ⋯
              source
              theorem CategoryTheory.CostructuredArrow.epi_iff_epi_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasPushouts A] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] {Y : CategoryTheory.CostructuredArrow G X} {Z : CategoryTheory.CostructuredArrow G X} (f : Y ⟶ Z) :
              CategoryTheory.Epi f ↔ CategoryTheory.Epi f.left