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.

$\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$ 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$ Sep 21, 2015 at 21:11

1 Answer 1

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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