Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 21st 2013
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAre W-types preserved by inverse image functors between pretoposes? Grothendieck toposes? Since the answer is yes for NNOs, I would guess the answer is yes. Or should I ask what sort of functors preserve W-types more generally? As a followup, does the proof that a Grothendieck topos has W-types use any strong axioms of set theory?

   Are W-types preserved by inverse image functors between pretoposes? Grothendieck toposes?

   Since the answer is yes for NNOs, I would guess the answer is yes.

   Or should I ask what sort of functors preserve W-types more generally?

   As a followup, does the proof that a Grothendieck topos has W-types use any strong axioms of set theory?

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 21st 2013
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAlso, what is the correct definition of a W-pretopos if we do not assume it is a Π-pretopos? Arbitrary polynomial.functors don't exist in that case.

   Also, what is the correct definition of a W-pretopos if we do not assume it is a Π-pretopos? Arbitrary polynomial.functors don’t exist in that case.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeApr 21st 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexWithout $\Pi$, even the definition of NNO needs to be relativised to slices, as discussed at [[natural numbers object#withparams]]. With that understanding, one can at least consider polynomial functors that are literally written as polynomials, such as $X \mapsto 1 + X$; this much is supported by a pretopos, certainly. At [[polynomial functor]], there is some talk about looking at polynomial functors defined by exponentiable morphisms even when those aren\'t all morphisms.

   Without $\Pi$, even the definition of NNO needs to be relativised to slices, as discussed at natural numbers object#withparams.

   With that understanding, one can at least consider polynomial functors that are literally written as polynomials, such as $X \mapsto 1 + X$; this much is supported by a pretopos, certainly. At polynomial functor, there is some talk about looking at polynomial functors defined by exponentiable morphisms even when those aren't all morphisms.

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 22nd 2013
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex> even the definition of NNO needs to be relativised to slices, ah, of course. But we _know_ that an NNO can be defined without local cartesian closedness, whereas the article [[pretopos]] very blithely defines a W-pretopos as having initial algebras for functors which, following the definition blindly, may not even exist.

   even the definition of NNO needs to be relativised to slices,

   ah, of course. But we know that an NNO can be defined without local cartesian closedness, whereas the article pretopos very blithely defines a W-pretopos as having initial algebras for functors which, following the definition blindly, may not even exist.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeApr 22nd 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYes; you\'ll notice that [[pretopos]] links to the nonexistent [[inductive object]] rather than to [[W-type]], and I was going to put something appropriate there, but then I realised that I didn\'t know exactly what that was, and then I never fixed it. (The link to [[polynomial endofunctor]] was also unfilled then, and only later did it get filled with the version appropriate only for $\Pi$-categories.) At the time, I thought that it was obvious what a polynomial endofunctor should be in an arbitrary pretopos, and then I realised that it wasn\'t. Actually, you won\'t notice what I said you would unless you look in the history, because I just changed the definition. Now a $W$-pretopos asks for all possible $W$-types, in the sense that every *exponentiable* morphism\'s corresponding polynomial endofunctor (locally, so in every slice category) has an initial object. (Then a $\Pi$-$W$-pretopos is simply a $\Pi$-pretopos that is also a $W$-pretopos.) But I am suspicious of this definition; it is like talking about a functor that preserves whatever finite limits exist, when what you really want is a flat functor. I have added a warning to the definition as well.

   Yes; you'll notice that pretopos links to the nonexistent inductive object rather than to W-type, and I was going to put something appropriate there, but then I realised that I didn't know exactly what that was, and then I never fixed it. (The link to polynomial endofunctor was also unfilled then, and only later did it get filled with the version appropriate only for $\Pi$-categories.) At the time, I thought that it was obvious what a polynomial endofunctor should be in an arbitrary pretopos, and then I realised that it wasn't.

   Actually, you won't notice what I said you would unless you look in the history, because I just changed the definition. Now a $W$-pretopos asks for all possible $W$-types, in the sense that every exponentiable morphism's corresponding polynomial endofunctor (locally, so in every slice category) has an initial object. (Then a $\Pi$-$W$-pretopos is simply a $\Pi$-pretopos that is also a $W$-pretopos.) But I am suspicious of this definition; it is like talking about a functor that preserves whatever finite limits exist, when what you really want is a flat functor. I have added a warning to the definition as well.

6. • CommentRowNumber6.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 22nd 2013
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI think I can, for the pretopos I am working with, show that I have initial algebras for all endofunctors which are literal polynomials. Is this sufficient to get W-types for polynomial functors arising from an exponentiable morphism?

   I think I can, for the pretopos I am working with, show that I have initial algebras for all endofunctors which are literal polynomials. Is this sufficient to get W-types for polynomial functors arising from an exponentiable morphism?

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeApr 22nd 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexNo, I don\'t think so; I am terrible at constructing counterexamples, but I don\'t see why it would work even in a $\Pi$-pretopos. Of course, it depends what you mean by a literal polynomial. If you allow $\coprod_{a\colon A} X^{B_a}$, when $A$ is an object and $B$ is an object of the slice category over $A$ that is (when viewed as a morphism in the ambient pretopos) exponentiable (so that the expression makes sense), then you\'ve got all $W$-types right there. But to my mind, that\'s not literal. Even so, what if $A$ is a set and $B$ is a family of exponentiable objects indexed by $A$? Then the expression is literal, but arguably it\'s not a literal *polynomial* unless $A$ is finite. But even allowing infinite sets, I don\'t see why every exponentiable morphism\'s polynomial endofunctor must follow. Conversely, if a pretopos, even a $\Pi$-pretopos, does have all $W$-types (or all $W$-types given by exponentiable morphisms), it does *not* follow that every set-indexed polynomial works, since the pretopos may not have all coproducts! These are the sorts of thoughts that kept me from writing down what I thought that a $W$-pretopos should be; the concept may only make the best sense in the context of a Grothendieck $\Pi$-pretopos. All this without considering whether $B$ should actually be a family of sets, rather than a family of exponentiable objects (and then, if infinite, things again might not exist).

   No, I don't think so; I am terrible at constructing counterexamples, but I don't see why it would work even in a $\Pi$-pretopos.

   Of course, it depends what you mean by a literal polynomial. If you allow $\coprod_{a\colon A} X^{B_a}$, when $A$ is an object and $B$ is an object of the slice category over $A$ that is (when viewed as a morphism in the ambient pretopos) exponentiable (so that the expression makes sense), then you've got all $W$-types right there. But to my mind, that's not literal.

   Even so, what if $A$ is a set and $B$ is a family of exponentiable objects indexed by $A$? Then the expression is literal, but arguably it's not a literal polynomial unless $A$ is finite. But even allowing infinite sets, I don't see why every exponentiable morphism's polynomial endofunctor must follow.

   Conversely, if a pretopos, even a $\Pi$-pretopos, does have all $W$-types (or all $W$-types given by exponentiable morphisms), it does not follow that every set-indexed polynomial works, since the pretopos may not have all coproducts! These are the sorts of thoughts that kept me from writing down what I thought that a $W$-pretopos should be; the concept may only make the best sense in the context of a Grothendieck $\Pi$-pretopos.

   All this without considering whether $B$ should actually be a family of sets, rather than a family of exponentiable objects (and then, if infinite, things again might not exist).