module Cat.Diagram.Limit.Base where
Limitsπ
This page describes the general definition of limits, and assumes some familiarity with some concrete examples, in particular terminal objects, products, equalisers, and pullbacks. It might be a good idea to check out those pages before continuing!
Ideaπ
To motivate limits, note how all the above examples have roughly the same structure. They all consist of some object, a bunch of maps out of said object, some commutativity conditions, and a universal property that states that we can construct unique maps into the object under certain conditions.
Our first step towards making this vague intuition precise is to construct a mathematical widget that picks out a collection of objects, arrows, and commutativity conditions in a category. This is required to describe the collection of maps out of our special objects, and the equations they satisfy. Luckily, we already have such a widget: functors!
To see how this works, letβs take a very simple example: a functor out of the single object category with one morphism into some category If we look at the image of such a functor, we can see that it picks out a single object; the single morphism must be taken to the identity morphism due to functoriality. We can scale this example up to functors from discrete category with elements; if we look at the image of such a functor, we shall see that it selects out objects of
We can perform the same trick with non-discrete categories; for instance, a functor out of the parallel arrows category selects a pair of parallel arrows in a functor out of the isomorphism category selects an isomorphism in and so on. We call such functors diagrams to suggest that we should think of them as picking out some shape in
We can use this newfound insight to describe the shape that each of our examples is defined over. Products are defined over a diagram that consists of a pair of objects; these diagrams correspond to functors out of the category with 2 objects and only identity morphisms. Equalisers are defined over a diagram that consists of a pair of parallel morphisms; such diagrams are given by functors out of the aforementioned parallel arrows category. Pullbacks defined over a diagram of the shape, again, these diagrams are given by functors out of the category with that exact shape. Terminal objects may seem to break this trend, but we can think of them as being defined over the empty diagram, the unique functor from the category with no objects.
We now move our attention to the maps out of our special object into the objects of the diagram. Note that these maps need to commute with any morphisms in the diagram, as is the case with pullbacks and equalisers. This is where our definition diverges from many other introductory sources. The typical approach is to define a bespoke widget called a cone that encodes the required morphisms and commuting conditions, and then proceeding from there.
However, this approach is somewhat unsatisfying. Why did we have to invent a new object just to bundle up the data we needed? Furthermore, cones are somewhat disconnected from the rest of category theory, which makes it more difficult to integrate results about limits into the larger body of work. It would be great if we could encode the data we needed using existing objects!
Luckily, we can! If we take a step back, we can notice that we are trying to construct a map into a functor. What are maps into functors? Natural transformations! Concretely, let be some diagram. We can encode the same data as a cone in a natural transformation where denotes the constant functor that maps object to and every morphism to and denotes the unique functor into the terminal category. The components of such a natural transformation yield maps from for every and naturality ensures that these maps must commute with the rest of the diagram. We can describe this situation diagrammatically like so:
All that remains is the universal property. If we translate this into our existing machinery, that means that must be the universal functor equipped with a natural transformation that is, for any other equipped with we have a unique natural transformation that factors This is a bit of a mouthful, so letβs look at a diagram instead.
We might be tempted to stop here and call it a day, but we can go one step further. It turns out that these universal functors have a name: they are right Kan extensions. This allows for an extremely concise definition of limits: is the limit of a diagram when the constant functor is a right Kan extension of along
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} (Diagram : Functor J C) where private module C = Precategory C open _=>_ open Functor is-limit : (x : C.Ob) β Const x => Diagram β Type _ is-limit x cone = is-ran !F Diagram (!Const x) cone
In a βbundledβ form, we may define the type of limits for a diagram as the type of right extensions of along the terminating functor
Limit : Type _ Limit = Ran !F Diagram
Concretelyπ
The definition above is very concise, and it has the benefit of being abstract: We can re-use definitions and theorems originally stated for right Kan extensions to limits. However, it has the downside of being abstract: itβs good for working with limits in general, but working with a specific limit is penalised, as the data we want to get at is βburiedβ.
The definition above is also hard to instantiate, since you
have to.. bury the data, and some of it is really quite deep! What we do
is provide an auxiliary record, make-is-limit
, which
computes right extensions to the point.
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} where private module J = Precategory J module C = Cat.Reasoning C record make-is-limit (Diagram : Functor J C) (apex : C.Ob) : Type (oβ β hβ β oβ β hβ) where no-eta-equality open Functor Diagram
We solve this by defining a concretised version of is-limit
, called make-is-limit
, which
exposes the following data. First, we have morphisms from the apex to
every value in the diagram, a family called
Moreover, if
is a morphism in the βshapeβ category
then
i.e., the
maps fit into triangles
field Ο : (j : J.Ob) β C.Hom apex (Fβ j) commutes : β {x y} (f : J.Hom x y) β Fβ f C.β Ο x β‘ Ο y
The rest of the data says that is the universal family of maps with this property: If is another family of maps with the same commutativity property, then each factors through the apex by a single, unique universal morphism:
universal : β {x : C.Ob} β (eps : β j β C.Hom x (Fβ j)) β (β {x y} (f : J.Hom x y) β Fβ f C.β eps x β‘ eps y) β C.Hom x apex factors : β {j : J.Ob} {x : C.Ob} β (eps : β j β C.Hom x (Fβ j)) β (p : β {x y} (f : J.Hom x y) β Fβ f C.β eps x β‘ eps y) β Ο j C.β universal eps p β‘ eps j unique : β {x : C.Ob} β (eps : β j β C.Hom x (Fβ j)) β (p : β {x y} (f : J.Hom x y) β Fβ f C.β eps x β‘ eps y) β (other : C.Hom x apex) β (β j β Ο j C.β other β‘ eps j) β other β‘ universal eps p
uniqueβ : β {x : C.Ob} β (eps : β j β C.Hom x (Fβ j)) β (p : β {x y} (f : J.Hom x y) β Fβ f C.β eps x β‘ eps y) β {o1 : C.Hom x apex} β (β j β Ο j C.β o1 β‘ eps j) β {o2 : C.Hom x apex} β (β j β Ο j C.β o2 β‘ eps j) β o1 β‘ o2 uniqueβ {x = x} eps p q r = unique eps p _ q β sym (unique eps p _ r)
If we have this data, then we can make a value of is-limit
. It might seem like
naturality, required for a right Kan extension, is missing from make-is-limit
, but it can
be derived from the other data we have been given:
open _=>_ to-cone : β {D : Functor J C} {apex} β make-is-limit D apex β Const apex => D to-cone ml .Ξ· = ml .make-is-limit.Ο to-cone ml .is-natural x y f = C.idr _ β sym (ml .make-is-limit.commutes f)
to-is-limit : β {D : Functor J C} {apex} β (mk : make-is-limit D apex) β is-limit D apex (to-cone mk) to-is-limit {Diagram} {apex} mklim = lim where open make-is-limit mklim open is-ran open Functor open _=>_ lim : is-limit Diagram apex (to-cone mklim) lim .Ο {M = M} Ξ± .Ξ· _ = universal (Ξ± .Ξ·) (Ξ» f β sym (Ξ± .is-natural _ _ f) β C.elimr (M .F-id)) lim .Ο {M = M} Ξ± .is-natural _ _ _ = lim .Ο Ξ± .Ξ· _ C.β M .Fβ tt β‘β¨ C.elimr (M .F-id) β©β‘ lim .Ο Ξ± .Ξ· _ β‘Λβ¨ C.idl _ β©β‘Λ C.id C.β lim .Ο Ξ± .Ξ· _ β lim .Ο-comm {Ξ² = Ξ²} = ext Ξ» j β factors (Ξ² .Ξ·) _ lim .Ο-uniq {Ξ² = Ξ²} {Ο' = Ο'} p = ext Ξ» _ β sym $ unique (Ξ² .Ξ·) _ (Ο' .Ξ· tt) (Ξ» j β sym (p Ξ·β j))
generalize-limitp : β {D : Functor J C} {K : Functor β€Cat C} β {eps : (Const (Functor.Fβ K tt)) => D} {eps' : K Fβ !F => D} β is-ran !F D (!Const (Functor.Fβ K tt)) eps β (β {j} β eps .Ξ· j β‘ eps' .Ξ· j) β is-ran !F D K eps' generalize-limitp {D} {K} {eps} {eps'} ran q = ran' where module ran = is-ran ran open is-ran open Functor ran' : is-ran !F D K eps' ran' .Ο Ξ± = !constβΏ (ran.Ο Ξ± .Ξ· tt) ran' .Ο-comm {M} {Ξ²} = ext Ξ» j β ap (C._β _) (sym q) β ran.Ο-comm {Ξ² = Ξ²} Ξ·β _ ran' .Ο-uniq {M} {Ξ²} {Ο'} r = ext Ξ» j β ran.Ο-uniq {Ο' = !constβΏ (Ο' .Ξ· tt)} (ext Ξ» j β r Ξ·β j β ap (C._β _) (sym q)) Ξ·β j to-is-limitp : β {D : Functor J C} {K : Functor β€Cat C} {eps : K Fβ !F => D} β (mk : make-is-limit D (Functor.Fβ K tt)) β (β {j} β to-cone mk .Ξ· j β‘ eps .Ξ· j) β is-ran !F D K eps to-is-limitp {D} {K} {eps} mklim p = generalize-limitp (to-is-limit mklim) p
To use the data of is-limit
, we provide a
function for unmaking a limit:
unmake-limit : β {D : Functor J C} {F : Functor β€Cat C} {eps} β is-ran !F D F eps β make-is-limit D (F Β· tt)
unmake-limit {D} {F} {eps = eps} lim = ml module unmake-limit where a = F Β· tt module eps = _=>_ eps open is-ran lim open Functor D open make-is-limit open _=>_ module _ {x} (eps : β j β C.Hom x (Fβ j)) (p : β {x y} (f : J.Hom x y) β Fβ f C.β eps x β‘ eps y) where eps-nt : Const x => D eps-nt .Ξ· = eps eps-nt .is-natural _ _ f = C.idr _ β sym (p f) hom : C.Hom x a hom = Ο {M = !Const x} eps-nt .Ξ· tt ml : make-is-limit D a ml .Ο j = eps.Ξ· j ml .commutes f = sym (eps.is-natural _ _ f) β C.elimr (F .Functor.F-id) ml .universal = hom ml .factors e p = Ο-comm {Ξ² = eps-nt e p} Ξ·β _ ml .unique {x = x} eps p other q = sym $ Ο-uniq {Ο' = other-nt} (ext Ξ» j β sym (q j)) Ξ·β tt where other-nt : !Const x => F other-nt .Ξ· _ = other other-nt .is-natural _ _ _ = C.idr _ β C.introl (F .Functor.F-id) to-limit : β {D : Functor J C} {K : Functor β€Cat C} {eps : K Fβ !F => D} β is-ran !F D K eps β Limit D to-limit l .Ran.Ext = _ to-limit l .Ran.eps = _ to-limit l .Ran.has-ran = l
module is-limit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} {F : Functor β€Cat C} {eps : F Fβ !F => D} (t : is-ran !F D F eps) where open make-is-limit (unmake-limit {F = F} t) public
We also provide a similar interface for the bundled form of limits.
module Limit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} (L : Limit D) where
private import Cat.Reasoning J as J import Cat.Reasoning C as C module Diagram = Functor D open Functor open _=>_ open Ran L public
The βapexβ object of the limit is the single value in the image of the extension functor.
apex : C.Ob apex = Ext.β tt
Furthermore, we can show that the apex is the limit, in the sense of
is-limit
,
of the diagram. Youβd think this is immediate, but unfortunately, proof
assistants: is-limit
asks for
the constant functor functor
with value apex
to be a Kan extension, but Limit
, being an instance of
Ran
,
packages an arbitrary functor
Since Agda does not compare functors for we have to shuffle our data around manually. Fortunately, this isnβt a very long computation.
cone : Const apex => D cone .Ξ· x = eps .Ξ· x cone .is-natural x y f = ap (_ C.β_) (sym $ Ext .F-id) β eps .is-natural x y f has-limit : is-limit D apex cone has-limit .is-ran.Ο Ξ± .Ξ· = Ο Ξ± .Ξ· has-limit .is-ran.Ο Ξ± .is-natural x y f = Ο Ξ± .is-natural tt tt tt β ap (C._β _) (Ext .F-id) has-limit .is-ran.Ο-comm = ext (Ο-comm Ξ·β_) has-limit .is-ran.Ο-uniq {M = M} {Ο' = Ο'} p = ext Ξ» _ β Ο-uniq {Ο' = nt} (reext! p) Ξ·β _ where nt : M => Ext nt .Ξ· = Ο' .Ξ· nt .is-natural x y f = Ο' .is-natural x y f β ap (C._β _) (sym $ Ext .F-id) open is-limit has-limit public
Uniquenessπ
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} {x y} {epsy : Const y => Diagram} {epsx : Const x => Diagram} (Ly : is-limit Diagram y epsy) (Lx : is-limit Diagram x epsx) where private module J = Precategory J module C = Cat.Reasoning C module Diagram = Functor Diagram open is-ran open _=>_ module Ly = is-limit Ly module Lx = is-limit Lx
Above, there has been mention of the limit. The limit of a diagram, if it exists, is unique up to isomorphism. This follows directly from uniqueness of Kan extensions.
We show a slightly more general result first: if there exist a pair of maps between the apexes of the two limits, and these maps commute with the two limits, then and are inverses.
limitsβinversesp : β {f : C.Hom x y} {g : C.Hom y x} β (β {j : J.Ob} β Ly.Ο j C.β f β‘ Lx.Ο j) β (β {j : J.Ob} β Lx.Ο j C.β g β‘ Ly.Ο j) β C.Inverses f g limitsβinversesp {f = f} {g = g} f-factor g-factor = inversesβΏβinverses {Ξ± = !constβΏ f} {Ξ² = !constβΏ g} (Ran-unique.Ο-inversesp Ly Lx (ext Ξ» j β f-factor {j}) (ext Ξ» j β g-factor {j})) tt
Furthermore, any morphism between apexes that commutes with the limit must be invertible.
limitsβinvertiblep : β {f : C.Hom x y} β (β {j : J.Ob} β Ly.Ο j C.β f β‘ Lx.Ο j) β C.is-invertible f limitsβinvertiblep {f = f} f-factor = is-invertibleβΏβis-invertible {Ξ± = !constβΏ f} (Ran-unique.Ο-is-invertiblep Ly Lx (ext Ξ» j β f-factor {j})) tt
This implies that the universal maps must also be inverses.
limitsβinverses : C.Inverses (Ly.universal Lx.Ο Lx.commutes) (Lx.universal Ly.Ο Ly.commutes) limitsβinverses = limitsβinversesp (Ly.factors Lx.Ο Lx.commutes) (Lx.factors Ly.Ο Ly.commutes) limitsβinvertible : C.is-invertible (Ly.universal Lx.Ο Lx.commutes) limitsβinvertible = limitsβinvertiblep (Ly.factors Lx.Ο Lx.commutes)
Finally, we can bundle this data up to show that the apexes are isomorphic.
limits-unique : x C.β y limits-unique = isoβΏβiso (Ran-unique.unique Lx Ly) tt
Furthermore, if the universal map is invertible, then that means that its domain is also a limit of the diagram.
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} {K : Functor β€Cat C} {epsy : Const (Functor.Fβ K tt) => D} (Ly : is-limit D (Functor.Fβ K tt) epsy) where private module J = Precategory J module C = Cat.Reasoning C module D = Functor D open is-ran open Functor open _=>_ module Ly = is-limit Ly familyβcone : β {x} β (eps : β j β C.Hom x (D.β j)) β (β {x y} (f : J.Hom x y) β D.β f C.β eps x β‘ eps y) β Const x => D familyβcone eps p .Ξ· = eps familyβcone eps p .is-natural _ _ _ = C.idr _ β sym (p _)
is-invertibleβis-limitp : β {K' : Functor β€Cat C} {eps : K' Fβ !F => D} β (eps' : β j β C.Hom (K' .Fβ tt) (D.β j)) β (p : β {x y} (f : J.Hom x y) β D.β f C.β eps' x β‘ eps' y) β (β {j} β eps' j β‘ eps .Ξ· j) β C.is-invertible (Ly.universal eps' p) β is-ran !F D K' eps is-invertibleβis-limitp {K' = K'} eps' p q invert = generalize-limitp (is-invertibleβis-ran Ly $ invertibleβinvertibleβΏ _ (Ξ» _ β invert)) q
Another useful fact is that if is a limit of some diagram and is naturally isomorphic to some other diagram then the apex of is also a limit of
natural-iso-diagramβis-limitp : β {D' : Functor J C} {eps : K Fβ !F => D'} β (isos : D β βΏ D') β (β {j} β IsoβΏ.to isos .Ξ· j C.β Ly.Ο j β‘ eps .Ξ· j) β is-ran !F D' K eps natural-iso-diagramβis-limitp {D' = D'} isos p = generalize-limitp (natural-iso-ofβis-ran Ly isos) p
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D D' : Functor J C} where natural-isoβlimit : D β βΏ D' β Limit D β Limit D' natural-isoβlimit isos L .Ran.Ext = Ran.Ext L natural-isoβlimit isos L .Ran.eps = IsoβΏ.to isos βnt Ran.eps L natural-isoβlimit isos L .Ran.has-ran = natural-iso-ofβis-ran (Ran.has-ran L) isos
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} {x} {eps : Const x => Diagram} where private module J = Precategory J module C = Cat.Reasoning C module Diagram = Functor Diagram open is-ran open _=>_ is-limit-is-prop : is-prop (is-limit Diagram x eps) is-limit-is-prop = is-ran-is-prop
Since limits are unique βup to isomorphismβ, if
is a univalent category, then Limit
itself is a
proposition! This is an instance of the more general uniqueness of Kan extensions.
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} where
Limit-is-prop : is-category C β is-prop (Limit Diagram) Limit-is-prop cat = Ran-is-prop cat
Completenessπ
A category is complete if it admits limits for diagrams 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 a poset. 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 if it has limits for any diagram indexed by a precategory with objects in and morphisms in
is-complete : β {oc βc} o β β Precategory oc βc β Type _ is-complete oj βj C = β {J : Precategory oj βj} (F : Functor J C) β Limit F
is-complete-lower : β {o β} {C : Precategory o β} oβ ββ oβ ββ β is-complete (oβ β oβ) (ββ β ββ) C β is-complete oβ ββ C is-complete-lower oβ ββ _ _ compl {J} F = to-limit (to-is-limit mk) where lim = compl {J = Lift-cat oβ ββ J} (Lift-functor-l _ _ F) module lim = Limit lim open make-is-limit mk : make-is-limit F lim.apex mk .Ο j = lim.Ο (lift j) mk .commutes f = lim.commutes _ mk .universal eps x = lim.universal (Ξ» j β eps (j .lower)) (Ξ» f β x (f .lower)) mk .factors eps p = lim.factors _ _ mk .unique eps p other x = lim.unique _ _ _ Ξ» j β x (j .lower)
While this condition might sound very strong, and thus that it would be hard to come by, it turns out we can get away with only two fundamental types of limits: products and equalisers. In order to construct the limit for a diagram of shape we will require products indexed by type of objects and by its type of morphisms.
module _ {o β} {C : Precategory o β} where private module C = Cat.Reasoning C open Indexed-product open make-is-limit open Equaliser
limit-as-equaliser-of-product : β {oj βj} {J : Precategory oj βj} β has-products-indexed-by C β J β β has-products-indexed-by C (Arrows J) β has-equalisers C β (F : Functor J C) β Limit F limit-as-equaliser-of-product {oj} {βj} {J} has-Ob-prod has-Arrows-prod has-eq F = to-limit (to-is-limit lim) where
Given a diagram we start by building the product of all the objects appearing in the diagram.
Obs : Indexed-product C Ξ» o β Fβ o Obs = has-Ob-prod _
Our limit will arise as a subobject of this product-of-objects, namely the equaliser of two carefully chosen morphisms.
As a guiding example, the pullback of and should be the subobject of consisting of triples such that In full generality, for each arrow in our diagram, we should have that projecting out the component of our product should give the same result as projecting out the component and postcomposing with
This suggests to build another indexed product of all the codomains of arrows in the diagram, taking the first morphism to be the projection of the codomain and the second morphism to be the projection of the domain postcomposed with
Cod : Indexed-product C {Idx = Arrows J} Ξ» (a , b , f) β Fβ b Cod = has-Arrows-prod _ s t : C.Hom (Obs .Ξ F) (Cod .Ξ F) s = Cod .tuple Ξ» (a , b , f) β Fβ f C.β Obs .Ο a t = Cod .tuple Ξ» (a , b , f) β Obs .Ο b eq : Equaliser C s t eq = has-eq _ _ lim : make-is-limit F (eq .apex)
The rest of the proof amounts to repackaging the data of the equaliser and products as the data for a limit.
lim .Ο c = Obs .Ο c C.β eq .equ lim .commutes {a} {b} f = Fβ f C.β Obs .Ο a C.β eq .equ β‘Λβ¨ C.extendl (Cod .commute) β©β‘Λ Cod .Ο (a , b , f) C.β β s C.β eq .equ β β‘β¨ ap! (eq .equal) β©β‘ Cod .Ο (a , b , f) C.β t C.β eq .equ β‘β¨ C.pulll (Cod .commute) β©β‘ Obs .Ο b C.β eq .equ β lim .universal {x} e comm = eq .universal comm' where e' : C.Hom x (Obs .Ξ F) e' = Obs .tuple e comm' : s C.β e' β‘ t C.β e' comm' = Indexed-product.uniqueβ Cod Ξ» i@(a , b , f) β Cod .Ο i C.β s C.β e' β‘β¨ C.extendl (Cod .commute) β©β‘ Fβ f C.β β Obs .Ο a C.β e' β β‘β¨ ap! (Obs .commute) β©β‘ Fβ f C.β e a β‘β¨ comm f β©β‘ e b β‘Λβ¨ Obs .commute β©β‘Λ Obs .Ο b C.β e' β‘Λβ¨ C.pulll (Cod .commute) β©β‘Λ Cod .Ο i C.β t C.β e' β lim .factors {j} e comm = (Obs .Ο j C.β eq .equ) C.β lim .universal e comm β‘β¨ C.pullr (eq .factors) β©β‘ Obs .Ο j C.β Obs .tuple e β‘β¨ Obs .commute β©β‘ e j β lim .unique e comm u' fac = eq .unique $ Obs .unique _ Ξ» i β C.assoc _ _ _ β fac i
This implies that a category with equalisers and large enough indexed products has all limits.
products+equalisersβcomplete : β {oj βj} β has-indexed-products C (oj β βj) β has-equalisers C β is-complete oj βj C products+equalisersβcomplete {oj} {βj} has-prod has-eq = limit-as-equaliser-of-product (Ξ» _ β Lift-Indexed-product C βj (has-prod _)) (Ξ» _ β has-prod _) has-eq
Preservation of limitsπ
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) (Diagram : Functor J C) where
Suppose you have a limit of a diagram in We say that preserves if is also a limit of in More precisely, we say a functor preserves limits of if it takes limiting cones βupstairsβ to limiting cones βdownstairsβ.
This definition is necessary because will not, in general, possess an operation assigning a limit to every diagram β therefore, there might not be a βcanonical limitβ of we could compare 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.
preserves-limit : Type _ preserves-limit = preserves-ran !F Diagram F
Reflection of limitsπ
Using the terminology from before, we say a functor reflects limits if it only takes limiting cones βupstairsβ to limiting cones βdownstairsβ: this is the converse implication from preservation of limits. More concretely, if we have a cone over in whose image under is a limiting cone over in then reflects this limit if we already had a limiting cone in to begin with!
reflects-limit : Type _ reflects-limit = reflects-ran !F Diagram F
module preserves-limit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F : Functor C D} {Dia : Functor J C} (preserves : preserves-limit F Dia) {K : Functor β€Cat C} {eps : K Fβ !F => Dia} (lim : is-ran !F Dia K eps) where private module D = Precategory D module C = Precategory C module J = Precategory J module F = Func F module Dia = Func Dia module lim = is-limit lim module F-lim = is-limit (preserves lim) universal : {x : C.Ob} β {eps : (j : J.Ob) β C.Hom x (Dia.Fβ j)} β {p : β {i j} (f : J.Hom i j) β Dia.Fβ f C.β eps i β‘ eps j} β F.Fβ (lim.universal eps p) β‘ F-lim.universal (Ξ» j β F.Fβ (eps j)) (Ξ» f β F.collapse (p f)) universal = F-lim.unique _ _ _ (Ξ» j β F.collapse (lim.factors _ _)) module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F F' : Functor C D} {Dia : Functor J C} where private module D = Cat.Reasoning D open Func open _=>_ natural-isoβpreserves-limits : F β βΏ F' β preserves-limit F Dia β preserves-limit F' Dia natural-isoβpreserves-limits Ξ± F-preserves {G = K} {eps} lim = natural-isosβis-ran idni (Ξ± βni Dia) (Ξ± βni K) (ext Ξ» j β Ξ±.to .Ξ· _ D.β (F .Fβ (eps .Ξ· j) D.β β F .Fβ (K .Fβ tt) D.β Ξ±.from .Ξ· _ β) β‘β¨ ap! (eliml F (K .F-id)) β©β‘ Ξ±.to .Ξ· _ D.β (F .Fβ (eps .Ξ· j) D.β Ξ±.from .Ξ· _) β‘β¨ D.pushr (sym (Ξ±.from .is-natural _ _ _)) β©β‘ (Ξ±.to .Ξ· _ D.β Ξ±.from .Ξ· _) D.β F' .Fβ (eps .Ξ· j) β‘β¨ D.eliml (Ξ±.invl Ξ·β _) β©β‘ F' .Fβ (eps .Ξ· j) β) (F-preserves lim) where module Ξ± = IsoβΏ Ξ±
Continuityπ
is-continuous : β (oshape hshape : Level) {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 hshape {C = C} F = β {J : Precategory oshape hshape} {Diagram : Functor J C} β preserves-limit F Diagram
Lifting and creation of limitsπ
Preserving and reflecting arenβt the only interesting things a functor can do to a limit. Suppose we have a diagram such that has a limiting cone in We say that lifts this limit if already had a limiting cone in and furthermore sends this cone to (up to isomorphism). Equivalently, since limits are unique, we can simply ask for to preserve
Note the difference with reflected limits: whereas reflecting a limit requires already having a cone in lifting a limit gives us a limiting cone in from a limiting cone in As an example, reflecting terminal objects means that, if is terminal in then was already terminal in by contrast, lifting terminal objects means that, if has a terminal object, then so does and (equivalently, is terminal).
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) {Diagram : Functor J C} where
record lifts-limit (lim : Limit (F Fβ Diagram)) : Type (oβ β hβ β oβ β hβ β oβ β hβ) where no-eta-equality field lifted : Limit Diagram preserved : preserves-is-ran F (Limit.has-ran lifted) liftsβpreserves-limit : preserves-limit F Diagram liftsβpreserves-limit = preserves-is-ranβpreserves-ran F (Limit.has-ran lifted) preserved
If furthermore reflects limits of then we say that creates those limits. This means equivalently that, for every limiting cone over there is a unique (up to isomorphism) cone in over it, and furthermore this cone is limiting.
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) (Diagram : Functor J C) where
record creates-limit : Type (oβ β hβ β oβ β hβ β oβ β hβ) where no-eta-equality field has-lifts-limit : (lim : Limit (F Fβ Diagram)) β lifts-limit F lim reflects : reflects-limit F Diagram
The definitions we have given here are standard, but one sometimes encounters the following alternative definition:
β
creates limits of
if it preserves and reflects limits of
and furthermore if
has a limit then
has a limit.β
While this may seem equivalent at first glance, there is a subtle difference: this definition says that unconditionally preserves limits of whereas our definition only says that preserves the limits that it creates; in other words, only preserves limits of if has a limit to begin with.
To see the difference, take to be one of the inclusions of the terminal category into the two-object category. Since does not have a terminal object, vacuously creates terminal objects; on the other hand, does not preserve terminal objects, since the unique object of which is terminal, is taken to a non-terminal object in
Because of this quirk, some authors write things like β creates all limits that exist in its codomainβ to be fully explicit. Using our definition, this side condition is redundant, so we will omit it.
We say that lifts (resp. creates) limits of shape if it lifts (resp. creates) limits of every diagram
module _ (J : Precategory oβ hβ) {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) where
lifts-limits-of : Type _ lifts-limits-of = β {Diagram : Functor J C} (lim : Limit (F Fβ Diagram)) β lifts-limit F lim creates-limits-of : Type _ creates-limits-of = β {Diagram : Functor J C} β creates-limit F Diagram
A useful observation is that, if lifts limits and is complete, then so is
lifts-limitsβcomplete : β {oj βj} β (β {J : Precategory oj βj} β lifts-limits-of J F) β is-complete oj βj D β is-complete oj βj C lifts-limitsβcomplete lifts dcomp Diagram = lifts (dcomp (F Fβ Diagram)) .lifts-limit.lifted
Stability under compositionπ
We conclude this section by proving that the properties above β preservation, reflection, lifting and creation of limits β are stable under functor composition.
module _ {C : Precategory oβ hβ} {D : Precategory oβ hβ} {E : Precategory oβ hβ} {F : Functor C D} {G : Functor D E} where open lifts-limit open creates-limit private fixup : β {oj βj} {J : Precategory oj βj} {Diagram : Functor J C} β {K : Functor β€Cat C} {eps : K Fβ !F => Diagram} β is-ran !F (G Fβ F Fβ Diagram) (G Fβ F Fβ K) (nat-assoc-from (G βΈ nat-assoc-from (F βΈ eps))) β is-ran !F ((G Fβ F) Fβ Diagram) ((G Fβ F) Fβ K) (nat-assoc-from ((G Fβ F) βΈ eps)) fixup = trivial-ran-equiv!
First, if preserves limits of and preserves limits of then preserves limits of conversely, if and reflect those limits, then so does
Fβ-preserves-limits : β {oj βj} {J : Precategory oj βj} {Diagram : Functor J C} β preserves-limit F Diagram β preserves-limit G (F Fβ Diagram) β preserves-limit (G Fβ F) Diagram Fβ-preserves-limits F-preserves G-preserves = Equiv.to fixup β G-preserves β F-preserves Fβ-reflects-limits : β {oj βj} {J : Precategory oj βj} {Diagram : Functor J C} β reflects-limit F Diagram β reflects-limit G (F Fβ Diagram) β reflects-limit (G Fβ F) Diagram Fβ-reflects-limits F-reflects G-reflects = F-reflects β G-reflects β Equiv.from fixup
Now, assume and both lift limits of shape and we have a limit of in lifts this to a limit of in in turn, lifts this to a limit of in The fact that preserves this limit follows from the previous result.
Fβ-lifts-limits : β {oj βj} {J : Precategory oj βj} β lifts-limits-of J F β lifts-limits-of J G β lifts-limits-of J (G Fβ F) Fβ-lifts-limits F-lifts G-lifts lim = Ξ» where .lifted β lim'' .preserved β Fβ-preserves-limits (liftsβpreserves-limit lifted-lim') (liftsβpreserves-limit lifted-lim) (Ran.has-ran lim'') where lifted-lim = G-lifts (natural-isoβlimit (ni-assoc niβ»ΒΉ) lim) lim' = lifted-lim .lifted lifted-lim' = F-lifts lim' lim'' = lifted-lim' .lifted
Since lifting and reflection of limits are closed under composition, so is creation.
Fβ-creates-limits : β {oj βj} {J : Precategory oj βj} β creates-limits-of J F β creates-limits-of J G β creates-limits-of J (G Fβ F) Fβ-creates-limits F-creates G-creates .has-lifts-limit = Fβ-lifts-limits (F-creates .has-lifts-limit) (G-creates .has-lifts-limit) Fβ-creates-limits F-creates G-creates .reflects = Fβ-reflects-limits (F-creates .reflects) (G-creates .reflects)