Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: questions

Topic: Limits in a category of fixpoints


view this post on Zulip fosco (Dec 20 2023 at 11:46):

I'm ironing some kinks in the paper I'm writing on fibrations from parametric functors. I have a problem with a statement.

Consider an accessible endofunctor FF of an accessible category CC; one can consider its category of algebras, and its category of "fixpoints" i.e. algebras such that the structure map is an isomorphism. The initial algebra of F will be an object of such category of fixpoints, by Lambek lemma.

Now: how are limits computed in the category of fixpoints? The nLab says that iteratively applying the completeness theorem for accessible categories one can prove that Fix(F)Fix(F) is accessible and cocomplete, hence locally presentable, so it's also complete. This is reasonable, as one can think this result de-categorifies to Knaster-Tarski.

But I think it's evident that the obvious embedding of fixpoints in algebras, regarding the former as full subcategory, can't preserve limits: a limit in algebras (Xi,ξi)(X_i,\xi_i) is computed giving to limXi\lim X_i the structure map F(limXi)limFXilimξilimFXiF(\lim X_i) \to \lim FX_i \xrightarrow{\lim \xi_i} \lim FX_i. Now, if all ξi\xi_i's are invertible, so is limξi\lim \xi_i, but then the whole algebra map will be invertible iff the canonical comparison FlimlimFF\lim \to \lim F is invertible, iff F preserves the limit in question. Edge case: fixpoints don't have as terminal object 11, if F1F1 is not terminal. But they are a complete category, in some different way.

Am I missing something, or indeed limits of fixpoints are computed in a weird way?

view this post on Zulip Todd Trimble (Dec 20 2023 at 13:41):

The example of the terminal object is convincing enough, so I don't think you're missing anything. However, I think it's true that the inclusion of fixpoints into algebras is coreflective. To check that it has a right adjoint, it suffices (by the adjoint functor theorem for locally presentable categories) that it preserve colimits, in other words that the colimit of a diagram of fixpoints as computed in the category of algebras is again a fixpoint. The proof of the latter statement, when written out, looks a lot like the Lambek lemma.

This means that the computation of limits in fixpoints, while perhaps a little weird, is not a total black box: you take the limit in the category of algebras, and then coreflect that back to fixpoints, to get the limit in fixpoints. I think this has a chance of being reasonably explicit, by tracing through the proof of the adjoint functor theorem.

view this post on Zulip fosco (Dec 20 2023 at 13:48):

Thank you! I will try to work out the details with this as a guidance

view this post on Zulip fosco (Dec 20 2023 at 15:31):

Given a square

FXFfFYXfY \begin{array}{ccc}FX &\overset{Ff}\to&FY\\ \downarrow && \downarrow\\ X &\underset f\to& Y\end{array}

where the left algebra map α\alpha is invertible, one gets a family of maps γn:XFnY\gamma_n : X\to F^nY inductively defines as γ0=f\gamma_0=f and γn+1=Fγnα1\gamma_{n+1} = F\gamma_n\circ\alpha^{-1}, which is actually a cone for the opchain

FYβYFY\xrightarrow\beta Y
FFYFβFYβYFFY\xrightarrow{F\beta} FY\xrightarrow\beta Y
FFFYFFYFYYFFFY\to FFY\to FY\to Y
...

view this post on Zulip fosco (Dec 20 2023 at 15:32):

This defines a unique map XlimnFnYX\to \lim_n F^n Y. So the candidate carrier for the coreflection of the algebra β\beta is indeed limnFnY\lim_n F^nY, which is compatible with the idea that the terminal object in fixpoints should be the terminal coalgebra of FF, by Adàmek theorem.

view this post on Zulip fosco (Dec 20 2023 at 15:33):

However, if FF doesn't preserve limits of op-chains, it seems that this object is not a fixpoint.

Do I have to assume it?

view this post on Zulip Todd Trimble (Dec 20 2023 at 16:01):

No, the nLab article titled Adamek's theorem (is it really an accent grave? I forget) just does the proof for the ω\omega-accessible case, but one can generalize the proof to handle κ\kappa-codirected limits. I actually just a few minutes ago "finished" (sketched) the incomplete proof of the dual statement, Theorem 5.1 here, and I may get around to fixing (heh) the one titled Adamek fixed point theorem, so as not to be restricted to the κ=ω\kappa = \omega case.

view this post on Zulip fosco (Dec 20 2023 at 16:03):

Well, that doesn't change the spirit of my question :grinning: sorry if it sounds stupid: F accessible means it preserves (long enough) colimits of chains . What about (co-long enough) limits of opchains? Is it for free?

view this post on Zulip Todd Trimble (Dec 20 2023 at 16:14):

Oh, wait, I see what you are asking. But no, I don't think that will work, and it wasn't the approach I was outlining earlier. I was suggesting to construct the coreflection Γ\Gamma of i:Fix(F)Alg(F)i: \mathrm{Fix(F)} \to \mathrm{Alg}(F) by means of colimits in comma categories, i.e., construct Γ(c)\Gamma(c) = terminal object of i()ci(-) \downarrow c as a suitable colimit in that comma category. I can try to be more explicit in a bit.

view this post on Zulip Todd Trimble (Dec 20 2023 at 16:35):

Okay, let me say it better this time (for the approach I was outlining before, I had in mind the proof of the General Adjoint Functor Theorem, but it seems to be better to use the Special Adjoint Functor Theorem, or SAFT [sounds juicy!]).

I guess I'll be lazy and direct attention to Theorem 2.2 here. The nLab mentions that you use the fact that locally presentable categories admit small generating sets and (nontrivial) are co-well-powered. Once you have those conditions, then you can apply the SAFT in its dual form (dualize the proof of SAFT given on the same nLab page). Anyway, it's a really explicit construction. Or, it's explicit modulo knowing how to construct colimits in Alg(F)\mathrm{Alg}(F) to begin with. :-)