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. • CommentRowNumber101.
   • CommentAuthorUrs
   • CommentTimeMar 1st 2014
   • (edited Mar 1st 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexRight, elsewhere (at _[[order-theoretic structure in quantum mechanics]]_) I had emphasized the observation that the foundational theorems in quantum mechanics taken all together show that the idea that quantum observables form a [[Bohr topos]] -- the glorified incarnation of the Jordan algebra of observables -- is, essentially not a speculation but a derivable fact. Now in the discussion of "quantization via linear homotopy-type theory" I have been adopting alltogether the "dual" perspective (in the sense that Bohr toposophy is [[Heisenberg picture]] where quantum logic as linear type theory is [[Schrödinger picture]]). I don't know yet how these two "pcictures" eventually want to merge to a single whole. We had talked about this issue once before, when we were discussing "[[coordination]]" (I am providing links just for completeness for eventual bystanders). There I had speculated that the issue is the following: suppose you manage to form the full extended quantization of 3d CS in $tmf Mod_4$. Then it ends up producing for you statements such as "the space of states on this manifold here is this tmf-$k$-module". This raises a clear coordination issue: what does that _mean physically_? We know by inspection how to do this coordination in some cases (e.g. an element of a $tmf$-1-module may be regarded as a Witten genus, hence as a partition function of a string). But we (well, me) don't know how to "coordinate" systematically and generally. Maybe Bohr toposophy is telling us that we should figure out to assign some kind of topos to any $E$-$k$-module such that the internal logic of this topos is the logic of statements about the universe of quantum states that make up this $E$-$k$-module. But this is just a vague hunch. I have no idea at the moment about how to make this more concrete.

   Right, elsewhere (at order-theoretic structure in quantum mechanics) I had emphasized the observation that the foundational theorems in quantum mechanics taken all together show that the idea that quantum observables form a Bohr topos – the glorified incarnation of the Jordan algebra of observables – is, essentially not a speculation but a derivable fact.

   Now in the discussion of “quantization via linear homotopy-type theory” I have been adopting alltogether the “dual” perspective (in the sense that Bohr toposophy is Heisenberg picture where quantum logic as linear type theory is Schrödinger picture).

   I don’t know yet how these two “pcictures” eventually want to merge to a single whole.

   We had talked about this issue once before, when we were discussing “coordination” (I am providing links just for completeness for eventual bystanders). There I had speculated that the issue is the following:

   suppose you manage to form the full extended quantization of 3d CS in $tmf Mod_4$. Then it ends up producing for you statements such as “the space of states on this manifold here is this tmf-$k$-module”. This raises a clear coordination issue: what does that mean physically?

   We know by inspection how to do this coordination in some cases (e.g. an element of a $tmf$-1-module may be regarded as a Witten genus, hence as a partition function of a string). But we (well, me) don’t know how to “coordinate” systematically and generally.

   Maybe Bohr toposophy is telling us that we should figure out to assign some kind of topos to any $E$-$k$-module such that the internal logic of this topos is the logic of statements about the universe of quantum states that make up this $E$-$k$-module.

   But this is just a vague hunch. I have no idea at the moment about how to make this more concrete.

2. • CommentRowNumber102.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 14th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexMellies makes a big deal about the factorization of ! in linear logic in his [Categorical Semantics of Linear Logic](http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf), e.g., >One lesson of categorical semantics is that the exponential modality of linear logic should be described as an adjunction, rather than as a comonad. The observation is not simply technical: it has also a deep effect upon the way we understand logic in the wider sense...This refined decomposition requires to think differently about proofs, and to accept the idea that >**logic is polychrome, not monochrome** >this meaning that several universes of discourse (in this case, the categories L and M) generally coexist in logic, and that the purpose of a proof is precisely to intertwine these various universes by applying back and forth modalities (in this case, the functors L and M). In this account of logic, each universe of discourse implements its own body of internal laws. Typically, in the case of linear logic, the category M is cartesian in order to interpret the structural rules (weakening and contraction) while the category L is symmetric monoidal closed, or ∗-autonomous, in order to interpret the logical rules. In view of #56 $$ ! Z = \Sigma_+^\infty \Omega^\infty Z : \mathbf{H} \to Mod(\ast), $$ could we have a similarly florid description of what's going on? Does something like that distinction between structural and logical rules persist?

   Mellies makes a big deal about the factorization of ! in linear logic in his Categorical Semantics of Linear Logic, e.g.,

   One lesson of categorical semantics is that the exponential modality of linear logic should be described as an adjunction, rather than as a comonad. The observation is not simply technical: it has also a deep effect upon the way we understand logic in the wider sense…This refined decomposition requires to think differently about proofs, and to accept the idea that

   logic is polychrome, not monochrome

   this meaning that several universes of discourse (in this case, the categories L and M) generally coexist in logic, and that the purpose of a proof is precisely to intertwine these various universes by applying back and forth modalities (in this case, the functors L and M). In this account of logic, each universe of discourse implements its own body of internal laws. Typically, in the case of linear logic, the category M is cartesian in order to interpret the structural rules (weakening and contraction) while the category L is symmetric monoidal closed, or ∗-autonomous, in order to interpret the logical rules.

   In view of #56

   $$! Z = \Sigma_+^\infty \Omega^\infty Z : \mathbf{H} \to Mod(\ast),$$

   could we have a similarly florid description of what’s going on? Does something like that distinction between structural and logical rules persist?

3. • CommentRowNumber103.
   • CommentAuthorUrs
   • CommentTimeMar 14th 2014
   • (edited Mar 14th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexFirst of all it was Mike who emphasized that once we talk about _dependent_ linear type theory then this adjunction arises canonically. In dependent linear type theory there are already two "universes of discourse": the intuitionistic logic of the base types and the linear logic of the linear types parameterized over them. The adjunction that gives the exponential modality is just one small aspect of this more general "interplay of two universes". Then of course in the application to cohomological quantization we find very naturally familar names for these "universes of discourse": that of the cartesian base category is the discourse of pre-quantum ("classical") geometry/physics, whereas the other one is that of quantum geometry/physics. The fact that one is parameterized over the other is really the content of geometric quantization.

   First of all it was Mike who emphasized that once we talk about dependent linear type theory then this adjunction arises canonically. In dependent linear type theory there are already two “universes of discourse”: the intuitionistic logic of the base types and the linear logic of the linear types parameterized over them. The adjunction that gives the exponential modality is just one small aspect of this more general “interplay of two universes”.

   Then of course in the application to cohomological quantization we find very naturally familar names for these “universes of discourse”: that of the cartesian base category is the discourse of pre-quantum (“classical”) geometry/physics, whereas the other one is that of quantum geometry/physics. The fact that one is parameterized over the other is really the content of geometric quantization.

4. • CommentRowNumber104.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 15th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSo we could still say something of Mellies' structural/logical split persists - weakening and contraction available in the classical world, logical rules as linear operators in the quantum world? Hmm, or does the shift to dependent type theory muddle things up? I guess there's type formation and term intro/elim/computation going on in the base and in the linear fibres.

   So we could still say something of Mellies’ structural/logical split persists - weakening and contraction available in the classical world, logical rules as linear operators in the quantum world?

   Hmm, or does the shift to dependent type theory muddle things up? I guess there’s type formation and term intro/elim/computation going on in the base and in the linear fibres.

5. • CommentRowNumber105.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 19th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIs * [[David Gepner]], [[Rune Haugseng]], [[Joachim Kock]], _∞-Operads as Analytic Monads_, ([arXiv:1712.06469](https://arxiv.org/abs/1712.06469)) what became of that forthcoming paper, Gepner, D. and J. Kock, Polynomial functors over infinity categories, mentioned in #76? I guess at the time I was wondering if it might be useful for [Quantization via Linear homotopy types](https://arxiv.org/abs/1402.7041). Was def 3.20 the first appearance of the $\infty$-version of polynomial functor?

   Is

   • David Gepner, Rune Haugseng, Joachim Kock, ∞-Operads as Analytic Monads, (arXiv:1712.06469)

   what became of that forthcoming paper, Gepner, D. and J. Kock, Polynomial functors over infinity categories, mentioned in #76?

   I guess at the time I was wondering if it might be useful for Quantization via Linear homotopy types. Was def 3.20 the first appearance of the $\infty$-version of polynomial functor?

6. • CommentRowNumber106.
   • CommentAuthorUrs
   • CommentTimeDec 20th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexI hadn't seen this reference. Best to add a pointer to it to a relevant entry!

   I hadn’t seen this reference. Best to add a pointer to it to a relevant entry!

7. • CommentRowNumber107.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 20th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI've added it to [[(infinity,1)-operad]]. I would also add to a suitable page on polynomial functors, but we've already reserved [[polynomial (∞,1)-functor]] for the Goodwillie version. This seems a recipe for confusion: >The notion of “polynomial functor” we consider here should not be confused with the notion of “polynomial functor” introduced by Eilenberg and Mac Lane and subsequently used in the study of functor homology, nor with the notion occurring in Goodwillie’s calculus of functors. Their version is a homotopified version of what we have as [[polynomial functor]]. They note: >The fundamental nature of these three operations is witnessed by the fact that they correspond precisely to substitution, dependent sums, and dependent products, the most basic building blocks of type theory [HoTT]. Not sure I'm up to cleaning out the Augean stables of mathematicians' naming conventions.

   I’ve added it to (infinity,1)-operad. I would also add to a suitable page on polynomial functors, but we’ve already reserved polynomial (∞,1)-functor for the Goodwillie version.

   This seems a recipe for confusion:

   The notion of “polynomial functor” we consider here should not be confused with the notion of “polynomial functor” introduced by Eilenberg and Mac Lane and subsequently used in the study of functor homology, nor with the notion occurring in Goodwillie’s calculus of functors.

   Their version is a homotopified version of what we have as polynomial functor. They note:

   The fundamental nature of these three operations is witnessed by the fact that they correspond precisely to substitution, dependent sums, and dependent products, the most basic building blocks of type theory [HoTT].

   Not sure I’m up to cleaning out the Augean stables of mathematicians’ naming conventions.

8. • CommentRowNumber108.
   • CommentAuthorMike Shulman
   • CommentTimeDec 20th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexUgh. I'm not familiar with the functor-homology version, does anyone know what that is? There's not much content at [[polynomial (∞,1)-functor]] currently, and the definition suggests that anything one might want to say about that kind of polynomial (∞,1)-functor could equally well be placed at [[n-excisive (∞,1)-functor]]. So could we take over [[polynomial (∞,1)-functor]] for this, aligning terminologically with our page [[polynomial functor]], and include a hatnote pointing the reader to [[n-excisive (∞,1)-functor]] or [[Goodwillie calculus]] if that's what they're after (like we already have at [[polynomial functor]])?

   Ugh. I’m not familiar with the functor-homology version, does anyone know what that is?

   There’s not much content at polynomial (∞,1)-functor currently, and the definition suggests that anything one might want to say about that kind of polynomial (∞,1)-functor could equally well be placed at n-excisive (∞,1)-functor. So could we take over polynomial (∞,1)-functor for this, aligning terminologically with our page polynomial functor, and include a hatnote pointing the reader to n-excisive (∞,1)-functor or Goodwillie calculus if that’s what they’re after (like we already have at polynomial functor)?

9. • CommentRowNumber109.
   • CommentAuthorUrs
   • CommentTimeDec 21st 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexSounds good to me!

   Sounds good to me!

10. • CommentRowNumber110.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 21st 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAnd we wouldn't then have to change the currently misleading link to 'polynomial (infinity,1)-functor' at [[polynomial functor]].

    And we wouldn’t then have to change the currently misleading link to ’polynomial (infinity,1)-functor’ at polynomial functor.

11. • CommentRowNumber111.
    • CommentAuthorMike Shulman
    • CommentTimeDec 21st 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOk, I did that.

    Ok, I did that.

12. • CommentRowNumber112.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 23rd 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #99 > In the KU-example above, for the particle on the boundary of the 2d PCS theory, the role of $A$ is played by tensoring with the prequantum line bundle of the boundary theory. Traditional geometric quantization is recovered here in the form that "the Hilbert space of quantum states of the particle is the 2-expectation value of its prequantum line bundle regarded as a boundary operator of the cobounding 2d PCS theory". >In the tmf-example above, for the string on the boundary of the 3d CS theory, the role of $A$ is similarly played by tensoring with the Kalb-Ramond B-field 2-bundle. Presumably this continues with something to do with the [[C-field]]. And what then if >the C-field is simply a cocycle in J- twisted Cohomotopy ?

    Re #99

    In the KU-example above, for the particle on the boundary of the 2d PCS theory, the role of $A$ is played by tensoring with the prequantum line bundle of the boundary theory. Traditional geometric quantization is recovered here in the form that “the Hilbert space of quantum states of the particle is the 2-expectation value of its prequantum line bundle regarded as a boundary operator of the cobounding 2d PCS theory”.

    In the tmf-example above, for the string on the boundary of the 3d CS theory, the role of $A$ is similarly played by tensoring with the Kalb-Ramond B-field 2-bundle.

    Presumably this continues with something to do with the C-field. And what then if

    the C-field is simply a cocycle in J- twisted Cohomotopy ?