10
$\begingroup$

A W-type is an initial algebra for a polynomial endofunctor $P$ on a category $C$. A well-known example is that of a natural numbers object (NNO). Usually it is assumed that $C$ is locally cartesian closed (lcc), but this only ensures that all polynomial endofunctors exist so as to ask whether the corresponding W-type exists, and it also simplifies the definition of W-type (one needs to use parameters if not in the lcc case, see for example the definition of an NNO in a merely finite-product category). One can always, in a lextensive category, talk about finitary polynomial endofunctors: these are 'really' polynomials, namely endofunctors of the form $$ X \mapsto \coprod_{i \leq n} A_i \times X^{\times i}, $$ for some collection of objects $\lbrace A_i\rbrace_{i \leq n}$, or, if countably extensive, with a coproduct over $\mathbb{N}$ (the external natural numbers), and this is the case in the example I'm particularly interested in (and I know it is not lcc, just a cocomplete pretopos with NNO, in the appropriate sense).

My question is this:

If I have an infinitary lextensive category (so all coproducts, compatible with pullbacks) that is locally cartesian closed, with an NNO, what W-types do I get for free? What if the category is not lcc?

The first question at least puts an upper bound on what I can expect, the second one is closer to what I expect to see.

$\endgroup$
2
  • 2
    $\begingroup$ I had convinced myself here, ncatlab.org/toddtrimble/published/…, that all W-types exist in an lcc infinitary extensive category that is well-powered. Of course, the well-poweredness assumption might be far too drastic for your purposes. $\endgroup$
    – Todd Trimble
    May 30, 2014 at 19:08
  • $\begingroup$ @ToddTrimble - thanks, I forgotten about that. I guess one could relax the infinitary extensivity condition to ordinary/finite extensivity and still get W-types for finitary polynomial functors. $\endgroup$
    – David Roberts
    May 31, 2014 at 2:00

1 Answer 1

6
$\begingroup$

If CC is infinitary lextensive and in addition locally small, then the global sections functor $\Gamma$ : CC --> Set has a lex left adjoint $\Delta$ : Set --> CC, and CC automatically has a natural numbers object since NNOs are preserved by inverse image functors. Moreover, the reason that this is the case can be formulated in a way that also works for initial algebras of more general polynomial functors.

If I haven't made a mistake, it should work at least for polynomial functors of the form $G(X)=\sum_n \Delta(A_n)\times X^n$, i.e. polynomial functors whose coefficients are in the image of $\Delta$. With each such polynomial functor on CC there comes an obvious polynomial functor $F(S)=\sum_n A_n\times S^n$ on Set, and if $T$ is an initial algebra for $F$, then I think that $\Delta T$ is an initial algebra for $G$.

The proof goes roughly as follows: Since $\Delta$ commutes with finite products and all coproducts we have $\Delta\circ F = G\circ \Delta$, whence applying $\Delta$ to the algebra structure $t: FT\to T$ on $T$ gives a $G$-algebra structure on $\Delta T$. Now given another $G$-algebra $x:GX\to X$ all we have to do is to find an $F$-algebra structure on $\Gamma X$ such that a morphism $f:\Delta T\to X$ is a $G$-algebra morphism iff its adjoint transpose is a $F$-algebra morphism. Initiality of $\Delta T$ among $G$-algebras then follows from initiality of $T$ among $F$-algebras.

The components of the algebra structure on $\Gamma X$ are given by $$ A_n\times (\Gamma X)^n\to\Gamma\Delta A_n\times (\Gamma X)^n\cong\Gamma(\Delta(A_n)\times X^n)\xrightarrow{\Gamma(x_n)}\Gamma X, $$ where $x_n:\Delta A_n\times X^n\to X$ is a component of $x:GX\to X$.

I also think that it is possible to construct free monoids in CC by the "tensor algebra formula" $A^*=\sum_n A^n$. However, this is not an instance of the previous construction since $A^*$ is the initial algebra for $H(X) = 1 + A\times X$ where $A$ appears as a coefficient and is not assumed in the image of $\Delta$. I wonder if there is a more general construction that comprises both as instances? Or did I get something totally wrong?

Anyway, all this supposes that CC is locally small, I don't know if this is the case in what you have in mind.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.