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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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 sheaves 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.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 12th 2013
   • (edited Feb 12th 2013)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI have some questions for the experts out there. (1) Is the exact completion of a lex, locally small, well-powered category also well-powered? If not, what's a nice counterexample? (2) Is the following result known? If it is, is it obvious? "A locally small well-powered infinitary pretopos has all W-types." Unless I'm deceiving myself somewhere, I think I can prove this in a nice way. Also, the ambient set theory (referring to phrases like "locally small", "well-powered", etc.) can be ETCS: no replacement needed. I got to thinking about this after responding to Andrej Bauer at MO [here](http://mathoverflow.net/questions/121406/where-in-ordinary-math-do-we-need-unbounded-separation-and-replacement/121421#121421) on where the replacement axiom schema is used in "ordinary mathematics". I began writing out some details for (2) based on Paul Taylor's development of general recursion via well-founded coalgebras -- what I have is simple and could well be in the literature, but all I have at home is his book, which doesn't have the specific details I wrote out (which I might put on my web here a little later today). (3) Possibly related to question 1: what is the precise meaning of this statement [here](http://ncatlab.org/nlab/show/geometric+category#wellpoweredness_12): "A requirement of well-poweredness is also inconsistent with the spectrum of familial regularity and exactness." ?

   I have some questions for the experts out there.

   (1) Is the exact completion of a lex, locally small, well-powered category also well-powered? If not, what’s a nice counterexample?

   (2) Is the following result known? If it is, is it obvious? “A locally small well-powered infinitary pretopos has all W-types.” Unless I’m deceiving myself somewhere, I think I can prove this in a nice way. Also, the ambient set theory (referring to phrases like “locally small”, “well-powered”, etc.) can be ETCS: no replacement needed.

   I got to thinking about this after responding to Andrej Bauer at MO here on where the replacement axiom schema is used in “ordinary mathematics”. I began writing out some details for (2) based on Paul Taylor’s development of general recursion via well-founded coalgebras – what I have is simple and could well be in the literature, but all I have at home is his book, which doesn’t have the specific details I wrote out (which I might put on my web here a little later today).

   (3) Possibly related to question 1: what is the precise meaning of this statement here: “A requirement of well-poweredness is also inconsistent with the spectrum of familial regularity and exactness.” ?

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 12th 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexRe question (1): shame on me. There are comments on this in [[regular and exact completions]], and counterexamples aplenty (e.g., in Menni's thesis). I suppose an answer to (3) might be just that: that taking the ex/lex completion (for example) does not preserve the property of well-poweredness.

   Re question (1): shame on me. There are comments on this in regular and exact completions, and counterexamples aplenty (e.g., in Menni’s thesis). I suppose an answer to (3) might be just that: that taking the ex/lex completion (for example) does not preserve the property of well-poweredness.

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeFeb 13th 2013
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexRegarding (2) - can it be stated more generally about "geometric morphisms" over a base topos? Can we even consider a(n infinitary) pretopos over a base topos? Regardless, this would be a nice result!

   Regarding (2) - can it be stated more generally about “geometric morphisms” over a base topos? Can we even consider a(n infinitary) pretopos over a base topos?

   Regardless, this would be a nice result!

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 14th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'd like to see (2) too! I don't think it's obvious to me, although I can imagine that some sort of adjoint-functory-thing might work. Regarding (3), I think what I meant (assuming I'm the one who wrote that, which seems likely) is that we don't require the subobject posets of a coherent category to be finite, or those of a regular category to be singletons, so why should we require those of a geometric category to be small?

   I’d like to see (2) too! I don’t think it’s obvious to me, although I can imagine that some sort of adjoint-functory-thing might work.

   Regarding (3), I think what I meant (assuming I’m the one who wrote that, which seems likely) is that we don’t require the subobject posets of a coherent category to be finite, or those of a regular category to be singletons, so why should we require those of a geometric category to be small?

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 14th 2013
   • (edited Feb 14th 2013)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks for responding, guys (and sorry for not responding sooner, David -- I'm still mulling over your comment). The theorem I'm asserting can be found [here](http://ncatlab.org/toddtrimble/show/Initial+algebras+and+terminal+coalgebras) (theorem 3, at the end). Actually, I think of this as just a sample or stopgap theorem: the techniques that lead up to it should be thought of as both simple and robust, meaning that with a little more thought, I think it should be possible to prove variants that don't require well-poweredness assumptions. But I'm still thinking this over.

   Thanks for responding, guys (and sorry for not responding sooner, David – I’m still mulling over your comment).

   The theorem I’m asserting can be found here (theorem 3, at the end). Actually, I think of this as just a sample or stopgap theorem: the techniques that lead up to it should be thought of as both simple and robust, meaning that with a little more thought, I think it should be possible to prove variants that don’t require well-poweredness assumptions. But I’m still thinking this over.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 14th 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOh dear, that link I gave requires my password. Sorry! Try [this](http://ncatlab.org/toddtrimble/published/Initial+algebras+and+terminal+coalgebras) instead.

   Oh dear, that link I gave requires my password. Sorry! Try this instead.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 22nd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexUnfortunately, I don't have time to read it carefully right now, but this looks very nice! Is local cartesian closure only used in Theorem 2 to conclude that colimits are stable under pullback? If so, then being an infinitary pretopos ought to also suffice for that. Do we know any examples of well-powered infinitary $\Pi$-pretoposes that are not Grothendieck toposes?

   Unfortunately, I don’t have time to read it carefully right now, but this looks very nice! Is local cartesian closure only used in Theorem 2 to conclude that colimits are stable under pullback? If so, then being an infinitary pretopos ought to also suffice for that.

   Do we know any examples of well-powered infinitary $\Pi$-pretoposes that are not Grothendieck toposes?

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 22nd 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexMike, thanks for having a look! And thanks for your observation about infinitary pretoposes. For some reason I thought I had (as of a few days ago) several examples, but one example of a well-powered infinitary $\Pi$-pretopos that is not a Grothendieck topos is the small colimit completion of $Set$. This is also the exact completion of the arrow category $Set^\to$ that I mentioned recently at [[generic proof]]. I'm thinking that there ought to be more such small colimit completion examples.

   Mike, thanks for having a look! And thanks for your observation about infinitary pretoposes.

   For some reason I thought I had (as of a few days ago) several examples, but one example of a well-powered infinitary $\Pi$-pretopos that is not a Grothendieck topos is the small colimit completion of $Set$. This is also the exact completion of the arrow category $Set^\to$ that I mentioned recently at generic proof. I’m thinking that there ought to be more such small colimit completion examples.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 22nd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe small colimit completion of $Set$ is equivalent to the exact completion of $Set^{\to}$??

   The small colimit completion of $Set$ is equivalent to the exact completion of $Set^{\to}$??

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, I believe so. The small colimit completion of a left exact category is equivalent to the exact completion of its small coproduct completion (see Rosicky, [Cartesian closed exact completions](http://www.sciencedirect.com/science/journal/00224049/142/3), lemma 3 on page 264), and the small coproduct completion of $Set$ can be identified with the arrow category $Set^\to$ (in general, if $E$ is a Grothendieck topos and $\Delta: Set \to E$ is left adjoint to the global sections functor $E \to Set$, then the small coproduct completion of $E$ can be identified with $E \downarrow \Delta$).

    Yes, I believe so. The small colimit completion of a left exact category is equivalent to the exact completion of its small coproduct completion (see Rosicky, Cartesian closed exact completions, lemma 3 on page 264), and the small coproduct completion of $Set$ can be identified with the arrow category $Set^\to$ (in general, if $E$ is a Grothendieck topos and $\Delta: Set \to E$ is left adjoint to the global sections functor $E \to Set$, then the small coproduct completion of $E$ can be identified with $E \downarrow \Delta$).

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, of course! The exact completion of any infinitary $\Pi$-pretopos is again such, right? So what remains is to verify well-poweredness, which seems to be some sort of AC-like condition on the category we start from.

    Ah, of course!

    The exact completion of any infinitary $\Pi$-pretopos is again such, right? So what remains is to verify well-poweredness, which seems to be some sort of AC-like condition on the category we start from.

12. • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, that's right. I am sort of interested in choice-like criteria for well-foundedness as part of one set of hypotheses to conclude the existence of $W$-types (as in this theorem 3), but I'm also open to other options. For example, maybe one could entertain the hypothesis that the infinitary $\Pi$-pretopos has large-complete subobject lattices? Any interesting examples there? Don't know; still mulling it over.

    Yes, that’s right. I am sort of interested in choice-like criteria for well-foundedness as part of one set of hypotheses to conclude the existence of $W$-types (as in this theorem 3), but I’m also open to other options. For example, maybe one could entertain the hypothesis that the infinitary $\Pi$-pretopos has large-complete subobject lattices? Any interesting examples there? Don’t know; still mulling it over.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 23rd 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe "usual" example I think of of a category with large-complete subobject lattices is quasitopological spaces. But it's not a pretopos. Hmm, our page on [[quasi-topological space]] doesn't seem quite right to me -- I thought they were the *small-set-valued* concrete sheaves on the large site of compact Hausdorff spaces, hence not obviously a quasitopos.

    The “usual” example I think of of a category with large-complete subobject lattices is quasitopological spaces. But it’s not a pretopos.

    Hmm, our page on quasi-topological space doesn’t seem quite right to me – I thought they were the small-set-valued concrete sheaves on the large site of compact Hausdorff spaces, hence not obviously a quasitopos.

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 23rd 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexHm, I seem to have been the culprit (?) on [[quasi-topological space]], and my memory is that I had trouble accessing a good reference from where I sit at my computer, and was going by my memory/seat of my pants. But if I understand your objection, it's not in how the notion was defined on the page, but rather with how the assertion of being a quasitopos was airily concluded. There is a brief paragraph on quasi-topological spaces in Wyler's Lecture Notes on Topoi and Quasitopoi, and he does say that they form a quasitopos. Which I am willing to believe, but I haven't gone through his argument (which requires some buildup) in detail.

    Hm, I seem to have been the culprit (?) on quasi-topological space, and my memory is that I had trouble accessing a good reference from where I sit at my computer, and was going by my memory/seat of my pants. But if I understand your objection, it’s not in how the notion was defined on the page, but rather with how the assertion of being a quasitopos was airily concluded.

    There is a brief paragraph on quasi-topological spaces in Wyler’s Lecture Notes on Topoi and Quasitopoi, and he does say that they form a quasitopos. Which I am willing to believe, but I haven’t gone through his argument (which requires some buildup) in detail.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 25th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOk -- I've made the assertion a little less airy. (-:

    Ok – I’ve made the assertion a little less airy. (-:

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 4th 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #15: thanks, Mike! Incidentally, can you tell me where it is proved that subobject lattices in the category of quasi-topological spaces are large-complete? Anything freely available online?

    Re #15: thanks, Mike!

    Incidentally, can you tell me where it is proved that subobject lattices in the category of quasi-topological spaces are large-complete? Anything freely available online?

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMar 5th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHmm, I thought it was fairly easy, since they have [[initial structures]] and final structures over Set.

    Hmm, I thought it was fairly easy, since they have initial structures and final structures over Set.