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 $P$ - and a family of maps from $P$ “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 $\id{Set}$ all along, and that $A$ was the set $\bb{Q}$ and $B$ was the set $\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'$ and $P$ were both apices for our original discrete diagram, we would draw a cone homomorphism $f : 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 $P$ to be a limit in our diagram above, we require that, for any other cone $P'$ there exists a unique arrow $P' \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 $\id{Sets}$, the limit is the Cartesian product of the objects of the diagram, and the arrows are the projections onto the factors.

• In $\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 \to b$ whenever $a \le b$.

  Normalising the definition of limit slightly, it’s works out to be an object $p$ such that $p \le a$ and $p \le b$, and if there are any other $p'$s satisfying that, then $p' \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 $(\bb{R} \setminus {0}, \le)$ of real numbers except zero, with the usual ordering. Then the product indexed by $\{ x \in \bb{R} : x > 0 \}$ - which is normally $0$ - 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 $A$, there’s a unique arrow $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 $F$ 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 \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) \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 $\psi$s 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 $o$ 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 : \ca{C} \to \ca{D}$ acts on a cone over $\id{Dia}$ (in $\ca{C}$), sending it to a cone over $F \circ \id{Dia}$ (in $\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 $\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 $L$ of $\id{Dia}$ — which is, to reiterate, a terminal object in the category of cones over $\id{Dia}$. We say that $F$ preserves $L$ if $F(L)$, as defined right above, is a terminal object in the category of cones over $F \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 $\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\circ\id{Dia}$ we could compare $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 $\ca{D}$ of $F \circ \id{Dia}$ with apex $F(a)$, then $a$ was already the limit of $\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 $\id{Dia}$ if it both preserves and reflects those limits. Intuitively, this means that the limits of shape $\id{Dia}$ in $\ca{C}$ are in a 1-1 correspondence with the limits $F \circ id{Dia}$ in $\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 $F$, suppose that $X$ and $Y$ are both limiting cones for for $F$.

  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 $Y$ (resp. $X$) being a terminal object that there is a unique cone homomorphism $f : X \to Y$ (resp $g : 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 $g$ is an inverse to $f$, consider the composition $g \circ f$ (the other case is symmetric): It is a map $g \circ f : X \to X$. Since $X$ is a terminal object, we have that the space of cone homomorphisms $X \to X$ is contractible - and thus any two such maps are equal. Thus, $g \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 \to L$ between apexes of some limit is invertible, then that means that $K$ 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, \ell)$-complete if it has limits for any diagram indexed by a precategory with objects in $\ty\ o$ and morphisms in $\ty\ \ell$.

is-complete : ∀ {oc ℓc} o ℓ → Precategory oc ℓc → Type _
is-complete o ℓ C = ∀ {D : Precategory o ℓ} (F : Functor D C) → Limit F