open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Diagram.Limit.Base where

IdeaπŸ”—

The idea of limits generalises many concrete constructions in mathematics - from several settings, such as set theory, topology and algebra - to arbitrary categories. A limit, if it exists, is β€œthe best solution” to an β€œequational problem.” For a first intuition, we can build them graphically, working directly β€œon top” of a diagram.

ProductsπŸ”—

Note: Products are described explicitly in Cat.Diagram.Product. The description there might be easier to parse.

Consider a discrete diagram - one that has no interesting morphisms, only identities, such as the collection of objects below.

To consider a limit for this diagram, we first have to go through an intermediate step - a Cone. Draw a new object, the apex - let’s call it PP - and a family of maps from PP β€œdown onto” all of the objects of the diagram. The new maps have to make everything in sight commute, but in the case of a discrete diagram, we can pick any maps. There are no obligations.

It’ll be helpful to think of the maps as projections - which is why they’re labelled with the greek letter Ο€\pi, for projection. However, for an arbitrary cone, the maps are.. well, arbitrary. To consider a concrete example, we can pretend our diagram was in Set\id{Set} all along, and that AA was the set Q\bb{Q} and BB was the set R\bb{R}. Then the following is a cone over it:

Abstracting again, there is a canonical definition of cone homomorphism - A map between the apices that makes everything in sight commute. If Pβ€²P' and PP were both apices for our original discrete diagram, we would draw a cone homomorphism f:Pβ€²β†’Pf : P' \to P as the dashed arrow in following commutative Starfleet comms badge.

These assemble into a category, Cones, with composition and identity given by the composition and identity of ambient category. A Limit is, then, a terminal object in this category. For PP to be a limit in our diagram above, we require that, for any other cone Pβ€²P' there exists a unique arrow Pβ€²β†’PP' \to P that makes everything commute.

The limit over a discrete diagram is called a product, and it’s important to note that the diagram need not be finite. Here are concrete examples of products in categories:

  • In Sets\id{Sets}, the limit is the Cartesian product of the objects of the diagram, and the arrows are the projections onto the factors.

  • In Top\id{Top}, the limit is the product space of the objects, and the arrows are projections, considered as continuous maps. The product topology can be defined as the coarsest topology that makes the projections continuous.

  • In a partially ordered set, considered as a category, the limit is the greatest lower bound of the objects - In a poset, we consider that there exists a map aβ†’ba \to b whenever a≀ba \le b.

    Normalising the definition of limit slightly, it’s works out to be an object pp such that p≀ap \le a and p≀bp \le b, and if there are any other pβ€²p's satisfying that, then p′≀pp' \le p.

This last example also demonstrates that, while we can always describe the limit over a diagram, it does not necessarily exist. Consider the poset (Rβˆ–0,≀)(\bb{R} \setminus {0}, \le) of real numbers except zero, with the usual ordering. Then the product indexed by {x∈R:x>0}\{ x \in \bb{R} : x > 0 \} - which is normally 00 - does not exist. Not every category has every limit. Some categories have no limits at all! If a category has every limit, it’s called complete.

Terminal objectsπŸ”—

Note: Terminal objects are described explicitly in Cat.Diagram.Terminal. The description there might be easier to parse.

Perhaps a simpler example of a limit is the one over the empty diagram. Since the empty diagram is discrete, what we’ll end up with is a kind of product - an empty product. A cone over the empty diagram is an object - the family of maps, indexed over the objects of the diagram, is empty.

In this case, a cone homomorphism works out to be a regular ol’ morphism, so the terminal object in the cone category is a terminal object in the ambient category: an object ⊀\top such that, for every other AA, there’s a unique arrow Aβ†’βŠ€A \to \top.

ConstructionπŸ”—

Cones are always considered over a diagram. Diagram just means β€œfunctor,” but it’s a concept with an attitude: Whereas, in general, functors can be a lot more involved than the name β€œdiagram” would suggest, every functor can be considered a diagram! However, for the purpose of constructing limits, we generally work with functors out of β€œshapes,” tiny categories like βˆ™β†’βˆ™β†βˆ™\bullet \to \bullet \leftarrow \bullet.

module _ {J : Precategory o₁ h₁} {C : Precategory oβ‚‚ hβ‚‚} (F : Functor J C) where
  private
    import Cat.Reasoning J as J
    import Cat.Reasoning C as C
    module F = Functor F

  record Cone : Type (o₁ βŠ” oβ‚‚ βŠ” h₁ βŠ” hβ‚‚) where
    no-eta-equality

A Cone over FF is given by an object (the apex) together with a family of maps ψ β€” one for each object in the indexing category J β€” such that β€œeverything in sight commutes.”

    field
      apex     : C.Ob
      ψ        : (x : J.Ob) β†’ C.Hom apex (F.β‚€ x)

For every map f:xβ†’yf : x \to y in the indexing category, we require that the diagram below commutes. This encompasses β€œeverything” since the only non-trivial composites that can be formed with the data at hand are of the form F(f)∘ψxF(f) \circ \psi_x.

      commutes : βˆ€ {x y} (f : J.Hom x y) β†’ F.₁ f C.∘ ψ x ≑ ψ y

These non-trivial composites consist of following the left leg of the diagram below, followed by the bottom leg. For it to commute, that path has to be the same as following the right leg.

Since paths in Hom-spaces are propositions, to test equality of cones, it suffices for the apices to be equal, and for their ψ\psis to assign equal morphisms for every object in the shape category.

  Cone-path : {x y : Cone}
        β†’ (p : Cone.apex x ≑ Cone.apex y)
        β†’ (βˆ€ o β†’ PathP (Ξ» i β†’ C.Hom (p i) (F.β‚€ o)) (Cone.ψ x o) (Cone.ψ y o))
        β†’ x ≑ y
  Cone-path p q i .Cone.apex = p i
  Cone-path p q i .Cone.ψ o = q o i
  Cone-path {x = x} {y} p q i .Cone.commutes {x = a} {y = b} f =
    is-propβ†’pathp (Ξ» i β†’ C.Hom-set _ _ (F.₁ f C.∘ q a i) (q b i))
      (x .commutes f) (y .commutes f) i
    where open Cone

Cone mapsπŸ”—

  record Cone-hom (x y : Cone) : Type (o₁ βŠ” hβ‚‚) where
    no-eta-equality

A Cone homomorphism is – like the introduction says – a map hom in the ambient category between the apices, such that β€œeverything in sight commutes.” Specifically, for any choice of object oo in the index category, the composition of hom with the domain cone’s ψ (at that object) must be equal to the codomain’s ψ.

    field
      hom      : C.Hom (Cone.apex x) (Cone.apex y)
      commutes : βˆ€ o β†’ Cone.ψ y o C.∘ hom ≑ Cone.ψ x o

Since cone homomorphisms are morphisms in the underlying category with extra properties, we can lift the laws from the underlying category to the category of Cones. The definition of compose is the enlightening part, since we have to prove that two cone homomorphisms again preserve all the commutativities.

  Cones : Precategory _ _
  Cones = cat where
    open Precategory

    compose : {x y z : _} β†’ Cone-hom y z β†’ Cone-hom x y β†’ Cone-hom x z
    compose {x} {y} {z} F G = r where
      open Cone-hom
      r : Cone-hom x z
      r .hom = hom F C.∘ hom G
      r .commutes o =
        Cone.ψ z o C.∘ hom F C.∘ hom G β‰‘βŸ¨ C.pulll (commutes F o) βŸ©β‰‘
        Cone.ψ y o C.∘ hom G           β‰‘βŸ¨ commutes G o βŸ©β‰‘
        Cone.ψ x o                     ∎

    cat : Precategory _ _
    cat .Ob = Cone
    cat .Hom = Cone-hom
    cat .id = record { hom = C.id ; commutes = Ξ» _ β†’ C.idr _ }
    cat ._∘_ = compose
    cat .idr f = Cone-hom-path (C.idr _)
    cat .idl f = Cone-hom-path (C.idl _)
    cat .assoc f g h = Cone-hom-path (C.assoc _ _ _)

LimitsπŸ”—

At risk of repeating myself: A Limit is, then, a terminal object in this category.

  Limit : Type _
  Limit = Terminal Cones

  Limit-apex : Limit β†’ C.Ob
  Limit-apex x = Cone.apex (Terminal.top x)

  Limit-universal : (L : Limit) β†’ (K : Cone) β†’ C.Hom (Cone.apex K) (Limit-apex L)
  Limit-universal L K = Cone-hom.hom (Terminal.! L {K})

  is-limit : Cone β†’ Type _
  is-limit K = is-terminal Cones K

Preservation of limitsπŸ”—

Since a cone is, in particular, a commutative diagram, and every functor preserves commutativity of diagrams, a functor F:Cβ†’DF : \ca{C} \to \ca{D} acts on a cone over Dia\id{Dia} (in C\ca{C}), sending it to a cone over F∘DiaF \circ \id{Dia} (in D\ca{D}).

  F-map-cone : Cone Dia β†’ Cone (F F∘ Dia)
  Cone.apex (F-map-cone x) = Fβ‚€ F (Cone.apex x)
  Cone.ψ (F-map-cone x) x₁ = F₁ F (Cone.ψ x x₁)
  Cone.commutes (F-map-cone x) {y = y} f =
    F.₁ (F₁ Dia f) D.∘ F.₁ (Cone.ψ x _)  β‰‘βŸ¨ F.collapse (Cone.commutes x _) βŸ©β‰‘
    F.₁ (Cone.ψ x y)                     ∎

Note that this also lets us map morphisms between cones into D\ca{D}.

  F-map-cone-hom
    : {X Y : Cone Dia}
    β†’ Cone-hom Dia X Y
    β†’ Cone-hom (F F∘ Dia) (F-map-cone X) (F-map-cone Y)
  F-map-cone-hom {X = X} {Y = Y} f = cone-hom
    where
      module X = Cone X
      module Y = Cone Y
      module f = Cone-hom f

      cone-hom : Cone-hom (F F∘ Dia) (F-map-cone X) (F-map-cone Y)
      cone-hom .Cone-hom.hom = F .F₁ f.hom
      cone-hom .Cone-hom.commutes _ =
        F .F₁ (Y.ψ _) D.∘ (F .F₁ f.hom) β‰‘βŸ¨ F.collapse (f .Cone-hom.commutes _) βŸ©β‰‘
        F .F₁ (X.ψ _)                   ∎

Suppose you have a limit LL of Dia\id{Dia} β€” which is, to reiterate, a terminal object in the category of cones over Dia\id{Dia}. We say that FF preserves LL if F(L)F(L), as defined right above, is a terminal object in the category of cones over F∘DiaF \circ \id{Dia}.

  Preserves-limit : Cone Dia β†’ Type _
  Preserves-limit K = is-limit Dia K β†’ is-limit (F F∘ Dia) (F-map-cone K)

This definition is necessary because D\ca{D} will not, in general, possess an operation assigning a limit to every diagram β€” therefore, there might not be a β€œcanonical limit” of F∘DiaF\circ\id{Dia} we could compare F(L)F(L) to. However, since limits are described by a universal property (in particular, being terminal), we don’t need such an object! Any limit is as good as any other.

In more concise terms, we say a functor preserves limits if it takes limiting cones β€œupstairs” to limiting cones β€œdownstairs.”

Reflection of limitsπŸ”—

Using our analogy from before, we say a functor reflects limits if it takes limiting cones β€œdownstairs” to limiting cones β€œupstairs.”

More concretely, if we have some limiting cone in D\ca{D} of F∘DiaF \circ \id{Dia} with apex F(a)F(a), then aa was already the limit of Dia\id{Dia}!

  Reflects-limit : Cone Dia β†’ Type _
  Reflects-limit K = is-limit (F F∘ Dia) (F-map-cone K) β†’ is-limit Dia K

Creation of limitsπŸ”—

Finally, we say a functor creates limits of shape Dia\id{Dia} if it both preserves and reflects those limits. Intuitively, this means that the limits of shape Dia\id{Dia} in C\ca{C} are in a 1-1 correspondence with the limits F∘idDiaF \circ id{Dia} in D\ca{D}.

  record Creates-limit (K : Cone Dia) : Type (o₁ βŠ” h₁ βŠ” oβ‚‚ βŠ” hβ‚‚ βŠ” o₃ βŠ” h₃) where
    field
      preserves-limit : Preserves-limit K
      reflects-limit : Reflects-limit K

ContinuityπŸ”—

is-continuous
  : βˆ€ {oshape hshape}
      {C : Precategory o₁ h₁}
      {D : Precategory oβ‚‚ hβ‚‚}
  β†’ Functor C D β†’ Type _

A continuous functor is one that β€” for every shape of diagram J, and every diagram diagram of shape J in C β€” preserves the limit for that diagram.

is-continuous {oshape = oshape} {hshape} {C = C} F =
  βˆ€ {J : Precategory oshape hshape} {diagram : Functor J C}
  β†’ (K : Cone diagram) β†’ Preserves-limit F K

UniquenessπŸ”—

Above, there has been mention of the limit. The limit of a diagram, if it exists, is unique up to isomorphism. We prove that here. The argument is as follows: Fixing a diagram FF, suppose that XX and YY are both limiting cones for for FF.

  Limiting-cone-unique
    : (X Y : Limit F)
    β†’ Terminal.top X Cones.β‰… Terminal.top Y
  Limiting-cone-unique X Y = Cones.make-iso f g f∘g≑id g∘f≑id where
    X-cone = Terminal.top X
    Y-cone = Terminal.top Y

It follows from YY (resp. XX) being a terminal object that there is a unique cone homomorphism f:X→Yf : X \to Y (resp g:Y→Xg : Y \to X).

    f : Cones.Hom X-cone Y-cone
    f = Terminal.! Y {X-cone}

    g : Cones.Hom Y-cone X-cone
    g = Terminal.! X {Y-cone}

To show that gg is an inverse to ff, consider the composition g∘fg \circ f (the other case is symmetric): It is a map g∘f:Xβ†’Xg \circ f : X \to X. Since XX is a terminal object, we have that the space of cone homomorphisms Xβ†’XX \to X is contractible - and thus any two such maps are equal. Thus, g∘f=idX:Xβ†’Xg \circ f = \id{id}_{X} : X \to X.

    f∘g≑id : (f Cones.∘ g) ≑ Cones.id
    f∘g≑id = Terminal.!-uniqueβ‚‚ Y (f Cones.∘ g) Cones.id

    g∘f≑id : (g Cones.∘ f) ≑ Cones.id
    g∘f≑id = Terminal.!-uniqueβ‚‚ X (g Cones.∘ f) Cones.id

There is an evident functor from Cones to C, which sends cones to their apices and cone homomorphisms to their underlying maps. Being a functor, it preserves isomorphisms, so we get an isomorphism of the limit objects from the isomorphism of limit cones.

Contrary to the paragraph above, though, rather than defining a functor, there is a direct proof that an isomorphism of limits results in an isomorphism of apices. Fortunately, the direct proof Cone≅→apex≅ is exactly what one would get had they defined the functor and used the proof that it preserves isomorphisms.

  Cone≅→apex≅ : {X Y : Cone F}
              β†’ X Cones.β‰… Y
              β†’ (Cone.apex X) C.β‰… (Cone.apex Y)
  Cone≅→apex≅ c =
    C.make-iso (Cone-hom.hom c.to) (Cone-hom.hom c.from)
      (ap Cone-hom.hom c.invl)
      (ap Cone-hom.hom c.invr)
    where module c = Cones._β‰…_ c

  Cone-invertible→apex-invertible : {X Y : Cone F} {f : Cones.Hom X Y}
                                  β†’ Cones.is-invertible f
                                  β†’ C.is-invertible (Cone-hom.hom f)
  Cone-invertible→apex-invertible {f = f} f-invert =
    C.make-invertible (Cone-hom.hom inv) (ap Cone-hom.hom invl) (ap Cone-hom.hom invr)
    where open Cones.is-invertible f-invert

  Limit-unique
    : {X Y : Limit F}
    β†’ Cone.apex (Terminal.top X) C.β‰… Cone.apex (Terminal.top Y)
  Limit-unique {X} {Y} = Cone≅→apex≅ (Limiting-cone-unique X Y)

If the universal map K→LK \to L between apexes of some limit is invertible, then that means that KK is also a limiting cone.

  apex-iso→is-limit
    : (K : Cone F)
      (L : Limit F)
      β†’ C.is-invertible (Limit-universal F L K)
      β†’ is-limit F K
  apex-iso→is-limit K L invert K′ = limits
    where
      module K = Cone K
      module Kβ€² = Cone Kβ€²
      module L = Cone (Terminal.top L)
      module universal {K} = Cone-hom (Terminal.! L {K})
      open C.is-invertible invert

      limits : is-contr (Cones.Hom Kβ€² K)
      limits .centre .Cone-hom.hom = inv C.∘ Limit-universal F L Kβ€²
      limits .centre .Cone-hom.commutes _ =
        (K.ψ _) C.∘ (inv C.∘ universal.hom)                   β‰‘Λ˜βŸ¨ ap ( C._∘ (inv C.∘ universal.hom)) (universal.commutes _) βŸ©β‰‘Λ˜
        (L.ψ _ C.∘ universal.hom) C.∘ (inv C.∘ universal.hom) β‰‘βŸ¨ C.cancel-inner invl βŸ©β‰‘
        L.ψ _ C.∘ universal.hom                               β‰‘βŸ¨ universal.commutes _ βŸ©β‰‘
        Kβ€².ψ _                                                ∎
      limits .paths f = Cone-hom-path F $ C.invertible→monic invert _ _ $
        universal.hom C.∘ (inv C.∘ universal.hom) β‰‘βŸ¨ C.cancell invl βŸ©β‰‘
        universal.hom                             β‰‘βŸ¨ ap Cone-hom.hom (Terminal.!-unique L (Terminal.! L Cones.∘ f)) βŸ©β‰‘
        universal.hom C.∘ Cone-hom.hom f          ∎

CompletenessπŸ”—

A category is complete if admits for limits of arbitrary shape. However, in the presence of excluded middle, if a category admits products indexed by its class of morphisms, then it is automatically thin. Since excluded middle is independent of type theory, we can not prove that any non-thin categories have arbitrary limits.

Instead, categories are complete with respect to a pair of universes: A category is (o,β„“)(o, \ell)-complete if it has limits for any diagram indexed by a precategory with objects in TypeΒ o\ty\ o and morphisms in TypeΒ β„“\ty\ \ell.

is-complete : βˆ€ {oc β„“c} o β„“ β†’ Precategory oc β„“c β†’ Type _
is-complete o β„“ C = βˆ€ {D : Precategory o β„“} (F : Functor D C) β†’ Limit F