Documentation

Mathlib.CategoryTheory.Inserter.Limits

(Co)limits of inserters #

Let F G : C ⥤ D be a parallel pair of functors. In this file, we show that if F (resp. G) preserves colimits (resp. limits) of shape J and if C has colimits (resp. limits) of shape J, then Inserter F G has colimits (resp. limits) of shape J and the projection preserves them.

source
@[implicit_reducible]
noncomputable def CategoryTheory.Inserter.coconeOfPreserves {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) :
Limits.Cocone K

Assuming F preserves the colimit of K ⋙ proj F G where K is a diagram valued in the inserter category Inserter F _, a colimit cocone under K ⋙ proj F _ can be lifted to a cocone under K.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Inserter.coconeOfPreserves_ι_app_hom {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) (j : J) :
    ((coconeOfPreserves hc).ι.app j).hom = c.ι.app j
    source
    @[simp]
    theorem CategoryTheory.Inserter.coconeOfPreserves_pt_obj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) :
    (coconeOfPreserves hc).pt.obj = c.pt
    source
    @[simp]
    theorem CategoryTheory.Inserter.map_ι_coconeOfPreserves_pt_hom {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) (j : J) :
    CategoryStruct.comp (F.map (c.ι.app j)) (coconeOfPreserves hc).pt.hom = CategoryStruct.comp (K.obj j).hom (G.map (c.ι.app j))
    source
    @[simp]
    theorem CategoryTheory.Inserter.map_ι_coconeOfPreserves_pt_hom_assoc {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) (j : J) {Z : D} (h : G.obj (coconeOfPreserves hc).pt.obj ⟶ Z) :
    CategoryStruct.comp (F.map (c.ι.app j)) (CategoryStruct.comp (coconeOfPreserves hc).pt.hom h) = CategoryStruct.comp (K.obj j).hom (CategoryStruct.comp (G.map (c.ι.app j)) h)
    source
    noncomputable def CategoryTheory.Inserter.isColimitCoconeOfPreserves {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesColimit (K.comp (proj F G)) F] {c : Limits.Cocone (K.comp (proj F G))} (hc : Limits.IsColimit c) :
    Limits.IsColimit (coconeOfPreserves hc)

    Assuming F preserves the colimit of K ⋙ proj F G where K is a diagram valued in the inserter category Inserter F _, coconeOfPreserves is a colimit cocone.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CategoryTheory.Inserter.hasColimit {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} (K : Functor J (Inserter F G)) [Limits.HasColimit (K.comp (proj F G))] [Limits.PreservesColimit (K.comp (proj F G)) F] :
      Limits.HasColimit K
      source
      instance CategoryTheory.Inserter.hasColimitsOfShape {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasColimitsOfShape J C] [Limits.PreservesColimitsOfShape J F] :
      Limits.HasColimitsOfShape J (Inserter F G)
      source
      instance CategoryTheory.Inserter.preservesColimitsOfShape_proj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasColimitsOfShape J C] [Limits.PreservesColimitsOfShape J F] :
      Limits.PreservesColimitsOfShape J (proj F G)
      source
      instance CategoryTheory.Inserter.reflectsColimitsOfShape_proj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasColimitsOfShape J C] [Limits.PreservesColimitsOfShape J F] :
      Limits.ReflectsColimitsOfShape J (proj F G)
      source
      @[implicit_reducible]
      noncomputable def CategoryTheory.Inserter.coneOfPreserves {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) :
      Limits.Cone K

      Assuming G preserves the limit of K ⋙ proj F G where K is a diagram valued in the inserter category Inserter _ G, a limit cone over K ⋙ proj _ G can be lifted to a cone under K.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Inserter.coneOfPreserves_π_app_hom {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) (j : J) :
        ((coneOfPreserves hc).π.app j).hom = c.π.app j
        source
        @[simp]
        theorem CategoryTheory.Inserter.coneOfPreserves_pt_obj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) :
        (coneOfPreserves hc).pt.obj = c.pt
        source
        @[simp]
        theorem CategoryTheory.Inserter.coneOfPreserves_pt_hom_map_π_app {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) (j : J) :
        CategoryStruct.comp (coneOfPreserves hc).pt.hom (G.map (c.π.app j)) = CategoryStruct.comp (F.map (c.π.app j)) (K.obj j).hom
        source
        @[simp]
        theorem CategoryTheory.Inserter.coneOfPreserves_pt_hom_map_π_app_assoc {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) (j : J) {Z : D} (h : G.obj ((proj F G).obj (K.obj j)) ⟶ Z) :
        CategoryStruct.comp (coneOfPreserves hc).pt.hom (CategoryStruct.comp (G.map (c.π.app j)) h) = CategoryStruct.comp (F.map (c.π.app j)) (CategoryStruct.comp (K.obj j).hom h)
        source
        @[implicit_reducible]
        noncomputable def CategoryTheory.Inserter.isLimitConeOfPreserves {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} {K : Functor J (Inserter F G)} [Limits.PreservesLimit (K.comp (proj F G)) G] {c : Limits.Cone (K.comp (proj F G))} (hc : Limits.IsLimit c) :
        Limits.IsLimit (coneOfPreserves hc)

        Assuming G preserves the limit of K ⋙ proj F G where K is a diagram valued in the inserter category Inserter _ G, coneOfPreserves is a limit cone.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance CategoryTheory.Inserter.hasLimit {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} (K : Functor J (Inserter F G)) [Limits.HasLimit (K.comp (proj F G))] [Limits.PreservesLimit (K.comp (proj F G)) G] :
          Limits.HasLimit K
          source
          instance CategoryTheory.Inserter.hasLimitsOfShape {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasLimitsOfShape J C] [Limits.PreservesLimitsOfShape J G] :
          Limits.HasLimitsOfShape J (Inserter F G)
          source
          instance CategoryTheory.Inserter.preservesLimitsOfShape_proj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasLimitsOfShape J C] [Limits.PreservesLimitsOfShape J G] :
          Limits.PreservesLimitsOfShape J (proj F G)
          source
          instance CategoryTheory.Inserter.reflectsLimitsOfShape_proj {C : Type u_1} {D : Type u_2} {J : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} J] {F G : Functor C D} [Limits.HasLimitsOfShape J C] [Limits.PreservesLimitsOfShape J G] :
          Limits.ReflectsLimitsOfShape J (proj F G)