open import Cat.Functor.Equivalence.Complete open import Cat.Functor.Conservative open import Cat.Functor.Equivalence open import Cat.Diagram.Limit.Base open import Cat.Diagram.Terminal open import Cat.Diagram.Monad open import Cat.Prelude import Cat.Reasoning module Cat.Diagram.Monad.Limits {o β} {C : Precategory o β} {M : Monad C} where
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 F = Functor F Forget-reflects-limits : (K : Cone F) β is-limit (Forget C M Fβ F) (F-map-cone (Forget C M) K) β is-limit F K Forget-reflects-limits K uniq other = contr ! unique where !β² = uniq (F-map-cone (Forget C M) other) .centre
Let be a cone over : Since is a limiting cone, then we have a unique map of , which we must show extends to a map of algebras , which by definition means . But those are maps β so if was a cone over , and those two were maps of cones, then they would be equal!
! : Cone-hom _ other K ! .hom .morphism = !β² .hom ! .hom .commutes = ap hom $ is-contrβis-prop (uniq coneβ²) (record { hom = !β² .hom C.β apex other .snd .Ξ½ ; commutes = Ξ» o β C.pulll (!β² .commutes o) }) (record { hom = apex K .snd .Ξ½ C.β M.Mβ (!β² .hom) ; commutes = Ξ» o β C.pulll (K .Ο o .commutes) Β·Β· C.pullr (sym (M.M-β _ _) β ap M.Mβ (!β² .commutes o)) Β·Β· sym (other .Ο o .commutes) })
The cone structure on is given by composites , which commute because is also a cone structure. More explicitly, what we must show is , which follows immediately.
where coneβ² : Cone (Forget C M Fβ F) coneβ² .apex = M.Mβ (apex other .fst) coneβ² .Ο x = morphism (Ο other x) C.β apex other .snd .Ξ½ coneβ² .commutes o = C.pulll (ap morphism (commutes other o)) ! .commutes o = Algebra-hom-path _ (uniq (F-map-cone (Forget C M) other) .centre .commutes o)
For uniqueness, we use that the map is unique, and that the functor is faithful.
unique : β x β ! β‘ x unique x = Cone-hom-path _ $ Algebra-hom-path _ $ ap hom (uniq (F-map-cone (Forget _ M) other) .paths homβ²) where homβ² : Cone-hom _ _ _ homβ² .hom = hom x .morphism homβ² .commutes o = ap morphism (x .commutes o)
I hope you like appealing to uniqueness of maps into limits, by the
way. We now relax the conditions on the theorem above, which relies on
the pre-existence of a cone
.
In fact, what we have shown is that Forget
reflects the
property of being a limit β what we now show is that it
reflects limit objects, too: if
has a limit, then so does
.
Forget-lift-limit : Limit (Forget _ M Fβ F) β Limit F Forget-lift-limit lim-over = record { top = coneβ² ; hasβ€ = Forget-reflects-limits coneβ² $ subst (is-limit _) (sym U$Lβ‘L) (lim-over .hasβ€) } where open Terminal module cone = Cone (lim-over .top)
What we must do, essentially, is prove that admits an algebra structure, much like we did for products of groups. In this, weβll use two auxiliary cones over , one with underlying object given by and one by . We construct the one with a single first, and re-use its maps in the construction of the one with .
The maps out of are given by the composite below, which assembles into a cone since is a map of algebras and is a cone.
coneβ : Cone (Forget _ M Fβ F) coneβ .apex = M.Mβ cone.apex coneβ .Ο x = F.β x .snd .Ξ½ C.β M.Mβ (cone.Ο x) coneβ .commutes {x} {y} f = F.β f .morphism C.β F.β x .snd .Ξ½ C.β M.Mβ (cone.Ο x) β‘β¨ C.pulll (F.β f .commutes) β©β‘ (F.β y .snd .Ξ½ C.β M.Mβ (F.β f .morphism)) C.β M.Mβ (cone.Ο x) β‘β¨ C.pullr (sym (M.M-β _ _) β ap M.Mβ (cone.commutes f)) β©β‘ F.β y .snd .Ξ½ C.β M.Mβ (cone.Ο y) β
Below, we can reuse the work we did above by precomposing with βs multiplication .
coneΒ² : Cone (Forget _ M Fβ F) coneΒ² .apex = M.Mβ (M.Mβ cone.apex) coneΒ² .Ο x = coneβ .Ο x C.β M.mult.Ξ· _ coneΒ² .commutes f = C.pulll (coneβ .commutes f)
We now define the algebra structure on . Itβs very tedious, but the multiplication is uniquely defined since itβs a map into a limit, and the algebraic identities follow from again from limits being terminal.
coneβ² : Cone F coneβ² .apex = cone.apex , alg where
alg : Algebra-on _ M cone.apex alg .Ξ½ = lim-over .hasβ€ coneβ .centre .hom alg .Ξ½-unit = ap hom $ is-contrβis-prop (lim-over .hasβ€ (lim-over .top)) (record { hom = alg .Ξ½ C.β M.unit.Ξ· cone.apex ; commutes = comm1 }) (record { hom = C.id ; commutes = Ξ» _ β C.idr _ }) alg .Ξ½-mult = ap hom $ is-contrβis-prop (lim-over .hasβ€ coneΒ²) (record { hom = alg .Ξ½ C.β M.Mβ (alg .Ξ½) ; commutes = comm2 }) (record { hom = alg .Ξ½ C.β M.mult.Ξ· cone.apex ; commutes = Ξ» o β C.pulll (lim-over .hasβ€ coneβ .centre .commutes o) })
The cone maps in are given by the cone maps we started with β specialising again to groups, weβre essentially showing that the projection map between sets is actually a group homomorphism.
coneβ² .Ο x .morphism = cone.Ο x coneβ² .Ο x .commutes = lim-over .hasβ€ coneβ .centre .commutes x coneβ² .commutes f = Algebra-hom-path _ (cone.commutes f) U$Lβ‘L : F-map-cone (Forget _ M) coneβ² β‘ lim-over .top U$Lβ‘L = Cone-path _ refl Ξ» o β refl
We conclude by saying that, if is a complete category, then so is , with no assumptions on .
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 _)