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 **p**rojection. 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