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.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat can be said about that old mantra of Joyal's [TWF102](http://math.ucr.edu/home/baez/week102.html): > Really we should call the sphere spectrum the 'true integers' now that HoTT has appeared? The spheres are definable in HoTT, and suspensions (sec. 6.5 of HoTT book) work out as hoped. Then you can define a spectrum as a family of pointed types (3.2 of these [notes](https://www.cs.cmu.edu/~rwh/theses/cavallo.pdf)). But is it really in the [linear version](https://ncatlab.org/nlab/show/dependent+linear+type+theory#LinearHomotopyTypeTheory) that the sphere spectrum will find its natural home, where one could talk about initial rings? Time for some HISTs, higher inductive stable types, perhaps. Is linear HoTT in any kind of state to have Coq-style proofs occur yet?

   What can be said about that old mantra of Joyal’s TWF102:

   Really we should call the sphere spectrum the ’true integers’

   now that HoTT has appeared?

   The spheres are definable in HoTT, and suspensions (sec. 6.5 of HoTT book) work out as hoped. Then you can define a spectrum as a family of pointed types (3.2 of these notes).

   But is it really in the linear version that the sphere spectrum will find its natural home, where one could talk about initial rings? Time for some HISTs, higher inductive stable types, perhaps. Is linear HoTT in any kind of state to have Coq-style proofs occur yet?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhile basics of [[sequential spectra]] have been formalized in HoTT (ask Google, see for instance [Library HoTT.Spectra.Coinductive](https://hott.github.io/HoTT/coqdoc-html/HoTT.Spectra.Coinductive.html)) the concept of $E_\infty$-ring spectra involves an infinite tower of coherence laws and hence will run into the same problem that already the formalization of simplicial types runs into, just worse. Maybe there is a workaround via implementing a formalization of plain 1-monoids in [[highly structured spectra]] (especially [[symmetric spectra]] would lend themselves to type theoretic formalization, I suppose), but that would then not make real use of the hot nature of HoTT.

   While basics of sequential spectra have been formalized in HoTT (ask Google, see for instance Library HoTT.Spectra.Coinductive) the concept of $E_\infty$-ring spectra involves an infinite tower of coherence laws and hence will run into the same problem that already the formalization of simplicial types runs into, just worse.

   Maybe there is a workaround via implementing a formalization of plain 1-monoids in highly structured spectra (especially symmetric spectra would lend themselves to type theoretic formalization, I suppose), but that would then not make real use of the hot nature of HoTT.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see. Thanks.

   I see. Thanks.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAnother possibility is "S-cohesive HoTT", the internal language of the $\infty$-topos of parametrized spectra. It's not yet clear what the best axioms for that are, but Eric Finster told me about some good ideas last month at CMU. Still no characterization of the sphere spectrum though, rather putting it in axiomatically. Is there a purely $(\infty,1)$-categorical characterization of the sphere spectrum within the $(\infty,1)$-topos of parametrized spectra?

   Another possibility is “S-cohesive HoTT”, the internal language of the $\infty$-topos of parametrized spectra. It’s not yet clear what the best axioms for that are, but Eric Finster told me about some good ideas last month at CMU. Still no characterization of the sphere spectrum though, rather putting it in axiomatically. Is there a purely $(\infty,1)$-categorical characterization of the sphere spectrum within the $(\infty,1)$-topos of parametrized spectra?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexI should say that in #2 I was thinking of the sphere spectrum with its $E_\infty$-ring structure, since David was referring to the homotopy version of the integers. If we are content with the sphere spectrum as such, and if we allow ourselves to assume that we have available the dependent linear type theory of the tangent $\infty$-topos, then we should have available the $\Sigma_+^\infty \dashv \Omega^\infty$-adjunction as the interpretation of the "canonical exponential modality" induced on the linear type theory over the point in a dependent linear type theory.

   I should say that in #2 I was thinking of the sphere spectrum with its $E_\infty$-ring structure, since David was referring to the homotopy version of the integers.

   If we are content with the sphere spectrum as such, and if we allow ourselves to assume that we have available the dependent linear type theory of the tangent $\infty$-topos, then we should have available the $\Sigma_+^\infty \dashv \Omega^\infty$-adjunction as the interpretation of the “canonical exponential modality” induced on the linear type theory over the point in a dependent linear type theory.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThe external smash-product of parametrized spectra [arXiv:1310.5174](https://arxiv.org/abs/1310.5174) is just the $(\infty,1)$-topos product? So the sphere spectrum is the unit, I guess. >“S-cohesive HoTT” Is that likely the way to go, with internal languages for specific $(\infty,1)$-toposes?

   The external smash-product of parametrized spectra arXiv:1310.5174 is just the $(\infty,1)$-topos product? So the sphere spectrum is the unit, I guess.

   “S-cohesive HoTT”

   Is that likely the way to go, with internal languages for specific $(\infty,1)$-toposes?

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeApr 19th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexNo, the Cartesian product in the $\infty$-topos of parameterized spectra does not involve smashing. The good thing about the Cartesian product though is that the corresponding Cartesian internal hom knows about twisted cohomology: For $X$ a plain space, regarded as the 0-spectrum parameterized over it, and for $E \to B$ any parameterized spectrum, then the Cartesian internal hom $[X,E]$ is the parameterized spectrum whose base is the space of twists $[X,B]$, and whose fiber over a twist $\tau$ is the $\tau$-twisted $E$-cohomology of $X$. But it is still a bif weird: if $X$ itself carries a non-trivial parameterized spectrum, then this does not participate in the internal hom in a way that would make sense from the point of view of twisted cohomology

   No, the Cartesian product in the $\infty$-topos of parameterized spectra does not involve smashing. The good thing about the Cartesian product though is that the corresponding Cartesian internal hom knows about twisted cohomology:

   For $X$ a plain space, regarded as the 0-spectrum parameterized over it, and for $E \to B$ any parameterized spectrum, then the Cartesian internal hom $[X,E]$ is the parameterized spectrum whose base is the space of twists $[X,B]$, and whose fiber over a twist $\tau$ is the $\tau$-twisted $E$-cohomology of $X$.

   But it is still a bif weird: if $X$ itself carries a non-trivial parameterized spectrum, then this does not participate in the internal hom in a way that would make sense from the point of view of twisted cohomology

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeApr 19th 2017
   • (edited Apr 19th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSorry, my comment in #5 is a bit overkill. Of course if we have assume that dependent linear type theory, then the sphere spectrum is there more immediately, simply as the linear unit over the Cartesian unit.

   Sorry, my comment in #5 is a bit overkill. Of course if we have assume that dependent linear type theory, then the sphere spectrum is there more immediately, simply as the linear unit over the Cartesian unit.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeApr 20th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> Is that likely the way to go? It's not clear to me that the type of "ways to go" is contractible, so "the-introduction" may not apply. (-:

   Is that likely the way to go?

   It’s not clear to me that the type of “ways to go” is contractible, so “the-introduction” may not apply. (-:

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 20th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexTime to coin "the-elimination" too. Is there something more specific to S-cohesive HoTT than some linear-cohesive combination of HoTT? Why stop at parametrized spectra when there are all the higher [jets](https://ncatlab.org/nlab/show/jet+%28infinity%2C1%29-category) to be had? I seem to recall Urs saying that the cohesive and linear aspects would commute. Ah [here](https://nforum.ncatlab.org/discussion/5340/nexcisive-functor/?Focus=55633#Comment_55633), e.g., $$ \sharp \simeq \sharp_{smooth} \circ \sharp_{parameterized} \simeq \sharp_{parameterized} \circ \sharp_{smooth} \,. $$

    Time to coin “the-elimination” too.

    Is there something more specific to S-cohesive HoTT than some linear-cohesive combination of HoTT? Why stop at parametrized spectra when there are all the higher jets to be had?

    I seem to recall Urs saying that the cohesive and linear aspects would commute. Ah here, e.g.,

    $$\sharp \simeq \sharp_{smooth} \circ \sharp_{parameterized} \simeq \sharp_{parameterized} \circ \sharp_{smooth} \,.$$
11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeApr 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI expect jet-cohesive HoTT is also a thing.

    I expect jet-cohesive HoTT is also a thing.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 20th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOh yes, Eric's involved in that approach discussed [here](https://ncatlab.org/nlab/show/excisive+%28%E2%88%9E%2C1%29-functor#CharacterizationViaAGenericStableObject). Urs [glossed](https://nforum.ncatlab.org/discussion/6946/weiss-topology-and-goodwillie-calculus/?Focus=56173#Comment_56173) it in terms of "Let there be a pointed object!" and "Let all finite pointed powers of that pointed object be linear!"

    Oh yes, Eric’s involved in that approach discussed here. Urs glossed it in terms of “Let there be a pointed object!” and “Let all finite pointed powers of that pointed object be linear!”