Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

(Co)limits in functor categories. #

We show that if D has limits, then the functor category C ⥤ D also has limits (CategoryTheory.Limits.functorCategoryHasLimits), and the evaluation functors preserve limits (CategoryTheory.Limits.evaluationPreservesLimits) (and similarly for colimits).

We also show that F : D ⥤ K ⥤ C preserves (co)limits if it does so for each k : K (CategoryTheory.Limits.preservesLimitsOfEvaluation and CategoryTheory.Limits.preservesColimitsOfEvaluation).

The evaluation functors jointly reflect limits: that is, to show a cone is a limit of F it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is limiting you can show it's pointwise limiting.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Limits.combineCones_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) {k₁ : K} {k₂ : K} (f : k₁ k₂) :
    (CategoryTheory.Limits.combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone (F.flip.map f) }

    Given a functor F and a collection of limit cones for each diagram X ↦ F X k, we can stitch them together to give a cone for the diagram F. combinedIsLimit shows that the new cone is limiting, and evalCombined shows it is (essentially) made up of the original cones.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The stitched together cones each project down to the original given cones (up to iso).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Stitching together limiting cones gives a limiting cone.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of F it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is colimiting you can show it's pointwise colimiting.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Limits.combineCocones_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) {k₁ : K} {k₂ : K} (f : k₁ k₂) :
            (CategoryTheory.Limits.combineCocones F c).pt.map f = (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := CategoryTheory.CategoryStruct.comp (F.flip.map f) (c k₂).cocone }

            Given a functor F and a collection of colimit cocones for each diagram X ↦ F X k, we can stitch them together to give a cocone for the diagram F. combinedIsColimit shows that the new cocone is colimiting, and evalCombined shows it is (essentially) made up of the original cocones.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The stitched together cocones each project down to the original given cocones (up to iso).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Stitching together colimiting cocones gives a colimiting cocone.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  If F : J ⥤ K ⥤ C is a functor into a functor category which has a limit, then the evaluation of that limit at k is the limit of the evaluations of F.obj j at k.

                  Equations
                  Instances For

                    If F : J ⥤ K ⥤ C is a functor into a functor category which has a colimit, then the evaluation of that colimit at k is the colimit of the evaluations of F.obj j at k.

                    Equations
                    Instances For

                      F : D ⥤ K ⥤ C preserves the limit of some G : J ⥤ D if it does for each k : K.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        F : D ⥤ K ⥤ C preserves limits of shape J if it does for each k : K.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The constant functor C ⥤ (D ⥤ C) preserves limits.

                          Equations
                          • One or more equations did not get rendered due to their size.

                          F : D ⥤ K ⥤ C preserves the colimit of some G : J ⥤ D if it does for each k : K.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            F : D ⥤ K ⥤ C preserves all colimits of shape J if it does for each k : K.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The constant functor C ⥤ (D ⥤ C) preserves colimits.

                              Equations
                              • One or more equations did not get rendered due to their size.

                              A variant of limitIsoFlipCompLim where the arguments of F are flipped.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                For a functor G : J ⥤ K ⥤ C, its limit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ lim. Note that this does not require K to be small.

                                Equations
                                Instances For

                                  A variant of colimit_iso_flip_comp_colim where the arguments of F are flipped.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    For a functor G : J ⥤ K ⥤ C, its colimit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ colim. Note that this does not require K to be small.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For