9
$\begingroup$

All sheaf topoi have W-types and in fact there's an explicit construction given by Benno van den Berg & Ieke Moerdijk, but the construction is quite involved.

I would like to know whether the inverse image part of a geometric morphism always preserves W-types for more general reasons or pointers to references detailing the conditions on functors so they preserve W-types.

Inverse image functors always preserve the natural numbers object, which is a particular kind of W-type, but the proof of this fact is very specific to the NNO so this might suggest that they don't all preserve W-types, but I have not found anything about this stated anywhere.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ I don't know enough about the details of W-types, but I conjecture that an old paper of mine might be useful: Well-ordering and induction in intuitionistic logic and topoi, in "Mathematical Logic and Theoretical Computer Science" (D. W. Kueker, E. G. K. Lopez-Escobar, and C. H. Smith, eds.) Marcel Dekker, Lecture Notes in Pure and Applied Mathematics 106 (1987) 22--48. One of the results in that paper is that inverse-image functors of topoi preserve totality of inductive constructions, which seems closely related to W-types. $\endgroup$
    – Andreas Blass
    Commented Sep 21, 2015 at 17:52
  • 3
    $\begingroup$ Presumably you at least need to require that the the inverse image functor respects the dependent product involved in the definition of the W-type. For finitary ones (that is, for initial algebras of endofunctors which are polynomial in the most restrictive sense, $A_0+A_1\times X+A_2\times X^2+...+A_{42}\times X^{42}$ say) or something slightly more general defined through NNO there should be no problem and it should work, but for more general W-types - I doubt it without additional requirements. $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Sep 21, 2015 at 21:11

1 Answer 1

Reset to default
2
$\begingroup$

We have a canonical map in one direction, namely $f^*(W(p)) \to W(f^*(p))$, but this map can fail to be an isomorphism. Here is an explicit counterexample.

Let $X$ be the set of countably-brancing trees, so $X = W(p)$ where $p : \mathbb{N} \to \mathbf{2}$ is a constant map. A tree is either a leaf or a node with countably many children.

Let $f$ be the canonical geometric morphism from the classifying topos $\mathcal{E}$ of enumerations of $X$ to $\mathrm{Set}$. (Incidentally, $f$ is surjective and open.)

As the definition of $p$ uses only geometric constructions, $f^*(p)$ is again a constant map $\mathbb{N} \to \mathbf{2}$. So $W(f^*(p))$ is again the set of countably-branching trees, just in $\mathcal{E}$ instead of $\mathrm{Set}$.

But $f^*(X)$ does not coincide with $W(f^*(p))$: As internally in $\mathcal{E}$ there is an enumeration of all elements of $f^*(X)$, we can build a certrain tree, an element of $f^*(X)$, which has all elements of $f^*(X)$ as children. Hence $f^*(X)$ contains an infinite path and is thus not well-founded.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .