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).
    • CommentRowNumber101.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2014
    • (edited Mar 1st 2014)

    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 tmfMod 4tmf Mod_4. Then it ends up producing for you statements such as “the space of states on this manifold here is this tmf-kk-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 tmftmf-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 EE-kk-module such that the internal logic of this topos is the logic of statements about the universe of quantum states that make up this EE-kk-module.

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

    • CommentRowNumber102.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2014

    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=Σ + Ω Z:HMod(*), ! 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?

    • CommentRowNumber103.
    • CommentAuthorUrs
    • CommentTimeMar 14th 2014
    • (edited Mar 14th 2014)

    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.

    • CommentRowNumber104.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 15th 2014

    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.

    • CommentRowNumber105.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 19th 2017

    Is

    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?

    • CommentRowNumber106.
    • CommentAuthorUrs
    • CommentTimeDec 20th 2017

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

    • CommentRowNumber107.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 20th 2017

    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.

    • CommentRowNumber108.
    • CommentAuthorMike Shulman
    • CommentTimeDec 20th 2017

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

    • CommentRowNumber109.
    • CommentAuthorUrs
    • CommentTimeDec 21st 2017

    Sounds good to me!

    • CommentRowNumber110.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 21st 2017

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

    • CommentRowNumber111.
    • CommentAuthorMike Shulman
    • CommentTimeDec 21st 2017

    Ok, I did that.

    • CommentRowNumber112.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 23rd 2022

    Re #99

    In the KU-example above, for the particle on the boundary of the 2d PCS theory, the role of AA 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 AA 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 ?