module Cat.Instances.Functor.Limits where

Limits in functor categoriesπŸ”—

Let C\mathcal{C} be a category admitting D\mathcal{D}-shaped limits. Then the functor category [E,S][\mathcal{E},\mathcal{S}], for E\mathcal{E} any category, also admits D\mathcal{D}-shaped limits. In particular, if C\mathcal{C} is (ΞΉ,ΞΊ)(\iota,\kappa)-complete, then so is [E,C][\mathcal{E},\mathcal{C}].

module _
  {o₁ ℓ₁} {C : Precategory o₁ ℓ₁}
  {oβ‚‚ β„“β‚‚} {D : Precategory oβ‚‚ β„“β‚‚}
  {o₃ ℓ₃} {E : Precategory o₃ ℓ₃}
  (has-D-lims : βˆ€ (F : Functor D C) β†’ Limit F)
  (F : Functor D Cat[ E , C ])

Let F:Dβ†’[E,C]F : \mathcal{D} \to [\mathcal{E},\mathcal{C}] be a diagram, and suppose C\mathcal{C} admits limits of D\mathcal{D}-shaped diagrams; We wish to compute the limit lim⁑F\lim F. First, observe that we can Uncurry FF to obtain a functor Fβ€²:DΓ—Eβ†’CF' : \mathcal{D} \times \mathcal{E} \to \mathcal{C}; By fixing the value of the E\mathcal{E} coordinate (say, to xx), we obtain a family F(βˆ’,x)F(-, x) of D\mathcal{D}-shaped diagrams in C\mathcal{C}, which, by assumption, all have limits.

    F-uncurried : Functor (D Γ—αΆœ E) C
    F-uncurried = Uncurry {C = D} {D = E} {E = C} F

    import Cat.Functor.Bifunctor {C = D} {D = E} {E = C} F-uncurried as Fβ€²
    module D-lim x = Limit (has-D-lims (Fβ€².Left x))

Let us call the limit of F(βˆ’,x)F(-, x) β€” taken in C\mathcal{C} β€” lim-for, and similarly the unique, β€œterminating” cone homomorphism Kβ†’lim⁑F(βˆ’,x)K \to \lim F(-, x) will be called !-for.

    !-for : βˆ€ {x y} (f : E.Hom x y) β†’ C.Hom (D-lim.apex x) (D-lim.apex y)
    !-for {x} {y} f =
      D-lim.universal y
        (Ξ» j β†’ Fβ€².Right j .F₁ f C.∘ D-lim.ψ x j)
        (Ξ» g β†’
          C.extendl Fβ€².first∘second
          βˆ™ apβ‚‚ C._∘_ refl (D-lim.commutes x g))

    functor-apex : Functor E C
    functor-apex .Fβ‚€ x = D-lim.apex x
    functor-apex .F₁ {x} {y} f = !-for f
    functor-apex .F-id =
      sym $ D-lim.unique _ _ _ _ Ξ» j β†’
        C.idr _ βˆ™ sym (D-lim.commutes _ _)
    functor-apex .F-∘ f g =
      sym $ D-lim.unique _ _ _ _ Ξ» j β†’
        C.pulll (D-lim.factors _ _ _)
        βˆ™ C.pullr (D-lim.factors _ _ _)
        βˆ™ C.pulll (sym (Fβ€².Right _ .F-∘ _ _))

  functor-limit : Limit F
  functor-limit = to-limit $ to-is-limit ml
      open make-is-limit

      ml : make-is-limit F functor-apex
      ml .ψ j .η x = D-lim.ψ x j
      ml .ψ j .is-natural x y f =
        D-lim.factors _ _ _ βˆ™ apβ‚‚ C._∘_ (C.eliml (F.F-id Ξ·β‚š _)) refl
      ml .commutes f = Nat-path Ξ» j β†’
        C.pushr (C.introl (F.β‚€ _ .F-id)) βˆ™ D-lim.commutes j f
      ml .universal eta p .Ξ· x =
        D-lim.universal x
          (Ξ» j β†’ eta j .Ξ· x)
          (Ξ» f β†’ apβ‚‚ C._∘_ (C.elimr (F.β‚€ _ .F-id)) refl βˆ™ p f Ξ·β‚š x)
      ml .universal eta p .is-natural x y f =
        D-lim.uniqueβ‚‚ y _
          (Ξ» g β†’ C.pulll (apβ‚‚ C._∘_ (C.elimr (F.β‚€ _ .F-id)) refl βˆ™ p g Ξ·β‚š y))
          (Ξ» j β†’ C.pulll (D-lim.factors _ _ _))
          (Ξ» j β†’
            C.pulll (D-lim.factors _ _ _)
            βˆ™ C.pullr (D-lim.factors _ _ _)
            βˆ™ apβ‚‚ C._∘_ (C.eliml (F.F-id Ξ·β‚š _)) refl
            βˆ™ sym (eta j .is-natural x y f))
      ml .factors eta p = Nat-path Ξ» j β†’
        D-lim.factors j _ _
      ml .unique eta p other q = Nat-path Ξ» x β†’
        D-lim.unique _ _ _ _ Ξ» j β†’ q j Ξ·β‚š x

As a corollary, if D\mathcal{D} is an (o,β„“)(o,\ell)-complete category, then so is [C,D][\mathcal{C},\mathcal{D}].

Functor-cat-is-complete :
  βˆ€ {o β„“} {o₁ ℓ₁} {C : Precategory o₁ ℓ₁} {oβ‚‚ β„“β‚‚} {D : Precategory oβ‚‚ β„“β‚‚}
  β†’ is-complete o β„“ D β†’ is-complete o β„“ Cat[ C , D ]
Functor-cat-is-complete D-complete = functor-limit D-complete