Schreiber Quantum gauge field theory in Cohesive homotopy type theory

A survey article that we have written:

• Urs Schreiber, Michael Shulman,

  Quantum Gauge Field Theory in Cohesive Homotopy Type Theory

  (arXiv:1408.0054, Coq code)

  in

  Ross Duncan, Prakash Panangaden (eds.)

  Proceedings 9th Workshop on Quantum Physics and Logic, Brussels, Belgium, 10-12 October 2012

  EPTCS 158 (2014) 109-126

  arXiv:1407.8427

  doi:10.4204/EPTCS.158.8

on the synthetic axiomatization of classical field theory/prequantum field theory within homotopy type theory in a flavor with three higher modalities added: cohesive homotopy type theory.

The formalization of cohesive homotopy type theory discussed in the article has been implemented in the Coq proof management system by Mike Shulman, the source code is here: Coq source code.

Related material for further reading includes:

• A discussion with more emphasis on the differential cohomology hexagon which is axiomatized by cohesive homotopy type theory is in Differential generalized cohomology in Cohesive homotopy type theory.

• More discussion of genuine synthetic quantum field theory, is at Quantization via Linear homotopy types.

• For a survey of the general picture see at Synthetic Quantum Field Theory.

• For a more detailed exposition of the physics involved see the pdf-document at Classical field theory via Cohesive homotopy types.

Abstract

We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in gauge quantum field theory. This is a brief survey of work by the authors developed in detail elsewhere (Sh, Sc).

Related references

Expositions of the general idea are in

• Urs Schreiber, Prequantum physics in a cohesive topos, Talk at Quantum Physics and Logic 2011, (pdf)

• geometry of physics– The full story in a few formal words

Lecture notes on more aspects of physics with an eye towards string theory in the context of cohesive homotopy type theory is in

• Urs Schreiber, twisted smooth cohomology in string theory, Lectures at ESI program on K-theory and quantum fields

For further related references see at differential cohomology in a cohesive topos – References.

Related projects

• differential cohomology in a cohesive topos

  • Synthetic Quantum Field Theory

    • Quantum gauge field theory in Cohesive homotopy type theory

    • Type-semantics for quantization

  • cohomology

    • Principal ∞-bundles – models and general theory

    • Fivebrane structures

  • ∞-Chern-Weil theory

    • L-∞ algebra connections

    • Cech cocycles for differential characteristic classes

    • Twisted differential structures

      • Twisted Differential String and Fivebrane Structures

      • The moduli 3-stack of the C-field

  • ∞-Chern-Simons theory

    • A higher stacky perspective on Chern-Simons theory

    • Higher Chern-Weil Derivation of AKSZ Sigma-Models

    • 7d Chern-Simons theory and the 5-brane

    • Extended higher cup-product Chern-Simons theories

  • ∞-Wess-Zumino-Witten theory

    • The brane bouquet

    • Obstruction theory for parameterized higher WZW terms

  • Higher geometric prequantum theory

    • Classical field theory via Cohesive homotopy types

    • Local prequantum field theory

    • L-∞ algebras of local observables from higher prequantum bundles

    • Higher extensions of mapping class groups

  • Motivic quantization of local prequantum field theory

    • Geometric quantization of symplectic and Poisson manifolds

    • Cohomological quantization of local prequantum boundary field theory