Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userQuantum Gauge Field Theory in Cohesive Homotopy Type Theory
202
0
0.0
(
0
)
Authors
Urs Schreiber
Ask ChatGPT about the research
No Arabic 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 quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
rate research
Read More
We define in the setting of homotopy type theory an H-space structure on $mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $mathbb S^3hookrightarrowmathbb S^7twoheadrightarrowmathbb S^4$, using only homotopy invariant tools.
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a localization higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
Algebraic quantum field theory and prefactorization algebra are two mathematical approaches to quantum field theory. In this monograph, using a new coend definition of the Boardman-Vogt construction of a colored operad, we define homotopy algebraic quantum field theories and homotopy prefactorization algebras and investigate their homotopy coherent structures. Homotopy coherent diagrams, homotopy inverses, A-infinity-algebras, E-infinity-algebras, and E-infinity-modules arise naturally in this context. In particular, each homotopy algebraic quantum field theory has the structure of a homotopy coherent diagram of A-infinity-algebras and satisfies a homotopy coherent version of the causality axiom. When the time-slice axiom is defined for algebraic quantum field theory, a homotopy coherent version of the time-slice axiom is satisfied by each homotopy algebraic quantum field theory. Over each topological space, every homotopy prefactorization algebra has the structure of a homotopy coherent diagram of E-infinity-modules over an E-infinity-algebra. To compare the two approaches, we construct a comparison morphism from the colored operad for (homotopy) prefactorization algebras to the colored operad for (homotopy) algebraic quantum field theories and study the induced adjunctions on algebras.
We argue that notions in quantum theory should have universal properties in the sense of category theory. We consider the completely positive trace preserving (CPTP) maps, the basic notion of quantum channel. Physically, quantum channels are derived from pure quantum theory by allowing discarding. We phrase this in category theoretic terms by showing that the category of CPTP maps is the universal monoidal category with a terminal unit that has a functor from the category of isometries. In other words, the CPTP maps are the affine reflection of the isometries.
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental formalism of crisp variables. This yields type theories that we call spatial and cohesive, in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the fundamental $infty$-groupoid or shape), disentangling the identifications of Homotopy Type Theory from the continuous paths of topology. In a further refinement called real-cohesion, the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwers fixed-point theorem.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
