module Cat.Diagram.Monad.Limits {o β} {C : Precategory o β} {M : Monad C} where
private module EM = Cat.Reasoning (Eilenberg-Moore C M) module C = Cat.Reasoning C module M = Monad M open Algebra-hom open Algebra-on
Limits in categories of algebrasπ
Suppose that be a category, be a monad on , and be a -shaped diagram of -algebras (that is, a functor into the Eilenberg-Moore category of M). Suppose that an evil wizard has given you a limit for the diagram in which underlies , but they have not (being evil and all) told you whether admits an algebra structure at all.
Perhaps we can make this situation slightly more concrete, by working in a category equivalent to an Eilenberg-Moore category: If we have two groups , , considered as a discrete diagram, then the limit our evil wizard would give us is the product in . But we already know we can equip this product with a βpointwiseβ group structure! Does this result generalise?
The answer is positive, though this is one of those cases where abstract nonsense can not help us: gotta roll up our sleeves and calculate away. Suppose we have a diagram as in the setup β weβll show that the functor both preserves and reflects limits, in that is a limiting cone if, and only if, is.
module _ {jo jβ} {J : Precategory jo jβ} (F : Functor J (Eilenberg-Moore C M)) where private module J = Precategory J module F = Functor F module FAlg j = Algebra-on (F.β j .snd) open Functor open _=>_
We begin with the following key lemma: Write for the limit of a diagram . If carries an -algebra structure , and the limit projections are -algebra morphisms, then is the limit of in .
make-algebra-limit : β {K : Functor β€Cat C} {eps : K Fβ !F => Forget C M Fβ F} β (lim : is-ran !F (Forget C M Fβ F) K eps) β (nu : Algebra-on C M (K .Fβ tt)) β (β j β is-limit.Ο lim j C.β nu .Ξ½ β‘ FAlg.Ξ½ j C.β M.Mβ (is-limit.Ο lim j)) β make-is-limit F (K .Fβ tt , nu) make-algebra-limit lim apex-alg comm = em-lim where module lim = is-limit lim open make-is-limit module apex = Algebra-on apex-alg open _=>_
The assumptions to this lemma are actually rather hefty: they pretty much directly say that was already the limit of . However, with this more βelementaryβ rephrasing, we gain a bit of extra control which will be necessary for constructing limits in out of limits in later.
em-lim : make-is-limit F _ em-lim .Ο j .morphism = lim.Ο j em-lim .Ο j .commutes = comm j em-lim .commutes f = ext (lim.commutes f) em-lim .universal eta p .morphism = lim.universal (Ξ» j β eta j .morphism) (Ξ» f i β p f i .morphism) em-lim .factors eta p = ext (lim.factors _ _) em-lim .unique eta p other q = ext (lim.unique _ _ _ Ξ» j i β q j i .morphism) em-lim .universal eta p .commutes = lim.uniqueβ _ (Ξ» f β C.pulll (F.Fβ f .commutes) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (ap morphism (p f)))) (Ξ» j β C.pulll (lim.factors _ _) β eta j .commutes) (Ξ» j β C.pulll (comm j) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim.factors _ _)))
This key lemma also doubles as a proof that the underlying object functor reflects limits: We already had an algebra structure βupstairsβ!
Forget-reflects-limits : reflects-limit (Forget C M) F Forget-reflects-limits {K} {eps} lim = to-is-limitp (make-algebra-limit lim (K .Fβ tt .snd) (Ξ» j β eps .Ξ· j .commutes)) trivial!
Having shown that reflects the property of being a limit, we now turn to showing it reflects limits in general. Using our key lemma, it will suffice to construct an algebra structure on , then show that the projection maps extend to algebra homomorphisms.
Forget-lift-limit : Limit (Forget C M Fβ F) β Limit F Forget-lift-limit lim-over = to-limit $ to-is-limit $ make-algebra-limit (Limit.has-limit lim-over) apex-algebra (Ξ» j β lim-over.factors _ _) where module lim-over = Limit lim-over module lim = Ran lim-over
An algebra structure consists, centrally, of a map : a map into the limit. Maps into limits are the happy case, since is essentially defined by a (natural) isomorphism between the sets and , the latter limit being computed in . We understand limits of sets very well: theyβre (subsets of) sets of tuples!
Our algebra map is thus defined componentwise: Since we have a bunch of maps , coming from the algebra structures on each , we can βtupleβ them into a big map . Abusing notation slightly, weβre defining to be .
apex-algebra : Algebra-on C M lim-over.apex apex-algebra .Ξ½ = lim-over.universal (Ξ» j β FAlg.Ξ½ j C.β M.Mβ (lim-over.Ο j)) comm where abstract comm : β {x y} (f : J.Hom x y) β F.β f .morphism C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x) β‘ FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y) comm {x} {y} f = F.β f .morphism C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x) β‘β¨ C.extendl (F.β f .commutes) β©β‘ FAlg.Ξ½ y C.β M.Mβ (F.β f .morphism) C.β M.Mβ (lim-over.Ο x) β‘Λβ¨ C.reflβ©ββ¨ M.M-β _ _ β©β‘Λ FAlg.Ξ½ y C.β M.Mβ (F.β f .morphism C.β lim-over.Ο x) β‘β¨ C.reflβ©ββ¨ ap M.Mβ (lim-over.commutes f) β©β‘ FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y) β
To show that really is an algebra structure, weβll reason componentwise, too: we must show that is the identity map: but we can compute
The other condition, compatibility with βs multiplication, is analogous. Formally, the computation is a bit less pretty, but itβs no more complicated.
apex-algebra .Ξ½-unit = lim-over.uniqueβ _ lim-over.commutes (Ξ» j β C.pulll (lim-over.factors _ _) Β·Β· C.pullr (sym $ M.unit.is-natural _ _ _) Β·Β· C.cancell (FAlg.Ξ½-unit j)) (Ξ» j β C.idr _) apex-algebra .Ξ½-mult = lim-over.uniqueβ _ (Ξ» f β C.pulll $ C.pulll (F.β f .commutes) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim-over.commutes f))) (Ξ» j β C.pulll (lim-over.factors _ _) Β·Β· C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim-over.factors _ _) β M.M-β _ _) Β·Β· C.extendl (FAlg.Ξ½-mult j) Β·Β· ap (FAlg.Ξ½ j C.β_) (M.mult.is-natural _ _ _) Β·Β· C.assoc _ _ _) (Ξ» j β C.pulll (lim-over.factors _ _))
Putting our previous results together, we conclude by observing that, if is a complete category, then so is , regardless of how ill-behaved the monad might be.
Eilenberg-Moore-is-complete : β {a b} β is-complete a b C β is-complete a b (Eilenberg-Moore _ M) Eilenberg-Moore-is-complete complete F = Forget-lift-limit F (complete _)