Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 definitions 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 19th 2011

    I added a comment to the end of the discussion at predicative mathematics to the effect that free small-colimit completions of toposes are examples of locally cartesian closed pretoposes that are generally not toposes.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 19th 2011
    • (edited Sep 19th 2011)

    In fact, there could be some interesting stability theorems here. For one, if C is a complete and cocomplete Π-pretopos, then we have an evident functor Δ:SetC and I believe

    • CΔ is also a complete and cocomplete Π-pretopos.

    (Note: it may be shown that CΔ, for C an -lextensive category, is the free small-coproduct completion of C.) Furthermore, if Eex denotes the ex/lex completion, then

    • Eex is a complete and cocomplete Π-pretopos if E is.

    One import of this is that the free small-colimit completion Colim(C), for C a complete and cocomplete Π-pretopos, is equivalent to (CΔ)ex, which by the above is also a complete and cocomplete Π-pretopos.

    Furthermore, I conjecture that the above stability theorems carry over to Π-W-pretoposes in place of Π-pretoposes. These constructions seem to give interesting ways of constructing lots of non-topos examples.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeSep 19th 2011

    Cool!

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 20th 2011

    If you have a left exact (or even pullback-preserving) comonad on a pretopos, is the category of coalgebras also a pretopos? Same question for Π-pretoposes.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 21st 2011
    • (edited Sep 21st 2011)

    My question in 4 is in fact an incredibly easy ’yes’ (on both counts). Well, certainly the pretopos part is: all the axioms of a pretopos are in terms of colimits and pullbacks. If G:EE is a pullback-preserving comonad, then the underlying functor U:CoalgGE preserves and reflects colimits and pullbacks, and this means that the pretopos axioms hold on CoalgG if they hold on E. Nothing could be simpler.

    (It makes me suspect that a very easy conceptual proof of the lex comonad theorem for toposes might be available if we ’define’ a topos to be a lex total category, which is not too far off from the truth for Grothendieck toposes.)

    The analogous result for Π-pretoposes is also pretty easy if you quote the result (say from the Elephant) that if E is locally cartesian closed, then so is CoalgG. (I am defining a Π-pretopos to be a cocomplete LCC pretopos; it is easy to see that a Π-pretopos is also complete.)

    I have been writing all this down on my web page here, including proofs of my assertions in 2 above (I haven’t tackled W-types yet). Some of it might be a bit clunky. But the basic upshot is that the free small-colimit cocompletion of a Π-pretopos is also a Π-pretopos (and almost never a topos). It bothers me though that all this is a bit abstract; I’m having trouble picturing the nature of these constructions.