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

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMar 15th 2019
   • (edited Mar 15th 2019)
   • PermaLink
   Author: Urs
   Format: MarkdownItexFelix Wellen has been thinking about the following, maybe somebody has further thoughts: Currently an open problem is to get an intrinsic construction of [[differential cohesion]], hence of the [[infinitesimal shape modality]] and/or the _smooth_ real line in some analogy to how Mike's real cohesion gets the [[shape modality]] from the topological real line constructed internally, in [arXiv:1509.07584](https://arxiv.org/abs/1509.07584). But if we take the base topos of the cohesion to be the Boolean $\not \not$-subtopos, so that $$ \sharp \; \simeq \;\not \not $$ (at least on 0-types?) then we may define infinitesimal disks to be the types $\mathbb{D}$ with $$ \sharp \mathbb{D} \simeq \ast $$ (as in "[[logical topology]]"). Then one could try to define $\Im$ as the localization at these $\mathbb{D}$. But also, the infinitesimal disks should know about the smooth real line. For instance the [[Kock-Lawvere axioms]] gives that for the first order 1d disk $\mathbb{D}^1(1)$ we have $[\mathbb{D}^1(1), \mathbb{D}^1(1)]^{\ast/} \simeq \mathbb{R} $, with the correct smooth real line on the right. So the collection of the $\mathbb{D}$-s, as above, should be enough to know the smooth $\mathbb{R}^1$, but I am not sure. If so, one could then declare the shape modality to be localization at this smooth $\mathbb{R}^1$. Maybe if all fits together, this construction could exhibit canonical [[differential cohesion]].

   Felix Wellen has been thinking about the following, maybe somebody has further thoughts:

   Currently an open problem is to get an intrinsic construction of differential cohesion, hence of the infinitesimal shape modality and/or the smooth real line in some analogy to how Mike’s real cohesion gets the shape modality from the topological real line constructed internally, in arXiv:1509.07584.

   But if we take the base topos of the cohesion to be the Boolean -subtopos, so that

   (at least on 0-types?) then we may define infinitesimal disks to be the types with

   (as in “logical topology”).

   Then one could try to define as the localization at these .

   But also, the infinitesimal disks should know about the smooth real line. For instance the Kock-Lawvere axioms gives that for the first order 1d disk we have , with the correct smooth real line on the right.

   So the collection of the -s, as above, should be enough to know the smooth , but I am not sure. If so, one could then declare the shape modality to be localization at this smooth .

   Maybe if all fits together, this construction could exhibit canonical differential cohesion.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMar 15th 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting thought. Of course there are obstacles to overcome, e.g. it's not clear that there are only a small number of such $\mathbb{D}$, or how to identify one of them to call $\mathbb{D}^1(1)$.

   Interesting thought. Of course there are obstacles to overcome, e.g. it’s not clear that there are only a small number of such , or how to identify one of them to call .

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMar 15th 2019
   • PermaLink
   Author: Urs
   Format: MarkdownItexSo Felix had this thought (if I may share this here) that the subobject of $Prop$ which is classified by $Prop \overset{\not \not}{\longrightarrow} Prop$ should be something like the universal formal disk, and that $\mathbb{R}$ should be the commutative part of its endomorphism ring. While I appreciate where he is headed, I don't see through this yet.

   So Felix had this thought (if I may share this here) that the subobject of which is classified by should be something like the universal formal disk, and that should be the commutative part of its endomorphism ring. While I appreciate where he is headed, I don’t see through this yet.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMar 17th 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexBTW, the equation $\sharp = \neg\neg$ only holds for (-1)-types (as it must, since $\neg\neg X$ is always a (-1)-type while $\sharp$ preserves $n$-types for all $n$). Also, I would expect that even in continuous $\infty$-groupoids, where there are no infinitesimals as such, there are still lots of (non-concrete) types $X$ with $\sharp X = \ast$.

   BTW, the equation only holds for (-1)-types (as it must, since is always a (-1)-type while preserves -types for all ). Also, I would expect that even in continuous -groupoids, where there are no infinitesimals as such, there are still lots of (non-concrete) types with .

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMar 17th 2019
   • PermaLink
   Author: Urs
   Format: MarkdownItex> BTW, the equation $\sharp = \neg\neg$ only holds for (-1)-types (as it must, since $\neg\neg X$ is always a (-1)-type while $\sharp$ preserves $n$-types for all $n$). Thanks, of course. I was misled by thinking about subtoposes labeled $J_\sharp = J_{\not \not}$, but of course that just means that $\sharp$ and $\not \not$ give the same Lawvere-Tierney operator. Still, I suppose it means we can _define_ $\sharp$ constructively in terms of $\not \not$, right? And all $\sharp$ corresponding to Boolean subtoposes should arise this way, I suppose. > I would expect that even in continuous $\infty$-groupoids, where there are no infinitesimals as such, there are still lots of (non-concrete) types $X$ with $\sharp X = \ast$. Hm, right. Maybe. Hm...

   BTW, the equation only holds for (-1)-types (as it must, since is always a (-1)-type while preserves -types for all ).

   Thanks, of course. I was misled by thinking about subtoposes labeled , but of course that just means that and give the same Lawvere-Tierney operator.

   Still, I suppose it means we can define constructively in terms of , right? And all corresponding to Boolean subtoposes should arise this way, I suppose.

   I would expect that even in continuous -groupoids, where there are no infinitesimals as such, there are still lots of (non-concrete) types with .

   Hm, right. Maybe. Hm…

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMar 17th 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> I suppose it means we can _define_ $\sharp$ constructively in terms of $\not \not$, right? Well, modulo hypercompletion. Assuming propositional resizing, we can nullify all the $\neg\neg$-closed propositions to yield a topological subtopos of double-negation sheaves, and $\sharp$ then coincides with this on all $n$-types for finite $n$ (8.13 in [BFP](https://arxiv.org/abs/1509.07584)). It's not immediately obvious that they coincide on untruncated types. But probably they do in the examples given that $\infty Gpd$ is hypercomplete? I haven't thought about this carefully. > And all $\sharp$ corresponding to Boolean subtoposes should arise this way, I suppose. Not all Boolean subtoposes are the double-negation sheaves, even in 1-topos theory. As a trivial case, the trivial subtopos is also Boolean.

   I suppose it means we can define constructively in terms of , right?

   Well, modulo hypercompletion. Assuming propositional resizing, we can nullify all the -closed propositions to yield a topological subtopos of double-negation sheaves, and then coincides with this on all -types for finite (8.13 in BFP). It’s not immediately obvious that they coincide on untruncated types. But probably they do in the examples given that is hypercomplete? I haven’t thought about this carefully.

   And all corresponding to Boolean subtoposes should arise this way, I suppose.

   Not all Boolean subtoposes are the double-negation sheaves, even in 1-topos theory. As a trivial case, the trivial subtopos is also Boolean.