A set of notes that I once wrote:
Quantization via Linear Homotopy Types
on the formalization of Motivic quantization of local prequantum field theory in the formal framework of dependent linear homotopy type theory, with application to the archetypical example of extended geometric quantization of 2d Chern-Simons theory.
To go along with talks I gave on the following occasions:
Gabriel Catren et al. (org.) Philosophy of Mechanics: Mathematical Foundations, Workshop Feb 12-14, 2014 (website, poster)
J. Fuchs, L. Katzarkov, N. Reshetikhin, C. Schweigert (org.) Modern Trends in Topological Quantum Field Theory, Workshop at Erwin-Schrödinger Institute Vienna, February 17 - 21, 2013 (pdf schedule)
Motivic quantization of local prequantum field theory
at GAP XI, Pittsburgh, August 2013 (website)
String Geometry Network meeting at Erwin-Schrödinger Institute Vienna, Feb 24-28 2014 (website)
Oberwolfach Workshop 1651a: New interactions between homotopical algebra and quantum field theory, Dec 2016
Related talks:
What, and for what is Higher geometric quantization, talk at Workshop on Higher Gauge Theory and Higher Quantization, Edinburgh, 25-26 June 2014; and at Symmetries and correspondences in number theory, geometry, algebra, physics: intra-disciplinary trends, Oxford, July 5-8 2014
Correspondences of cohesive linear homotopy types and Quantization,talk at Symmetries and correspondences: instra-disciplinary trends, Oxford, July 5-8 2014
This is a companion of
Followup articles:
See also:
Related talks:
We discuss in the foundational logical framework of homotopy-type theory a natural formalization of secondary integral kernels in geometric stable homotopy theory. We observe that this yields a process of non-perturbative cohomological quantization of local prequantum field theory. We show that quantum anomaly cancellation amounts to realizing this as the boundary of a field theory that is given by genuine (primary) integral transforms. Recalling that traditional linear logic has categorical semantics in symmetric monoidal categories, such as that of Hilbert spaces, and hence serves to axiomatize quantum mechanics, e.g. Pratt (1992), Abramsky-Duncan (2005), Duncan (2006), what we consider is its refinement to linear homotopy-type theory which has categorical semantics in stable ∞-categories of bundles of stable homotopy-types, hence of generalized cohomology theories. We discuss how this provides a natural formalization of geometric quantization of local prequantum field theory, following (dcct, Nuiten (2013)) and closely related to Hopkins-Lurie (2014).
For the reader interested in technical problems of quantization we discuss how this formalization informs the discussion of quantum anomaly cancellation. For the reader inclined to the interpretation of quantum mechanics we exhibit quantum superposition and quantum interference as existential quantification in linear homotopy-type theory. For the reader inclined to ontological philosophy we provide a modal homotopy-type theory formalizing Hegelian metaphysics (Hegel (1812)) in refinement of the proposal in Lawvere (1991), Lawvere (1994) for a formal foundations of physics, Lawvere (1986), Lawvere (1997), lifted from classical mechanics to local quantum gauge field theory (Sch (2013c)).
The axiomatic characterization of local quantum field theory (QFT) on spacetimes/worldvolumes of arbitrary topology (see here for a review) had been completed in (Lurie 09) via a universal construction in monoidal higher category theory. While in the “bulk” of the worldvolume this describes topological QFT, the axiomatization also captures defects (domain walls) and boundaries (branes) and the corresponding boundary field theories may be geometric (non-topological) (dcct). Notably ordinary quantum mechanics is a boundary field theory of a 2d Poisson-Chern-Simons theory TQFT in this way (Nuiten 13, Bongers 13).
But modern quantum physics is more than quantum mechanics, and the quantum field theories of interest both in nature and in theory are not random examples of the axioms of local QFT, instead they arise via a process of “quantization” from geometric data. An axiomatic characterization also of pre-quantum data and of the quantization step has been proposed and studied in (dcct, Nuiten 13). This may be naturally formalized entirely in type theory – in its dependent and intensional flavor called homotopy type theory.
This note here gives a brief survey of the key aspects of quantization axiomatized in homotopy type theory this way.
The process is naturally divided into two stages: first, pre-quantum geometry (phase spaces and local Lagrangians) is naturally axiomatized in cohesive homotopy type theory (ScSh 12); second, quantization (geometric quantization and path integral quantization, in fact we find a subtle mix of both) is naturally axiomatized in linear homotopy type theory. The first step has been discussed in detail in (dcct, ScSh 12), see Classical field theory via Cohesive homotopy types for a quick exposition. The second step is worked out in various key examples in (Nuiten 13). There however the type-theoretic formalization is not discussed. The present note essentially points out how the quantization process in section 4 of (Nuiten 13) has a natural abstract formalization in linear homotopy type theory.
While we produced this note the preprint
appeared, which in its section 4.1 considers a special case of the abstract integral kernels of section 4.3 in the above note (namely the case of vanishing twist and realized in the model of local systems of stable homotopy types). This development seems to be motivated from serving as a building block in making precise the quantization prescription inducated in sections 3 and 8 of
differential cohomology in a cohesive topos
Synthetic Quantum Field Theory
Type-semantics for quantization
Last revised on May 30, 2024 at 12:11:38. See the history of this page for a list of all contributions to it.
