nLab geometry of physics

This page is growing incrementally as a series of lecture series proceeds.

Surveys, textbooks and lecture notes

Differential geometry

synthetic differential geometry

Introductions

from point-set topology to differentiable manifolds

Differentials

V-manifolds

smooth space

Tangency

The magic algebraic facts

Theorems

Axiomatics

cohesion

• (shape modality $\dashv$ flat modality $\dashv$ sharp modality)

$(\esh \dashv \flat \dashv \sharp )$

• dR-shape modality$\dashv$ dR-flat modality

$\esh_{dR} \dashv \flat_{dR}$

tangent cohesion

differential cohesion

singular cohesion

$\array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }$

Models

Lie theory, ∞-Lie theory

differential equations, variational calculus

Chern-Weil theory, ∞-Chern-Weil theory

Cartan geometry (super, higher)

A set of lecture notes on differential geometry and theoretical fundamental physics, combining an introduction to traditional notions with an exposition of their formulation and refinement by higher geometry and extended prequantum field theory. With an eye towards Hilbert's sixth problem approached via cohesion.

Divided into two parts:

$\,$

$\phantom{AA}$ physics $\phantom{AA}$$\phantom{AA}$ mathematics $\phantom{AA}$
$\phantom{AA}$ gauge principle $\phantom{AA}$$\phantom{AA}$ higher geometry $\phantom{AA}$
$\phantom{AA}$ (geometric homotopy theory) $\phantom{AA}$
$\phantom{AA}$ Pauli exclusion principle $\phantom{AA}$$\phantom{AA}$ supergeometry $\phantom{AA}$

Here:

1. Supergeometry is geometry whose spaces may have algebras of functions that are $\mathbb{Z}_2$-graded-commutative algebras. This is the mathematical reflection of the Pauli exclusion principle, which says that a fermionic wave function $\Psi$ on a phase space of a physical system with fermions has to have vanishing square. By linearity this implies that

\begin{aligned} 0 & = (\Psi_1 + \Psi_2)^2 \\ & = \underset{ = 0}{\underbrace{ (\Psi_1)^2 }} + \underset{ = 0}{\underbrace{ \Psi_1 \Psi_2 + \Psi_2 \Psi_1 }} + \underset{ = 0}{\underbrace{ (\Psi_2)^2 }} \end{aligned}

and hence that fermionic wave functions anti-commute, and hence are the odd-graded elements in a commutative superalgebra (a slightly noncommutative algebra!)

Ever since the existence of fermionic particles was experimentally established, around the time of the Stern-Gerlach experiment in the 1920s, it is thus an experimental fact that fundamental physics is described by supergeometry. (This is not necessarily super-symmetric, though of course there is a close relation.)

2. Higher structures is short for higher homotopy theoretic structures and reflects the gauge principle of physics: This says that, generally, it does not make invariant sense to ask if any two things $x$, $y$ (e.g. field histories) are equal, instead one must ask for a gauge transformation between them, mathematically a homotopy:

$x \stackrel{\gamma}{\longrightarrow} y$

This principle applies also to gauge transformations themselves, and thus leads to gauge-of-gauge transformations and so on to ever higher gauge transformations: mathematically reflected by higher homotopies in higher homotopy types.

Ever since the existence of gauge fields was understood in the 1920s, it is thus an experimental fact that fundamental physics is described by higher geometry.

A striking consequence is that, both in higher geometry as well as in supergeometry and therefore in the geometry of fundamental physics, spaces generally are not sets of points, as in the traditional definition of topological spaces or differentiable manifolds.

What, then, is the geometry of fundamental physics?

The right framework to answer questions like this has been urged by Alexander Grothendieck already in Grothendieck 73 (see Lawvere 03) and has been much expanded on by William Lawvere (e.g. Lawvere 97, Lawvere 91) and has an evident lift to higher geometry (Lurie 09, S. 13), but has remained somewhat of a “public secret”:

The answer is known, alternatively, as (higher) functorial geometry (Grothendieck) or synthetic differential geometry in gros toposes (Lawvere), or variants thereof.

In this lecture series we try to give a self-contained introduction to higher differential supergeometry this way, following Schreiber 13. We begin at the beginning, with introducing relevant basics of category theory and topos theory and will provide brief indication of real-world applications to perturbative quantum field theory and fundamental super p-branes.

The higher differential geometry which we lay out subsumes various special cases that are discussed separately in the literature:

geometries of physics

$\phantom{A}$(higher) geometry$\phantom{A}$$\phantom{A}$site$\phantom{A}$$\phantom{A}$sheaf topos$\phantom{A}$$\phantom{A}$∞-sheaf ∞-topos$\phantom{A}$
$\phantom{A}$discrete geometry$\phantom{A}$$\phantom{A}$Point$\phantom{A}$$\phantom{A}$Set$\phantom{A}$$\phantom{A}$Discrete∞Grpd$\phantom{A}$
$\phantom{A}$differential geometry$\phantom{A}$$\phantom{A}$CartSp$\phantom{A}$$\phantom{A}$SmoothSet$\phantom{A}$$\phantom{A}$Smooth∞Grpd$\phantom{A}$
$\phantom{A}$formal geometry$\phantom{A}$$\phantom{A}$FormalCartSp$\phantom{A}$$\phantom{A}$FormalSmoothSet$\phantom{A}$$\phantom{A}$FormalSmooth∞Grpd$\phantom{A}$
$\phantom{A}$supergeometry$\phantom{A}$$\phantom{A}$SuperFormalCartSp$\phantom{A}$$\phantom{A}$SuperFormalSmoothSet$\phantom{A}$$\phantom{A}$SuperFormalSmooth∞Grpd$\phantom{A}$

Notably diffeological spaces find home and company here: We explain how these are equivalently the concrete objects among the the bosonic smooth h-sets:

$\array{ \big\{ \text{diffeological spaces} \big\} \\ \;\simeq\; \\ \big\{ \text{concrete bosonic smooth h-sets} \big\} } \,.$

and we discuss how, even if one is initially interested only in ordinary smooth manifolds or only in diffeological spaces, it is useful to work with more general super differential homotopy types. graphics taken from Higher Prequantum Geometry

$\,$

$\,$

Contents

This page is going to contain an introduction to aspects of differential geometry and their application in fundamental physics: the gauge theory appearing in the standard model of particle physics and the Riemannian geometry appearing in the standard model of cosmology, as well as the symplectic geometry appearing in the quantization of both.

Scope and perspective

The intended topic scope and readership of the first layer of this page – the Model Layer – is much like that of the book (Frankel), only that here we make use of a more modern and more transparent conceptual toolbox. We also discuss in two other layers, the Semantic Layer and the Syntactic Layer deeper mechanisms at work in the background.

Notably, where traditional expositions of differential geometry proceed by generalizing the geometry of abstract coordinate systems $\mathbb{R}^n$ to smooth manifolds, here we instead begin by generalizing, in Smooth sets – Model Layer, coordinate systems right away to smooth sets, which happens to be both more expressive as well as actually much easier. In parallel (and to be read independently or not at all) we discuss in Smooth sets – Semantic Layer how this means that we are working in the sheaf topos over abstract coordinate systems. Smooth manifolds are then introduced later as an intermediate notion, together with that of diffeological spaces. (Many of the constructions in differential geometry applied in physics do not actually need the notion of a smooth manifold, and, more importantly, for many notions in modern theoretical physics smooth manifolds are not actually sufficiently general.)

In fact we introduce smooth manifolds only after we introduce smooth groupoids (below in Smooth homotopy type - Model Layer - Smooth groupoids), which are differential geometric structures that are still simpler than smooth manifolds, and of course even more expressive than smooth sets. Moreover, smooth groupoids are at the very heart of the geometry of physics: modern fundamental physics is all based on the “gauge principle” and in Model Layer – Gauge transformations in electromagnetism we explain how, mathematically, this is essentially nothing but the theory of smooth groupoids. As further background information we discuss in Smooth homotopy types - Semantic Layer how this means that we are working in a higher topos over abstract coordinate systems, and in Smooth homotopy type - Syntactic Layer how this means that we are reasoning about physics using the natural deduction rules of homotopy type theory.

From this setup then naturally flow all the many structures and phenomena seen in the geometry of physics:

Layers of exposition

We discuss each topic below in three stages, in three layers.

1. The first layer, called the Model Layer, deals with concrete explicit constructions as familiar from traditional textbooks on differential geometry and physics. This layer is supposed to be readable and useful all in itself and the reader who feels that this is all he or she wants to see can stick to this and ignore the other layers. In particular, while the Model Layer does invoke the basic notion of a category and of a functor – which are as simple as the notions of group or algebra –, it does not use any actual category theory.
1. The second layer, called the Semantic Layer, makes explicit the (higher) category theory and (higher) topos theory at work in the background. This puts the concrete constructions of the Model Layer into a more general context and helps to see certain organizational patterns that underlie the seemingly different phenomena. It provides some powerful theorems which the Model Layer is secretly benefitting from. For instance this layer gives a systematic rule for generalizing everything at the beginning Model Layers from ordinary differential geometry to what is called supergeometry, which is the context in which fermionic particles are formalized: the matter constituents of the observable universe.
1. The third layer, called the Syntactic Layer, makes explicit the expression of these phenomena in the formal internal language of the topos of smooth sets – which is dependent type theory – and of the higher topos of smooth higher groupoids – which is homotopy type theory. This makes more transparent various constructions in (higher) topos theory used in Semantic Layer, and in fact it provides a natural construction principle for objects in a (higher) topos that model some intended meaning – which is precisely what mathematical physics is all about. This is meant for readers who enjoy seeing fundamental physics naturally rooted in genuinely fundamental mathematics, in natural deduction from practical foundations, as it were. Everybody else should ignore this.

The three layers

This topos-theoretic perspective on fundamental physics which is discussed here is mostly original in the identifications it makes (Schreiber), but it draws insights and inspiration from (and maybe realizes) a vision already expressed since the 1960s by William Lawvere, one of the central figures in the development of topos theory and categorical logic. Lawvere links the very inception of topos theory to the motivation to axiomatize physics:

My own motivation $[$ for developing topos theory $]$ came from my earlier study of physics. The foundation of the continuum physics of general materials, $[...]$ involves powerful and clear physical ideas which unfortunately have been submerged under a mathematical apparatus including not only Cauchy sequences and countably additive measures, but also ad hoc choices of charts for manifolds and of inverse limits of Sobolev Hilbert spaces, to get at the simple nuclear spaces of intensively and extensively variable quantities. But, as Fichera lamented, all this apparatus may well be helpful in the solution of certain problems, but can the problems themselves and the needed axioms be stated in a direct and clear manner? And might this not lead to a simpler, equally rigorous account? (Lawvere, 2000)

More historical pointers along these lines and further related material can also be found at higher category theory and physics.

To give a survey of how the exposition below proceeds in the fashion of these three layers, the following section The full story in a few formal words provides what may be read as commented index to the central themes of the following text. Whereas the exposition below is organized to start each topic with the discussion of its concrete models in a Model layer, then pass to a general abstract semantics in a Semantic Layer and then finally to the abstract formal syntax in a Syntactic Layer, these tables indicates how this passage to abstract syntax usefully reflects back onto the concrete theory:

The leftmost columns of the following tables formulate concepts in terms of ordinary language. The second columns translate that ordinary language fairly directly to the formal language of (homotopy) type theory. The third columns then interprets these formal syntactical expressions as universal constructions in a (higher, cohesive) topos by the rules of categorical semantics. Finally, the fourth columns indicate what this universal construction amounts to when concretely realized in the model given by smooth sets and smooth ∞-groupoids. Finally the rightmost columns point to the chapters in the text below that deal with the given construction.

These tables show that fairly evident and naïve sounding statements in ordinary language turn under this translation into what is generally regarded as fairly sophisticated constructions. In fact some of these constructions have only been found by translating along the categorical semantics dictionary this way. So the following tables also serves to show how the general abstract discussion here is a means to facilitate reasoning about seemingly complicated concepts underlying fundamental physics:

The full story in a few formal words

We give an overview in the spirit of Synthetic Quantum Field Theory.

The fundamental physics of the observed world is governed by what is called quantum theory. (This is explicitly so for the standard model of particle physics and induced from this all fundamental physics ever tested in laboratories; but by all that is known also the remaining ingredient of gravity is fundamentally a quantum theory, see at quantum gravity for comments).

Two major axiomatizations of quantum theory are known, namely

1. FQFT where one axiomatizes the assignment of spaces of states to pieces of worldvolume (the “Schrödinger picture” of quantum theory)

fragments of which involve:

2. AQFT where one axiomatizes the assignment of algebras of observables to pieces of worldvolume (the “Heisenberg picture” of quantum theory)

fragments of which involve:

(For an attempt at a survey of the state of the art as of 2011 see the collection (Sati-Schreiber)).

But all fundamental quantum field theories observed in (or conjectured to underlie) nature arise by a process called quantization from structures in differential geometry (or are induced via a mechanism called the holographic principle from such that do).

This differential geometric data involves

Similar differential geometric structures are involved in the geometric quantization of such an action functional to an actual quantum field theory.

Hence there is a sequence:

differential geometry$\to$geometric quantization$\to$quantum field theory

We discuss a formalization of central aspects of this entire sequence. Our development proceeds – as befits a theory of physics and hence of nature – via natural deduction from practical foundations.

$\,$

Fundamentally, a language for physics is to be a language about existence; a language in which we can express judgements of the form:

There is a thing $x$ of type $X$.

For instance:

There is a gauge field $\nabla$ in the standard model $[X,\mathbf{B}\left(U\left(1\right)\times SU\left(2\right)\times SU\left(3\right)\right)_{conn}]$ of gauge fields on spacetime $X$.

(Here the square bracket expression for a moduli stack of gauge fields will be incrementally explained in the following.)

To be predictive, a language for physics is moreover to be a language in which we can make natural deductions to deduce further such judgements from given ones. For instance:

Given a gauge field $\nabla$ as above, there is an underlying instanton sector, $UnderlyingBundle(\nabla)$, in the collection $\left[X,\mathbf{B}\left(U\left(1\right)\times SU\left(2\right)\times SU\left(3\right)\right)\right]$ of instanton configurations in the standard model.

Quantum superpositions of such Yang-Mills instantons are the very substrate out of which the vacuum of the observed world is build: the instanton liquid in quantum chromodynamics. (For more see at Yang-Mills theory below.) We consider here a language to reason about such phenomena formally.

The formal language for such natural deduction of judgements about there being terms of some type is called type theory.

Expressions in (dependent) type theory:

(read columns 1+2 first, then 3+4)

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
There is…$\vdash \ldots$(We speak in the context of a (higher) topos $\mathbf{H}$, a place where things may be. (For the time being a (higher) locally cartesian closed category is sufficient.))(A topos for synthetic differential geometry, such as $\mathbf{H} =$ Sh$($SmthMfd$)$. Eventually a higher such topos: $\mathbf{H} =$ Smooth∞Grpd or SynthDiff∞Grpd or SmoothSuper∞Grpd or …)Smooth sets and Smooth homotopy types
There is a thing $x$ of type $X$.$\vdash\; x \colon X$An element $\left(* \stackrel{x}{\to} X\right) \in Mor(\mathbf{H})$ of an object $X$ of $\mathbf{H}$.A point $x$ in a smooth moduli stack $X$.Judgements about types and terms
There is a type $X$ of things $x$.$\vdash\; X \colon Type$An element $(* \stackrel{\vdash X}{\to} Obj) \in Mor(\mathbf{H})$ of the small-object classifier $Obj$ of $\mathbf{H}$.A point in the moduli stack of all small moduli stacks.Judgements about types and terms
Given a thing $x$ of type $X$ there is a thing $a(x)$ of type $A(x).$$x \colon X\;\vdash\; a(x) \colon A(x)$An element of a morphism $(A \to X)$ $\left(\array{ X &&\stackrel{a}{\to}&& A \\ & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow_{} \\ && X }\right)$ in the slice topos $\mathbf{H}_{/X}$.An $X$-family in a moduli stack bundle $A$ over $X$.Slice categories and Slice toposes and Slice ∞-Toposes
There is the collection of all things $a(x)$ for all $x$.$\vdash\; \left(\sum_{x \colon X} A\left(x\right)\right) \colon Type$The dependent sum/left adjoint to the product: $\array{ \mathbf{H}_{/X} &\stackrel{X_!}{\to} & \mathbf{H} \\ (A \to X) &\mapsto& A \in \mathbf{H}}$The total space of a bundle.Natural deduction rules for dependent sum types
There is a thing $t$ in the collection of all things $a(x)$ for all $x$.$\vdash\; t \colon \sum_{x \colon X} A(x)$An element $*\stackrel{t}{\to} A$ of the total space object.A point in the moduli stack $A$ over $X$.
There is an assignment $f$ of an $a(x)$ to each $x$.$\vdash \; f \colon \prod_{x \colon X} A(x)$.An element in the internal object of sections $* \stackrel{f}{\to} [X,A]_X$A point in the smooth relative mapping space of smooth sections.Natural deduction rules for dependent product types
There is the collection of assignments of an $a(x)$ to each $x$.$\vdash\; \left( \prod_{x \colon X} A\left(x\right) \right) \colon Type$internal space of sections $[X,A]_X \in \mathbf{H}$A smooth relative mapping space of smooth sections.
In particular, there is the collection of such assignments when $A$ does not depend on $x$, the collection of functions from $X$ to $A$.$\vdash \; \left(X \to A\right) \coloneqq \left(\prod_{x \colon X} A\right) \colon Type$The internal hom object $[X,A] \in \mathbf{H}$.A smooth mapping space.Smooth mapping spaces and smooth moduli spaces
There is a proof $p$ that it is true that there is $x$ of type $X$.$\vdash \; p \colon [X]$An element $* \stackrel{p}{\to}\tau_{-1}(X)$ of the (-1)-truncation of the object $X$.A point in the smooth sets of equivalence classes of points in $X$.Subobjects
There is a proof $p$ that it is true that there is an $a(x)$ for some $x$.$\vdash\; p \colon \left(\exists_{x \colon X} A\left(x\right) \right) \coloneqq \left[ \sum_{x \colon X} A\left(x\right)\right]$

In order to describe a structured reality, our language needs to be able to speak about comparison of things.

Fundamental physics rests on the gauge principle: it is meaningless to say that two things – such as two gauge fields $\nabla$ as above – are equal; instead they are gauge equivalent if there is a gauge transformation between them.

So our language needs to express judgements of the form:

There is a gauge equivalence between gauge fields $\nabla_1$ and $\nabla_2$.

And the language needs to be able to make natural deductions from such judgements to arrive at:

Given an equivalence $\lambda \colon \nabla_1 \simeq \nabla_2$ there is an equivalence $UnderlyingBundle(\lambda) \colon UnderlyingBundle(\nabla_1) \simeq UnderlyingBundle(\nabla_2)$ between the underlying instanton sectors.

The formal language based of the dependent type theory which we have so far that contains these statements is type theory with propositional equality. In this language we have judgements such as the following.

Expressions in dependent type theory with propositional equality:

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
Given $x,x'$, there is the collection of equivalences between $x$ and $x'$ equivalent.$x,x' \colon X \;\vdash \; \left(x \simeq x'\right) \colon Type$.The mapping cocone object $\array{ P_{x,x'} X &\to& * \\ \downarrow &\swArrow_{e}& \downarrow^{\mathrlap{x}} \\ * &\stackrel{x'}{\to} & X }$The moduli stack of gauge transformations between $x$ and $x'$.Identity types
There is an equivalence $e$ between $x$ and $x'$.$\array{\vdash \; e \colon (x \simeq x') \\ or \\ \vdash \; e \colon (x \rightsquigarrow x') }$An element of the mapping cocone object.A gauge transformation between $x$ and $x'$.
Given $x,x'$, there is the collection of proofs that it is true that $x$ and $x'$ are equivalent.$x,x' \colon X \;\vdash \; [x \simeq x'] \colon Type$.The (-1)-truncation fo the mapping cocone.The smooth set of equivalence classes of gauge transformations from $x$ to $x'$.

But the gauge principle reaches deeper: gauge transformations themselves are subject to the gauge principle.

In general it is meaningless to ask if two gauge transformations are equal, but we may ask if there is a higher gauge transformation that transforms one gauge transformation into the other. In the physics literature such gauge-of-gauge transformations are best known in their incarnation as ghost-of-ghost fields in what is called the BRST complex of the given gauge theory.

Careful analysis for instance of the Dirac charge quantization of magnetic charge shows that already quite mundane physical phenomena exhibit such higher gauge transformations. But more famously they are known to arise in various guises in string theory, which is a hypothetical refinement of the standard model of particle physics and gravity.

In either case, our formal language should not allow the deduction that gauge equivalences are themselves either equal or not, but only allow judgements of the following form:

There is a gauge-of-gauge equivalence $\rho \colon (\lambda_1 \simeq \lambda_2)$ between two given gauge equivalences $\lambda_1, \lambda_2 \colon (\nabla_1 \simeq \nabla_2)$ between two given gauge fields $\nabla_1, \nabla_2$.

The flavor of type theory with propositional equality for which this is the case is called intensional type theory.

Since therefore a type $X$ in intensional type theory may contain homotopies between its terms of arbitrary order, we call it a homotopy type.

The homotopy-type nature of the type of gauge connections $[X,\mathbf{B}G_{conn}]$ is most familiar in the physics literature in its infinitesimal approximation, which is the (off-shell) BRST complex of the gauge theory: the $n$-fold ghost-of-ghost fields in the BRST complex correspond to the $n$-fold homotopies in $[X, \mathbf{B}G_{conn}]$.

In particular, in intensional type theory we find the gauge group of a homotopy type, as indicated in the following table.

Expressions in intensional type theory:

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
Given a type $X$, there is (the underlying space) of a group $G$ of ways that $X$ is equivalent to itself.$X \colon Type \;\vdash \; (X \stackrel{\simeq}{\to} X ) \colon Type$A loop space object $\array{ G &\to& * \\ \downarrow &\swArrow& \downarrow^{\mathrlap{X}} \\ * &\stackrel{X}{\to} & Type }$A smooth ∞-group.n-groups
Given a function between collections of things $X$ and $Y$, and given a thing $y$, there is its preimage-up-to-equivalence.$\left( f \colon \left(X\to Y\right)\right), \left(y \colon Y\right) \;\vdash\; \sum_{x \colon X} \left(f\left(x\right) \simeq y\right)$A homotopy pullback $\array{ X \times_{Y} \{y \} &\to& X \\ \downarrow &\swArrow& \downarrow^{\mathrlap{f}} \\ {*} &\underset{y}{\to}& Y }$The homotopy fiber of a homomorphism of smooth moduli stacks.

Suppose then that we have such a map between collections of gauge fields

$\phi \colon [X, \mathbf{B}G_{conn}] \to [Y, \mathbf{B}H_{conn}]$

on two possibly different spacetimes with two possibly different gauge groups.

(For instance we might be looking at Montonen-Olive duality/_S-duality_ or Seiberg duality of super Yang-Mills theory.)

Then we should call $\phi$ an equivalence - in the physics literature often: a duality – if, while not necessarily being a “bijection”, it is such that the preimage $\phi^{-1}(\nabla) \in [X,\mathbf{B}G_{conn}]$ of a gauge field $\nabla \in [Y, \mathbf{B}H_{conn}]$ consists of gauge fields that are all gauge equivalent to each other, with the gauge equivalences exhibiting this equivalence themselves all being gauge equivalent to each other, etc.

If this is the case one says that all homotopy fibersall gauge pre-images – of $\phi$ are contractible – are gauge equivalent to a single gauge field – and that $\phi$ is a weak homotopy equivalence.

For consistency we should demand that the notion of equivalence is such that the space of direct equivalences $[X, \mathbf{B}G_{conn}] \simeq [Y, \mathbf{B}H_{conn}]$ is itself equivalent to the space of such weak homotopy equivalences (“dualities”) $[X, \mathbf{B}G_{conn}] \stackrel{\simeq}{\to} [Y, \mathbf{B}H_{conn}]$.

This requirement is called the univalence axiom. The intensional type theory-language considered so far equipped with this axiom is called homotopy type theory.

We indicate now some central judgements that are expressible in homotopy type theory. This involves fundamental judgements in group theory and in representation theory, two of the pillars of modern quantum theory/quantum field theory.

Structures expressible in homotopy type theory:

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
Given a type $X$, there is a group $G$ of ways that $X$ is equivalent to itself.$X \colon Type \;\vdash \; (X \stackrel{\simeq}{\to} X ) \colon Type$A loop space object $\array{ G &\to& * \\ \downarrow &\swArrow& \downarrow^{\mathrlap{X}} \\ * &\stackrel{X}{\to} & Type }$A smooth automorphism ∞-group.n-groups
Given a type $X$, there is the delooping $\mathbf{B}G$ of $G$, which is the collection of things equipped with equivalences to $X$.$X \colon Type \; \vdash \; \mathbf{B}G \coloneqq \sum_{Y \colon Type} \left[X \simeq Y\right]$The looping and delooping relation $\array{G \simeq &\Omega \mathbf{B}G &\to& * \\ & \downarrow &\swArrow& \downarrow^{\mathrlap{}} \\ & * &\underset{}{\to}& \mathbf{B}G}$The smooth moduli stack of smooth $G$-principal ∞-bundles.Principal n-bundles
Given a thing in $\mathbf{B}G$, there is a thing $V$.$\array{* \colon \mathbf{B}G \;\vdash\; V(*) \colon Type \\ or\;with\;more\;emphasis: \\ (*,*',g) \colon \sum_{*,*' \colon \mathbf{B}G} (*\rightsquigarrow *') \;\vdash\; V(* \stackrel{g}{\rightsquigarrow} *') \colon Type }$A homotopy fiber sequence $\array{V &\to& V\sslash G \\&& \downarrow^{\overline{\rho}} \\ && \mathbf{B}G }$ with homotopy fiber $V$ over $\mathbf{B}G$.An ∞-action/∞-representation of $G$ on some $V$, together with its universal $\rho$-associated $V$-fiber ∞-bundle over the moduli stack $\mathbf{B}G$ for $G$-principal ∞-bundles.Higher actions
Given a function $g$ classifying a $G$-principal bundle and given a point in the delooping, there is the $G$-principal bundle $P$ itself, being the collection of identifications of the fiber $g(x)$ with $X$$\left(g \colon X \to \mathbf{B}G\right), \left(* \colon \mathbf{B}G\right) \;\vdash\; P \coloneqq \sum_{x \colon X} (g(x) \simeq *)$$\array{P &\to& * & \simeq \mathbf{E}G \\ \downarrow &\swArrow& \downarrow \\ X &\stackrel{g}{\to} & \mathbf{B}G }$The principal ∞-bundle given as the homotopy pullback of the universal principal ∞-bundle.Principal ∞-bundles
There is a $G$-equivariant map from the principal bundle to the representation space.$\vdash\; \sigma \colon \prod_{* \colon \mathbf{B}G} \left(P \to V\right)$An element $\array{ X &&\stackrel{\sigma}{\to}&& V \\ & \searrow &\swArrow& \swarrow \\ && \mathbf{B}G}$ of $V$ in the slice topos $\mathbf{H}_{/\mathbf{B}G}$A section of the $\rho$-associated $V$-fiber ∞-bundle.

In gauge theory physics, a representation $\rho$ of the gauge group $G$ encodes the particle-content of the model (in theoretical physics): a section of the $\rho$-associated bundle to the gauge bundle is a matter field in the model.

Therefore all the ingredients so far encode the kinematics of gauge theory, its setup before an actual dynamics is specified.

Dynamics in physics says how things move, hence how they trace out trajectories in a given spacetime or more generally in some phase space.

Our language for reasoning about physics should be able to express this. For $X$ a homotopy type that models spacetime (the collection of all points of spacetime) there should be a homotopy type $\Pi(X)$ whose homotopies and higher homotopies are the smooth trajectories, the smooth paths and higher paths in $X$.

In order to analyse the notion of smoothness here – we will say: the way that points hold together by cohesion – there should also be

• an expression $\flat X$ for the discrete collection of points underlying $X$detaching all points;

• an expression $\sharp X$ which dissolves the cohesion and produces the codiscrete smooth structure on $X$.

There are some natural simple axioms on these constructions. For instance every smooth path in a discrete space $\flat X$ should be constant: $\Pi (\flat X) \simeq \flat X$.

With such natural axioms understood, these three constructions constitute an adjoint triple of modalities $(\Pi \dashv \flat \dashv \sharp)$ in our language. In particular $\Pi$ and $\flat$ are a monad and comonad on the type system, in the sense of computer science and $\sharp$ is even an internal monad.

Equipping the above homotopy type theory with these modalities turns it into what we call cohesive homotopy type theory.

Structures expressible in cohesive homotopy type theory:

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
Given a cohesive homotopy type $X$, there is the dissolved homotopy type $\sharp X$ in which all separate points are collected to one cohesive blob.$X \colon Type \;\vdash\; \sharp X \colon Type$The codiscrete object-monad on a (higher) local topos.The codiscrete smooth structure on the points of $X$.Locality of the topos of smooth spaces
Given a cohesive homotopy type, there is the map that dissolves the cohesion of the points.$X \colon Type \;\vdash\; DeCoh_X \colon X \to \sharp X$The unit of the codiscrete object monad.The function that sends smooth families in a smooth moduli stack to families of points.
Given $X$ there is the collection $\Pi(X)$ of points in $X$ and smooth trajectories between points in $X$.$\left(X \colon \sharp Type\right) \;\vdash\; \Pi(X) \colon \sharp Type$The construction of the fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos.The smooth path ∞-groupoid of $X$.The local ∞-connectedness of the (∞,1)-topos of smooth ∞-groupoids
Given $X$, there is a canonical map to $\Pi(X)$.$\left(X \colon \sharp Type\right) \;\vdash\; ConstantPathInclusion_X \colon X \to \Pi(X)$.The unit of the $\Pi$-monad on a locally ∞-connected (∞,1)-topos.The inclusion of $X$ into its smooth path ∞-groupoid as the constant paths.
Given $X$, there is the result of detaching the points in $X$.$\left(A \colon \sharp Type\right) \;\vdash\; \flat A \colon \sharp Type$The operation of the discrete object comonad on a (higher) local topos.The moduli stack for flat ∞-connections.
Given $A$, there is a map from flat $A$-connections to the underlying $A$-bundles$\left(A \colon \sharp Type\right) \;\vdash\; UnderlyingBundle_A \colon \flat A \to A$The counit of the discrete object-comonad on a (higher) local topos.The function that sends a flat ∞-connection to its underlying principal ∞-bundle.Flat connections

Adding the modalities $(\Pi \dashv \flat \dashv \sharp)$ to the above language of homotopy type theory yields a language that we call cohesive homotopy type theory (following a term introduced by Lawvere).

Fundamental judgements in cohesive homotopy type theory include those indicated in the following table, which capture central concepts of gauge theory and its (higher) geometric quantization.

Structures expressible in cohesive homotopy type theory:

Gauge fields, matter fields, and smooth action functionals on their moduli stacks

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
A flat connection $\nabla$ on $X$ is a rule for sending paths $(x \stackrel{\gamma}{\to} y) \in \Pi X$ to group elements, respecting composition.$transport(\nabla) \colon \underset{x,y \colon \Pi X}{\sum} \left( x \rightsquigarrow y \right) \to \underset{*,*' \colon \mathbf{B}G}{\sum} (* \rightsquigarrow *')$$\frac{\Pi(X) \stackrel{transport(\nabla)}{\to} \mathbf{B}G}{X \stackrel{\nabla}{\to} \flat \mathbf{B}G}$.The higher parallel transport $trans(\nabla)$ of a flat connection $\nabla$: a (higher) gauge field with vanishing field strength.Flat connections
A closed differential form $\omega$ is a flat connection $\nabla$ and a trivialization of the underlying bundle.\begin{aligned} & \flat_{dR} \mathbf{B} G \coloneqq \\ & \sum_{\nabla \colon \flat \mathbf{B}G} (UnderlyingBundle(\nabla) \simeq *) \end{aligned}\begin{matrix} \flat_{dR}\mathbf{B}G & \stackrel{UnderlyingConnection}{\begin{svg} [[!include SVG rightarrow]]\end{svg}}& \flat \mathbf{B}G \\ \begin{svg}[[!include SVG downarrow]]\end{svg} & \mathclap{\array{\arrayopts{\align{bottom}}\;\begin{svg}[[!include SVG pullback]]\end{svg} & \space{10}{0}{30} \\ \space{10}{30}{1} & \swArrow}} & \begin{svg}[[!include SVG downarrow]]\end{svg}{}^{\mathrlap{Underlying \atop Bundle}} \\ * &\stackrel{}{\begin{svg}[[!include SVG rightarrow]]\end{svg}}& \mathbf{B}G \end{matrix}The coefficients for de Rham hypercohomology – flat ∞-Lie algebra valued differential forms.de Rham coefficients
A general connection $\nabla$ is the equivalence between the curvature $curv(\mathbf{c})$ of a bundle $\mathbf{c}$ and a closed differential form $\omega$.$\nabla \colon \underset{{\mathbf{c} \colon \mathbf{B}^n \mathbb{G}} \atop { \omega \colon \Omega^{n+1}_{cl} }}\sum \left( curv\left(\mathbf{c}\right) = \omega\right)$\begin{matrix} \mathbf{B}^n \mathbb{G}_{conn} & \stackrel{F_{(-)}}{\begin{svg} [[!include SVG rightarrow]]\end{svg}}& \Omega^{n+1}_{cl} \\ \begin{svg}[[!include SVG downarrow]]\end{svg} & \mathclap{\array{\arrayopts{\align{bottom}}\;\begin{svg}[[!include SVG pullback]]\end{svg} & \space{10}{0}{30} \\ \space{10}{30}{1} & \swArrow}} & \begin{svg}[[!include SVG downarrow]]\end{svg} \\ \mathbf{B}^n \mathbb{G} &\stackrel{curv}{\begin{svg}[[!include SVG rightarrow]]\end{svg}}& \flat_{dR} \mathbf{B}^{n+1}\mathbb{G} \end{matrix}The coefficients for smooth differential cohomology: abelian (higher) gauge fields.Circle principal n-connections
There is a cohesive function from $G$-gauge fields to higher $\mathbb{G}$-gauge fields.$\vdash \; \exp(i S) \colon \mathbf{B}G_{conn} \to \mathbf{B}^n \mathbb{G}_{conn}$A differential universal characteristic class.An extended action functional/prequantum n-bundle for extended higher Chern-Simons-type gauge theory.

… and their ∞-geometric prequantization (see there for a more comprehensive dictionary):

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
There is a $\mathbb{G}$-equivariant map $\psi$ from the prequantum bundle to the representation space.$\vdash \; \psi \colon \underset{\nabla \colon \mathbf{B}\mathbb{G}_{conn}}{\prod} \left( P\left(\nabla\right) \to V\left(\nabla\right) \right)$$\array{ X &&\stackrel{\psi}{\to}&& V\sslash \mathbb{G}_{conn} \\ & {}_{\mathllap{\nabla}}\searrow &\swArrow& \swarrow_{\overline{\rho}} \\ && \mathbf{B} \mathbb{G}_{conn}}$A prequantum state.Geometric quantization
There is a differentially $\mathbb{G}$-equivariant equivalence $\exp(\hat O)$ from the prequantum bundle to itself.$\vdash \; \exp(\hat O) \colon \underset{\nabla \colon \mathbf{B}\mathbb{G}_{conn}}{\prod} \left( P\left(\nabla\right) \stackrel{\simeq}{\to} P\left(\nabla\right) \right)$$\array{ X &&\stackrel{\exp(\hat O)}{\to}&& X \\ & {}_{\mathllap{\nabla}}\searrow &\swArrow& \swarrow_{\nabla} \\ && \mathbf{B} \mathbb{G}_{conn}}$A prequantum operator: an element of the quantomorphism group/Heisenberg group of the quantum system.Geometric quantization

Finally, in order to be able to concretely speak about not just about any gauge field, but the concrete particular gauge fields in the observable universe, our language should be able to express the existence of the continuum real line.

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
There is the continuum line.\begin{aligned}\vdash\; & \mathbb{R} \colon Type \\ & i \colon \mathbb{Z} \to \mathbb{R} \\ & GeometricallyContract_{\mathbb{R}} \colon (\Pi(\mathbb{R}) \simeq Point) \end{aligned}line objectreal lineThe continuum real worldline

This then induces the existence of the circle group $U(1) = \mathbb{R}/\mathbb{Z}$. The electromagnetic field is a gauge field for gauge group $U(1)$. Therefore in the language of cohesive homotopy type theory we can say

Let there be light.

ordinary languagesyntaxsemanticsmodelchapter
general abstractgeneral concreteconcrete particular
There is the collection of higher $U(1)$-principal connections.$n\colon \mathbb{N} \; \vdash \; \mathbf{B}^n U(1)_{conn} \colon Type$The coefficients for ordinary differential cohomology (with coefficients in an Eilenberg-MacLane object.)The smooth higher moduli stack of smooth circle n-bundles with connection.Circle-principal n-connections.
There is light.$\vdash \; \nabla_{em} \colon [X,\mathbf{B}U(1)_{conn}]$A cocycle in ordinary differential cohomology in degree-2.A configuration of the electromagnetic field on spacetime $X$.Circle principal connection

$\,$

There are of many more constructions in fundamental (quantum) physics that are naturally expressible in cohesive homotopy type theory, but the above should already give an idea and highlight the cornerstones of the following discussion.

$\,$

We now end this introduction and overview and turn to the in-depth account of geometry of physics.

Contents

I) Geometry

We begin by laying the foundations of differential geometry. Doing this in the natural abstract way seamlessly leads over to the foundations of higher differential geometry (see also motivation for higher differential geometry). Once this is set up, we discuss the fundamental constructions: groups, actions/representations, fiber bundles, connections, Chern-Weil theory.

Categories and Toposes

This chapter is as geometry of physics – Categories and Toposes

Smooth set

This chapter is at geometry of physics – smooth sets.

Smooth homotopy types

This chapter is at geometry of physics – smooth homotopy types.

Stable homotopy types

This chapter is at geometry of physics – stable homotopy types.

Groups

This chapter is at geometry of physics – groups.

Principal bundles

This chapter is at geometry of physics – principal bundles.

Manifolds and Orbifolds

this chapter is at geometry of physics – manifolds and orbifolds

$G$-Structure and Cartan geometry

this chapter is at geometry of physics – G-structure and Cartan geometry

Representations and Associated bundles

this chapter is at geometry of physics – representations and associated bundles

Modules

this chapter is at geometry of physics - modules

Flat connections

this chapter is at geometry of physics – flat connections

Principal connections

this chapter is at geometry of physics – principal connections

Integration

this chapter is at geometry of physics – integration

Super-geometry

this chapter is at geometry of physics – supergeometry and superphysics

Prequantum geometry

this chapter is at geometry of physics – prequantum geometry

WZW terms

this chapter is at geometry of physics – WZW terms

BPS charges

this chapter is at geometry of physics – BPS charges

Perturbative quantum field theory

This section is at geometry of physics – perturbative quantum field theory.

Physics in Higher Geometry: Motivation and Survey

Before we discuss technical details starting in the next chapter here we survey general ideas of theories in fundamental physics and motivate how these are naturally formulated in terms of the higher geometry that we developed in the first part.

This chapter is at geometry of physics – physics in higher geometry.

Hamilton-Jacobi-Lagrange mechanics via prequantized Lagrangian correspondences

This chapter is at prequantized Lagrangian correspondence.

Hamilton-de Donder-Weyl field theory via Higher correspondences

This chapter is at Local field theory via Higher correspondences.

Local (topological) prequantum field theory

This chapter is at geometry of physics – local prequantum field theory.

Prequantum Gauge theory and Gravity

this chapter is at geometry of physics – prequantum gauge theory and gravity

Quantum mechanics

This section is at geometry of physics – quantum mechanics

(…)

Application to open questions in physics

What is it that higher geometry, higher gauge theory, extended/local field theory and generally higher category theory in physics contribute to open research questions in theoretical physics?

Often when this question is asked the most glaring open question of contemporary theoretical physics is forgotten:

What IS local quantum field theory?

While something going by this name is clearly in use, it is just as clear that the full answer to this question is only being discovered these days, with formalizations such as the cobordism theorem and constructions such as factorization algebras in BV-quantization – both of which are crucially constructions in higher geometry/higher category theory.

Despite the huge success of quantum field theory, it it worthwhile to remember that all the fundamental open questions in present day fundamental physics quite likely require a deeper understanding of what quantum field theory actually is, notably non-perturbatively:

For instance the standard model of cosmology says that the bulk of all energy and matter in the observable universe is entirely unknown to us (dark matter, “dark energy”), while at the same time the theoretical prediction what the cosmological constant vacuum energy should be is entirely off. How glaring an open question about the nature of quantum field theory this actually is is often forgotten due to the success of effective field theory-type of reasoning that allows to neatly wrap up all this unknown energy into a single term in some effective equation. Phenomenologically this may be regarded as a success, but for fundamental theoretical physics it is a glaring open question.

And while there is work going in this direction, it may be worthwhile to recall how relatively primitive the available theoretical tools often still are. For instance it seems clear that “canonical non-covariant quantization” can hardly be an approrpiate tool to approach anything in the direction of quantum gravity. Even so fundamental a notion as that of covariant phase space necessary to make progress here is not widely known in the theoretical physics community. Attempts to refine quantization to a “covariant” and “local” formalism via multisymplectic geometry have mainly got stuck, since local observables just do not form a sensible structure in ordinary Lie theory. This is resolved only in infinity-Lie theory and higher differential geometry, as discussed above (hgp 13, lo 13).

If one assumes that string theory is part of the answer as to what underlies the standard model of particle physics and cosmology, then this situation becomes more drastic even. The fundamental fields of string theory are clearly objects in higher differential geometry, such as the B-field, the RR-field, the supergravity C-field etc. For instance the natural identification of the latter as a homotopy fiber product of moduli stacks in (FSS7dCS, FSSCField) is hardly conceivable when ignoring higher differential geometry. And this is a structure meant to be at the very heart of what makes up string theory. It is unlikely that the landscape of string theory vacua and hence the relation of string theory to phenomenology can really be understood if such basic higher-geometric phenomena of string theory are ignored (see Distler-Freed-Moore 09 on this point).

(…)

General

A textbook with basic introductions to differential geometry and physics is

A discussion of aspects of quantum field theory with emphasis on the kind of modern tools that we are using here is in

The present discussion corresponds to section “1.2 Geometry of phyics” in

which gives a more comprehensive account.

Another set of lecture notes along the above lines with an emphasis on aspects in gravity and higher gauge theory motivated from string theory is in

An exposition and survey of matters related to Chern-Simons theory and higher geometric quantization is in

The syntactic perspective above is laid out further in

see also at motivic quantization the section General abstract type theoretic summary.

Mathematical quantum field theory

A textbook (really a collection of lecture notes) on quantum field theory and string theory that tries to present material in a conceptually clean way is

David Kazhdan, John Morgan, D.R. Morrison and Edward Witten, eds. Quantum Fields and Strings, A course for mathematicians, 2 vols. Amer. Math. Soc. Providence 1999. (web version)

A collection trying to summarize the state of the art of the formalization of QFT by FQFT and AQFT as of 2011 is

Topos theory in differential geometry and physics

One of the central figures of topos theory and categorical logic, William Lawvere, has motivated his interest in these subject always with intended application to the formalization of physics (of classical continuum mechanics in his case).

An influential text is

• William Lawvere, Toposes of laws of notion, Toposes of laws of motion , transcript of a talk in Montreal, Sept. 1997 (pdf)

which motivates synthetic differential geometry from differential equations appearing as equations of motion in physics. The early text

already sketches the formulation of cohesive toposes and motivates their axioms with heuristics from geometry and physics.

A review by Lawvere is in

• William Lawvere, Comments on the Development of Topos Theory, Development of Mathematics 1950-2000, 715-734 (2000) Birkhäuser Basel

Modern accounts of physics in this spirit includes notably also the book (Paugam) listed above.

Higher category theory in physics

An early proposal that the action functional of $n$-dimensional quantum field theory should refine to a structure involving (n-k)-vector spaces in codimension $(n-k)$ is in

The full formalization of this for extended topological field theory is due to

Related comments on the extended quantization of infinity-Dijkgraaf-Witten theory are in

For more pointers see at higher category theory and physics.

Local prequantum field theory

The idea of formulating local prequantum field theory by spans in a slice over a “space of phases” in higher geometry has been expressed in the unpublished note

A formulation of the idea for Dijkgraaf-Witten theory-type field theories is indicated in section 3 of

based on the considerations in section 3.2 of

Based on the general formulation of the more general field theory with defects described in section 4.3 there, in

the structure of such domain walls/defects/branes are analyzed in the prequantum theory, hence with coefficients in an (∞,n)-category of spans.

The study of local prequantum ∞-Chern-Simons theory with its codimension-1 ∞-Wess-Zumino-Witten theory and codimension 2-Wilson line-theory in this fashion, in an ambient cohesive (∞,1)-topos is discussed in (lpqft)

Much of the content of this entry here are, or arose as, lecture notes for

Further details

Physical fields

For references on the tradtional formulation of physical fields by sections of field bundles as discussed above see there references there.

The formulation of physical fields as cocycles in twisted cohomology in an (∞,1)-topos as in the Definition-section above originates around

Further articles since then are listed at

In particular the general notion of fields as twisted differential c-structures appears in

and the general theory of cohomology and twisted cohomology with local coefficient ∞-bundles as referred to in Relation to twisted cohomology above as well as the theory of associated ∞-bundles as in Sections of associated ∞-bundles is laid out in

Some examples of fields in this sense are called “relative fields” in

Differential forms and parallel transport

The relation between differential 1-forms and smooth incremental path measures as used above is discussed in

For a commented list of related literature see here.

(…)

3d Chern-Simons theory and Wilson loops

• Chris Beasley, Localization for Wilson Loops in Chern-Simons Theory, in J. Andersen, H. Boden, A. Hahn, and B. Himpel (eds.) Chern-Simons Gauge Theory: 20 Years After, , AMS/IP Studies in Adv. Math., Vol. 50, AMS, Providence, RI, 2011. (arXiv:0911.2687)

Higher Chern-Simons theories

The discussion of the abelian 7d Chern-Simons theory involved in AdS7/CFT6 duality is due to (Witten 98). A discussion of the non-abelian quantum-corrected and extended refinement is in

Construction of differential cup-product theories is in