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 deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

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.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    The codiscrete objects in a cohesive (,1)(\infty,1)-topos, and the coreduced objects in a differentially cohesive one, are subtoposes, i.e. accessible left exact localizations. Are they (in the primary examples) topological localizations, in the sense of HTT 6.2.1?

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2014
    • (edited Nov 2nd 2014)

    In the Cahiers topos Sh({ n×Spec(W)} n,W)Sh(\{\mathbb{R}^n \times Spec(W)\}_{n,W}) the infinitesimal shape modality is localization at the morphisms ()×Spec(W)()(-) \times Spec(W)\to (-) that contract the infinitesimally thickened points away (WW ranging over “Weil algebras” W=finitedimensionalnilpotentidealW = \mathbb{R} \oplus finite\;dimensional\;nilpotent\;ideal). Regarding this as localization at the unique point inclusions ()()×Spec(W)(-) \hookrightarrow (-)\times Spec(W), all these are monomorphisms. So this should be a topological localization.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    Ok, so localization at a morphism that has a section is the same as localization at the section, and since Spec(W)Spec(W) is an hset, the inclusion of its point is a mono. Thanks!

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    Any thoughts about \sharp?

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2014
    • (edited Nov 2nd 2014)

    Hm, nothing that seems to lead to the conclusion of topological localization.

    Let’s see. I suppose \sharp is equivalent to localization at \flat-equivalences,which are the same as Γ\Gamma-equivalence (equivalences under global sections).

    Factoring Γ\Gamma-equivalences into 1-epis followed by 1-monos, we are left with having to show that localization at 1-epis that are Γ\Gamma-equivalences might be given by localization at monos.

    What could we do?

    Using a site of definition we know that the condition of 1-epi + Γ\Gamma-equivalence means that the morphism is an equivalence on points and an epi on stalks after 0-truncation. Is that enough to even build a retract, let alone show that it may be assumed 1-mono, without restriction of generality?

    I am a bit out of ideas here.

    (So probably you are after topological localization now because it simplifies some formalization, is that so?)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2014

    It occurred to me to wonder because in formalizing lex modalities, I’ve discovered the issue of universes requires a bit more care. In HoTT we can’t actually say “\bigcirc preserves finite limits” because it is a quantification over all types. We can quantify over all types in a particular universe, but that isn’t quite the same. I do know how (I think) to prove that an internal localization at a family of hprops is automatically lex, so that would be a “small” way of ensuring that a modality is lex; hence I wondered whether the modalities we care about are of that form, which is at least closely related to being topological. This is also what prompted this question.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014

    Thanks. I am following what you say about smallness, but I am momentarily confused about the motivation.

    Wasn’t the point that a modality phrased internally is automatically externally lex? We used to discuss the issue of how to get rid of this left exactness. Now you seem to want to get hold of it.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2014

    A reflective subuniverse phrased internally is automatically an exponential ideal, and a modality phrased internally automatically has stable units. Those are both left-exactness properties, but neither of them is as strong as full left exactness.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014

    I was thinking of this statement that a reflective factorization system is stable iff the reflector is lex.

    There is by now a plethora of different internal versions of the naive concept of reflection. Do you personally keep some map of the territory, or is it just all manifest to you by now?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    Ah, yes. The issue is that an internally defined modality is a stable factorization system, but it may not be a reflective one. Even though it is “determined by the class M/1M/1” in some way (internally; externally not even this is true), it’s not determined in the same way as a reflective FS: we define MM to be the maps with fibers in M/1M/1, and EE to be the maps whose reflection into M/1M/1 is trivial. This EE is pullback-stable, but in general not every map inverted in M/1M/1 lies in EE. Think of the nn-connected/truncated FS: a map is nn-connected if it is iso on π n\pi_{\le n} and surjective on π n+1\pi_{n+1}, whereas the first condition is enough for it to be inverted by nn-truncation.

    I have a pretty good picture of the landscape in my head by now, but unfortunately it isn’t written out very clearly anywhere. I’m hoping to write a nice exposition once I’ve got it all implemented in the new HoTT Coq library.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    The issue is that an internally defined modality is a stable factorization system, but it may not be a reflective one.

    Oh, okay, thanks. I don’t think about this often enough to remember all the fine print. But I should.

    I’m hoping to write a nice exposition once I’ve got it all implemented in the new HoTT Coq library.

    That sounds good. Am looking forward to that!

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2015

    I don’t remember whether I made this connection back in November, but I’m recording it here now for future reference. Over in that thread a day after this one, we concluded that at least for Sh(CartSp)Sh(CartSp), the codiscrete modality \sharp is localization at the maps Δ nR n\Delta \mathbb{R}^n \to R^n. Since these are all monomorphisms, \sharp should be a topological localization, answering the question asked at the beginning of this thread.

    Therefore, since it is also a Boolean and dense subtopos, by this result it also consists of the double-negation sheaves (by which in an \infty-context I mean the localization at the class of ¬¬\neg\neg-dense monos).