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.
   • CommentAuthorMike Shulman
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe codiscrete objects in a cohesive $(\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?

   The codiscrete objects in a cohesive $(\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?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 2nd 2014
   • (edited Nov 2nd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexIn the [[Cahiers topos]] $Sh(\{\mathbb{R}^n \times Spec(W)\}_{n,W})$ the infinitesimal shape modality is localization at the morphisms $(-) \times Spec(W)\to (-)$ that contract the infinitesimally thickened points away ($W$ ranging over "Weil algebras" $W = \mathbb{R} \oplus finite\;dimensional\;nilpotent\;ideal$). Regarding this as localization at the unique point inclusions $(-) \hookrightarrow (-)\times Spec(W)$, all these are monomorphisms. So this should be a topological localization.

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

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOk, so localization at a morphism that has a section is the same as localization at the section, and since $Spec(W)$ is an hset, the inclusion of its point is a mono. Thanks!

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

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAny thoughts about $\sharp$?

   Any thoughts about $\sharp$?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeNov 2nd 2014
   • (edited Nov 2nd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, 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?)

   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?)

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIt 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](http://mathoverflow.net/questions/185980/a-small-definition-of-sub-%E2%88%9E-1-topoi).

   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.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks. 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI was thinking of [this statement](http://ncatlab.org/nlab/show/stable+factorization+system#StableReflectiveFactorizationSystems) 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?

   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?

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, 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/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 $M$ to be the maps with fibers in $M/1$, and $E$ to be the maps whose reflection into $M/1$ is trivial. This $E$ is pullback-stable, but in general not every map inverted in $M/1$ lies in $E$. Think of the $n$-connected/truncated FS: a map is $n$-connected if it is iso on $\pi_{\le n}$ and surjective on $\pi_{n+1}$, whereas the first condition is enough for it to be inverted by $n$-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.

    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/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 $M$ to be the maps with fibers in $M/1$, and $E$ to be the maps whose reflection into $M/1$ is trivial. This $E$ is pullback-stable, but in general not every map inverted in $M/1$ lies in $E$. Think of the $n$-connected/truncated FS: a map is $n$-connected if it is iso on $\pi_{\le n}$ and surjective on $\pi_{n+1}$, whereas the first condition is enough for it to be inverted by $n$-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.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItex> 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!

    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!

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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](http://nforum.ncatlab.org/discussion/6315/internal-definitions-of-cohesion/) a day after this one, we concluded that at least for $Sh(CartSp)$, the codiscrete modality $\sharp$ is localization at the maps $\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](http://ncatlab.org/nlab/show/double+negation#boolean_subtopos) 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).

    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)$, the codiscrete modality $\sharp$ is localization at the maps $\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).