Schreiber Modern Physics formalized in Modal Homotopy Type Theory

• Urs Schreiber

  Modern Physics formalized in Modal Homotopy Type Theory,

  (pdf)

  expanded notes for a talk at

  What are Suitable Criteria for a Foundation of Mathematics?

  FOMUS – Foundations of Mathematics, July 2016

Abstract. Where plain homotopy type theory provides a formal concept-logic, adding adjoint modal operators to it (Shulman 12, Schreiber-Shulman 14, Licata-Shulman 15, Shulman 15) serves to encode determinations of further qualities. Following (Lawvere 9x-0x), these categories of being naturally organize themselves in a progressive system of oppositions and resolutions which the inclined philosopher might enjoy to compare to the informal “Science of Logic”. This formal substance of modal homotopy type theory subsumes modal predicate logic but is immensely more expressive. The talk surveys how (Schreiber 13) externalizing this idea into natural models gives rise to the modern mathematics of space in higher/derived geometry and to modern physics of local prequantum field theory in supergravity/string theory.

$\,$

---

For full technical details glossed over in the following see:

• geometry of physics – categories and toposes

• geometry of physics – supergeometry

---

$\,$

Introduction

We survey axioms for a system of modal operators that may naturally be added to homotopy type theory; and we survey how these induce a synthetic formalizaton of differential cohomology, higher differential geometry and of key structures in fundamental physics, notably Einstein-Cartan higher gauge prequantum field theory (dcct).

Formalization. The following is written in the pseudocode formerly known as mathematics. Parts of this have been fully formalized in computer-verified code (Shulman), the rest is in a form that should lend itself to such full formalization.

Synthetic axioms. Here synthetic axiomatics is meant in contrast with the following analytic axiomatics: The restriction of homotopy type theory to homotopy 0-types (“h-sets”) is a constructive set theory. A traditional assumption is that in principle and with enough patience it is possible to fullly formalize all rigorous mathematics in set theory, and with a little bit of extra care added also in constructive set theory. This way one could imagine to formalize, in principle and with much patience, first standard simplicial homotopy theory within the h-sets, then formalize the homotopy theory of simplicial presheaves, hence of infinity-stacks, to obtain a full formalization of homotopy toposes, then impose axioms on these to formalize the particular examples of, say, smooth infinity-groupoids, formal smooth infinity-groupoids and super formal smooth infinity-groupoids that are the necessary backdrop for, finally, formalizing modern physics.

While this program already sounds hardly tractable in practice, its practical usefulness is arguably even more remote. One is reminded of the fully formal proof of $1+1 = 2$ which in the Principia Mathematica takes 300 pages. Nobody ever did or will ever do any useful mathmatics (as opposed to metamathematics) based on this.

But in both cases type theory and homotopy type theory, respectively, comes to the rescue. In type theory the proof of $1+1 = 2$ is as trivial as it should be, thanks to the natural concept of inductive types. Similarly, in homotopy type theory the concept of infinity-stacks is already built in: every type in homotopy type theory has the generic interpretation of an infinity-stack. Instead of throwing that away by restricting to homotopy 0-types (whose interpretation is as mere sheaves of sets) and then tediously analytically rebuilding the informaltion thus lost, it is clearly advisable to retain that structure and make use of it synthetically. This is what we do below.

Modern physics. Our axioms owe a lot to William Lawvere, who had long ago suggested ( Toposes of laws of motion ) that some suitable elementary axioms imposed on toposes should provide a good context for formalization of physics. Lawvere’s axioms of synthetic differential geometry allow to formalize differential equations and hence much of classical field theory (his motivation is drawn from continuum mechanics). However, modern physics is considerably richer than that, being based on local higher gauge quantum field theory, including fermions, hence supergeometry, and including boundary conditions such as branes in string theory. Our axioms serve to formalize considerable chunks of this, and they do so naturally in that these structures follow from just a few lines of universal constructions involving the axioms.

Metaphysics. The following indulges in idealistic jargon of “subjective and objective logic”, following (Lawvere 92, Lawvere-Rosebrugh 03, section C.1). This is meant as a suggestion for a kind of pre-mathematical meaning explanation of the axioms. Dies zu wissen ist nicht not.

Expanded talk notes

Subjectivity

Concept

We use the Laws of Type:

Homotopy type theory as such (UFP 13) is a logic of types, of (mathematical) concepts (Martin-Löf 73, 1.1, Ladyman&Presnel 14). (References which recall that the modern “type” is a contraction of “type of mathematical concepts” include for instance also (Sale 77, p. 6).

With the univalence axiom for weakly Tarskian type universes included – which says that this essence appears properly reflected within itself – then its interpretation via categorical semantics is in elementary homotopy toposes (Shulman 12a, Shulman 12b, Shulman 14). These are the models of homotopy type theory. Conversely, homotopy type theory is the internal language of homotopy toposes, hence the latter are its “externalization”. This way homotopy type theory overlaps much with (higher) categorical logic. See at relation between type theory and category theory for more background on this.

Accordingly, since it is more immediately readable, we display mostly categorical expressions in the following, instead of the pure type theoretic syntax.

Judgement

The earliest formulation of a logic of concepts is arguably Aristotle's logic, which famously meant to reason about the relation of concepts such as “human” and “mortal”. We consider now a natural formalization of at least the core intent of Aristotle’s logic in dependent homotopy type theory.

Formalizations of Aristotle’s logic in categorical logic or type theory has previously been proposed in (LaPalmeReyes-Macnamara-Reyes 94, 2.3) and in (Pagnan 10, def. 3.1). The formalization below agrees with these proposal in the identification of the Aristotlean judgement “All $B$ are $A$” with the type-theoretic judgement “$\vdash f \colon B\to A$”, and with the identification of syllogisms with composition of fuch function terms.

All $B$ are $A$.

If $C$ is a concept, a type, then a judgement

$$c \colon C$$

says that $c$ is an instance of the concept $C$, or that $c$ is a term of type $C$.

For instance if $\mathbb{N}$ is the concept of natural numbers, then the judgement $n \colon \mathbb{N}$ says that $n$ is a natural number. Clearly here the “concept” $\mathbb{N}$ may just as well be thought of as the set of all its instances.

Given concepts/types $A$ and $B$, there is the concept of maps between them, the function type $B\to A$. In the categorical semantics this is the internal hom.

The judgement that there is a function, hence an instance $f$ of the concept of functions

$$f \colon B \longrightarrow A$$

says that $f$ is a rule that takes instances/terms of $B$ to instances/terms of $A$. At least if this is a monomorphism $f \colon B \hookrightarrow A$ (so that the corresponding $a\colon A \vdash f^{-1}(a)$ is a proposition) then this says in words that $f$ witnesses the fact that

All instances of $B$ are instances of $A$.

or for short just

All $B$ are $A$

hence that if $A$ is das Allgemeine (general, universal) concept then $B$ is das Besondere (special, particular) concept.

This formalization of Aristotle’s “All $B$ are $A$” in categiorical logic/type has been proposed in (LaPalmeReyes-Macnamara-Reyes 94, 2.3), where it is attributed to William Lawvere, and in (Pagnan 10, def. 3.1).

Notice that the choice of $f$ here is an important part of the formalization which is missing in Aristotle’s informal logic and causing ambiguity there.

For instance all natural numbers are real numbers, but there are many inequivalent subgroup inclusions $\mathbb{Z}\hookrightarrow \mathbb{R}$ realizing this. For the purposes of prequantum field theory these choices correspond to the choice of Planck's constant (see the discussion there).

Similarly, once we have that the informal “All $B$ are $A$.” is formalized by a map of types, we see further refinement of the ancient logical notion.

First, the meaning of $B$,$A$ may depend on some context $C$. Leaving that implicit is arguably the greatest source of ambiguity in Aristotle’s logic. But it is easily fixed while staying true to the original intention: in general $B$ and $A$ are to be taken as $C$-dependent types. Then the intended meaning of All $B$ are $A$. is expressed by the dependent product over the function type formed in context $C$

$$f\colon \underset{C}{\prod} (B \longrightarrow A) \,.$$

Second, if $f$ is not a monomorphism it still expresses the fact that for every instance of $B$ there is a corresponding instance of $A$. Hence in general, we should further specify if $f$ is an n-truncated morphism. This is a general phenomenon in passing to higher homotopy types: the (epi, mono) factorization system on homotopy 0-types refines to a tower of (n-epi, n-mono) factorization systems for all natural numbers $n$.

Individual $E$ is $B$.

There is the unit type

$$E = \ast$$

of which there is a unique instance, das Einzelne (individual). As a concept, this may be regarded as the concept of pure being: since any two instances of the concept $E$ just purely are, there is no distinction and hence there is a unique instance.

Hence a function of the form $E \longrightarrow B$ is equivalently an instance/term $b$ of $B$. In words this says that

The individual $b$ is an instance of the general concept $B$.

of for short just

Individual $b$ is $B$.

There is the identity type $b = b$, which expresses the concept that $b$ is equivalent to itself.

The single introduction rule for identity types gives for all $X$ the statement that there is indeed an instance of this concept

$$r_b \colon b = b \,.$$

The categorical semantics of $(b = b)$ is the loop space object $\Omega_b B$, which is canonically a pointed object via the constant loop $id_n \colon \ast \to \Omega_b B$.

Under composition of loops, this object canonically carries the structure of an infinity-group.

Proposition

In any homotopy topos $\mathbf{H}$, the operation of forming loop space objects constitutes an equivalence of (infinity,1)-categories

$$Grp(\mathbf{H}) \stackrel{\overset{\Omega}{\longleftarrow}}{\underset{\mathbf{B}}{\longrightarrow}} \mathbf{H}^{\ast/}_{\geq 1}$$

between infinity-groups in $\mathbf{H}$ and pointed connected objects in $\mathbf{H}$.

The inverse equivalence $\mathbf{B}$ is called delooping. See at looping and delooping for more.

Now in homotopy type theory and in elementary (infinity,1)-toposes, the definition of infinity-groups as grouplike A-infinity algebras is not available, since the latter is not a finitary concept. But by prop. the concept also has a simple finitary equivalent incarnation, which is available in homotopy type theory: we may identify an infinity-group $G$ with its pointed connected delooping type $\mathbf{B}G$.

Indeed this is most useful: homotopy type theory in the context of $\mathbf{B}G$ is the infinity-representation theory of $G$:

representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory (FSS 12 I, exmp. 4.4):

homotopy type theory	representation theory
pointed connected context $\mathbf{B}G$	∞-group $G$
dependent type on $\mathbf{B}G$	$G$-∞-action/∞-representation
dependent sum along $\mathbf{B}G \to \ast$	coinvariants/homotopy quotient
context extension along $\mathbf{B}G \to \ast$	trivial representation
dependent product along $\mathbf{B}G \to \ast$	homotopy invariants/∞-group cohomology
dependent product of internal hom along $\mathbf{B}G \to \ast$	equivariant cohomology
dependent sum along $\mathbf{B}G \to \mathbf{B}H$	induced representation
context extension along $\mathbf{B}G \to \mathbf{B}H$	restricted representation
dependent product along $\mathbf{B}G \to \mathbf{B}H$	coinduced representation
spectrum object in context $\mathbf{B}G$	spectrum with G-action (naive G-spectrum)

(NSS, dcct)

Some $B_1$ is $B_2$.

In order to formalize judgements of intersection of concepts of the form

Some $B_1$ is $B_2$.

it is necessry to specify a context. Regard both $B_1$ and $B_2$ as dependent types witnessed by display maps

$f_i \colon B_i \longrightarrow C$

to a common context $C$. Then the product type in context, hence, in the categorical semantics, the homotopy fiber product

$$B_1 \underset{C}{\times} B_2$$

is the type whose terms are the “some” instances of $B_1$ which are also instances of $B_2$, and vice versa. Indeed, the fiber product canonically sits in the homotopy pullback diagram

$$\array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 \\ \downarrow && \downarrow \\ B_1 &\longrightarrow& C }$$

and if we read $B_1 \underset{C}{\times} B_2$ as “some $B_1$” then according to the previous paragraph the top morphism expresses that “all of these particular $B_1$ (but not necessarily all of $B_1$ itself) are $B_2$”.

Example

(principal infinity-bundles as judgements)

Specifically if $C = \mathbf{B}G$ here is pointed via a map from $B_2 = E = \ast$, and connected, hence equivalently the delooping of its infinity-group $G$ of loops, then (writing now $B$ for $B_1$) a map of types

$$c \colon B \longrightarrow \mathbf{B}G$$

may be thought of as a cocycle on $B$ with coefficients in $G$, representing a class in the nonabelian cohomology of $B$. See at cohomology for more on this general concept of cohomology.

In this case the homotopy fiber of $f$ is the $G$-principal infinity-bundle $P \to B$ classified by $f$, fitting into the homotopy pullback square.

$$\array{ P &\longrightarrow& E \\ \downarrow && \downarrow \\ B &\stackrel{c}{\longrightarrow} & \mathbf{B}G }$$

Via the above translation this is an Aristotlean judgement of the form “Some $B$ are $E$” in the context of $\mathbf{B}G$.

Summary

In summary we have that basic judgements in Aristotle’s logic, when some implicit assumptions are made explicit and the broad intention is retained, are naturally taken to be formalized in type theory as combinations of a type former and a judgement asserting a term of that type, as follows.

Aristotle's logic	formal syntax	type theory
concept	$C$	type
judgement	$c \colon C$	typing judgement
All $B$ are $A$.	$f \colon B \longrightarrow A$	function type
Some $B_1$ is $B_2$.	$s \colon B_1 \underset{A}{\times} B_2$	product type
Individual $E$ is $B$.	$e \colon E \to B$.	unit type/global element

Deduction

The figure $E-B-A$

Functions may be composed. Given $b \colon E \to B$ and $f \colon B \to A$, then their composite is a function $f e \colon E \to A$. In type theory this is an example of natural deduction (cut elimination), in words this is a syllogism

All $B$ are $A$.

Individual $E$ is $B$.

Hence

Individual $E$ is $A$.

$$\begin{aligned} f & \colon B \longrightarrow A \\ b & \colon E \longrightarrow B \\ f b & \colon E \longrightarrow A \end{aligned}$$

The figure $B-B-A$

Analogously, the categorical semantics for

Some $B_1$ is $B_2$.

All $B_2$ is $A$.

Hence

Some $B_1$ is $A$.

(all in some context $C$) is given by the horizontal composite in diagrams of the form

$$\array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 &\longrightarrow& A \\ \downarrow && \downarrow & \swarrow \\ B_1 &\longrightarrow& C } \,.$$

The method (absolute Idea)

What is not present in such bare homotopy type theory is determination of further qualities of types. For instance for synthetically formalizing physics one needs that types have topological and moreover differential geometric qualities to them. Some externalizations of homotopy type theory exhibit these, others do not. We now consider adding axioms to homotopy type theory that narrow it in on those models that do exhibit further quality in addition to the pure being of types.

Moments

A general abstract way to express a kind of quality carried by types is to posit a projection operation $\bigcirc$ that projects out the moment of pure such quality.

For instance for formalizing realistic physics one needs to determine bosonic and fermionic moments (we come to this below), and one way of doing so is by considering a projection operation that projects every space of fields to its purely bosonic body (lemma below).

Generally, for $X$ a type, then $\bigcirc X$ is to be the result of projecting out some pure quality of $X$. This being a projection means that $\bigcirc X \simeq \bigcirc \bigcirc X$. For this to be constructive, we need to specify a specific comparison map that gives this equivalence. Hence we say a moment projection is an operation $\bigcirc$ on the type system together with natural functions $X \to \bigcirc X$ such that $\bigcirc(X \to \bigcirc X)$ is an equivalence $\bigcirc \stackrel{\simeq}{\longrightarrow} \bigcirc \bigcirc X$.

In categorical semantics this means essentially that $\bigcirc$ is an idempotent monad on the type system $\mathbf{H}$.

Alternatively we may ask for a comparison map the other way around, $\Box X \longrightarrow X$, such that $\Box(\Box X \longrightarrow X)$ is an equivalence. In categorical semantics this means essentially that $\Box$ is an idempotent comonad.

Definition

A moment on (or in) a type system $\mathbf{H}$ is

• an idempotent monad $\bigcirc \colon \mathbf{H} \to \mathbf{H}$

or

• an idempotent comonad $\Box \colon \mathbf{H} \to \mathbf{H}$.

Given a moment, we write

$$\mathbf{H}_{\bigcirc, \Box} \hookrightarrow \mathbf{H}$$

for the inclusion of its image, which we think of as the collection of those types that exhibit the moment purely (conversely these define the kind of moment as whatever quality it is that they all exhibit purely).

Remark

This is a language construct natural and familiar also from the point of view of computational trinitarianism, see at monad (in computer science).

Further, it makes sense to refer to moments $\Box,\;\bigcirc$ also as modal operators or just modalities for short, and speak of type theory equipped with such operators as modal type theory, a type-theoretic refinement of modal logic. In this language the types in $\mathbf{H}_{\Box}$ are the $\Box$-_modal types.

Remark

A moment $\bigcirc$ or $\Box$ may be thought of as encoding a concept of similarity: as the operator projects out some details of the quality of a type and only retains some pure moment, it coarse-grains the nature of a type to some extent. Hence two types $X$ and $Y$ may be different but “similar with respect to $\bigcirc$-quality” if their images under $\bigcirc$ are equivalent:

$$(X \,similar_{\bigcirc}\, Y) \coloneqq (\bigcirc(X) \,= \, \bigcirc(Y))$$

(where on the right we have an identity type of the type universe).

Example of this are made explicit below as example , example .

Proposition

The category $\mathbf{H}_{\bigcirc}$ is equivalently the Eilenberg-Moore category of $\bigcirc$.

This is a standard fact in category theory, see at idempotent monad – Algebras.

Remark

Prop. means that we may naturally make sense of “pure qualtity” also for (co-)monads that are not idempotent, the pure types should be taken to be the “algebras” over the monad.

A single moment $\Box$ or $\bigcirc$ may be interpreted as most anything, since it is not further determined yet. One now observes that there is an intrinsic, self-propelling way to further determine such abstract moments, by asking for their opposite and for their negative moments.

Opposites

Definition

(unity of opposites)

The opposite of a moment $\bigcirc$, def. is, if it exists, another moment $\Box$ in adjunction with it,

1. either $\bigcirc$ left adjoint to $\Box$ and such that there is an adjoint triple

   $$\mathbf{H}_{\Box}\simeq H_{\bigcirc} \stackrel{\hookrightarrow}{\stackrel{\longleftarrow}{\hookrightarrow}} \mathbf{H}$$

   which we denote by

   $$\Box \dashv \bigcirc$$

2. or right adjoint to it with

   $$\mathbf{H}_{\Box}\simeq \mathbf{H}_{\bigcirc} \stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}} \mathbf{H}$$

   which we denote by

   $$\bigcirc \dashv \Box \,.$$

(We always display adjoint functors with the left adjoint on top and its right adjoint beneath.)

We say that the adjunction itself is the unity of opposites, and we indicate this by labels as in

$$\stackrel{moment}{} \Box \stackrel{unity \atop {of\,opposites}}{\dashv} \bigcirc \stackrel{opposite\;moment}{} \,.$$

Remark

In categorical semantics an opposition of moments, def. ,

• of the form $\Box \dashv \bigcirc$ defines an essential subtopos, the image of $\bigcirc$. This is also called a level of a topos.

• of the form $\bigcirc \dashv \Box$ defines a bireflective subcategory (in the sense of: reflective and coreflective subcategory).

It is fairly familiar from the practice of category theory that adjunctions express oppositions. The following example is drawn from arithmetic and is meant to illustrate this in a familar context, but the actual examples that we will be concerned with are more fundamental.

Example

Consider the two inclusions $even, odd \colon (\mathbb{Z},\lt ) \hookrightarrow (\mathbb{Z},\lt)$ of the even and the odd integers, i.e. the maps $n \mapsto 2 n$ and $n \mapsto (2n+1)$, respectively.

$$\mathbb{Z} \stackrel{\overset{even}{\hookrightarrow}}{\stackrel{\longleftarrow}{\underset{odd}{\hookrightarrow}}} \mathbb{Z}$$

Both are adjoint to the operation of forming the $floor$ of the result of dividing by two, this is right adjoint to the inclusion of even numbers, and left adjoint to the inclusion of odd numbers.

$$\array{ \stackrel{even}{} & \Box &\dashv& \bigcirc & \stackrel{odd}{} }$$

This has been considered in (Lawvere 00)

Example

Consider the inclusion $\iota \colon (\mathbb{Z}, \lt) \hookrightarrow (\mathbb{R}, \lt)$ of the integers into the real numbers, both regarded linear orders. This inclusion has a left adjoint given by $ceiling$ and a right adjoint given by $floor$. The composite $Ceiling \coloneqq \iota ceiling$ is an idempotent monad and the composite $Floor \coloneqq \iota floor$ is an idempotent comonad on $\mathbb{R}$. Both express a moment of integrality in an real number, but in opposite ways, each real number $x\in \mathbb{R}$ sits in between its floor and celling

$$Floor(x) \lt x \lt Ceiling(x) \,.$$

$$\array{ \stackrel{ceiling}{} &\bigcirc &\dashv& \Box & \stackrel{floor}{} } \,.$$

This example highlights that:

Remark

There is an opposition between the two kinds of opposition here:

1. $(\Box \dashv \bigcirc)$ – Here are two different opposite “pure moments” .

2. $(\bigcirc \dashv \Box)$ – Here is only one pure moment, but two opposite ways of projecting onto it.

Determinate negation

If $\Box X$ is a pure moment found inside $X$, then it makes to ask for its complement moment or its negative

Definition

The negative of a comonadic moment $\Box$ is what remains after taking away the piece of pure $\Box$-quality, hence is the cofiber of the counit map:

$$\overline{\Box} X \coloneqq cofib(\Box X \to X) \,.$$

The intuitive meaning suggests to ask whether this kind of negation of determinations is faithful in that there is no $\Box$-moment left in the negative $\overline{\Box}$, hence whether

$$\Box \overline{\Box} \simeq \ast \,.$$

In general there is no reason for this to be the case. But if $\Box$ also has an opposite in the sense of def. , then one of the two opposite moments is left adjoint, hence preserves cofibers, and then a little more may be said.

Consider the case of an opposition of the form $\bigcirc \dashv \Box$. In view of remark then both $\bigcirc$ and $\Box$ express the same pure moment, just opposite ways of projecting onto it. Therefore in this situation it makes sense to alternatively ask that there is no $\bigcirc$-moment left in the $\overline{\Box}$.

Definition

Given a unity of opposite moments $\bigcirc \dashv \Box$, def. , we say this has determinate negation if $\Box$ and $\bigcirc$ both restrict to 0-type and such that there

1. $\bigcirc \ast \simeq \ast$;

2. $\Box \longrightarrow \bigcirc$ is epi.

Proposition

For an opposition with determinate negation, def. , then on 0-types there is no $\bigcirc$-moment left in the negative of $\Box$-moment:

$$\bigcirc \overline{\Box} \simeq \ast \,.$$

Proof

Given that $\bigcirc$, being a left adjoint, preserves colimits, hence cofibers, the first condition in def. gives that

$$\bigcirc \overline{\Box} X = \bigcirc cofib(\Box X \to X) \simeq cofib(\Box X \to \bigcirc X) \,.$$

Now the second condition and the fact that epiness is preserved by pushout say that this result receives an epimorphism from the terminal object. But this forces it to be the terminal obect itself.

The proof of prop. depends crucially on the restriction to 0-types. At the other extreme, on stable types the intuition that $\bigcirc$-moment is complementary to $\overline{\Box}$-moment is verified in the following sense:

Proposition

For opposite moments of the form $\bigcirc \dashv \Box$, def. , then for stable types $X$ the hexagons

$$\array{ && \overline{\bigcirc} X && \longrightarrow && \overline{\Box} X \\ &\nearrow& &\searrow& & \nearrow && \searrow \\ \overline{\bigcirc} \Box X && && X && && \bigcirc \overline{\Box} X \\ &\searrow& &\nearrow & & \searrow && \nearrow \\ && \Box X && \longrightarrow && \bigcirc X }$$

are homotopy exact in that

1. both squares are homotopy Cartesian, hence are fracture squares;

2. the boundary sequences are long homotopy fiber sequences.

In particular every stable type is the fibered direct sum of its pure $\bigcirc$-moment and its pure $\overline{\Box}$-moment:

$$X \simeq (\bigcirc X) \underset{\bigcirc \overline{\Box} X}{\oplus} (\overline{\Box} X) \,.$$

In this form this has been highlighted in (Bunke-Nikolaus-Völkl 13) in the context of our prop. below. See at differential hexagon for the proof.

Note that in the diagram we have also referred to the negative of a monadic moment, $\overline{\bigcirc} X$. We define this as follows:

Definition

The negative of a monadic moment $\bigcirc$ is the fiber of the unit map:

$$\overline{\bigcirc} X \coloneqq fib(X \to \bigcirc X) \,.$$

Accidence

Definition

Say that a moment $\bigcirc$, is exhibited by a type $J$ if $\bigcirc$ is equivalently $J$-homotopy localization

$$\bigcirc \simeq loc_{J} \,.$$

This implies in particular that $\bigcirc J \simeq \ast$.

Progression

We have seen how to formalize determination of qualities of types together with their opposite and their negative determination. But so far these determinations are abstract in that when interpreting them in models they could come out as all kinds of very different-natured (co-)monads. What is missing is something that bases these determinations on a concrete ground with respect to which they would gain actual meaning.

Indeed, there are natural ways in which determinations of qualities may progress from given ones to further ones: on the one hand a given unity of oppositions may itself have an opposite and hence exhibit a higher order “opposition of oppositions”, on the other hand a given unity of oppositions may be “resolved” inside one new quality, which then in turn may have its own opposite and negative in turn, and so on.

Progression I: Higher order opposition

Given a concrete particular moment (i.e. an interpretation of the moment in categorical semantics), then adjoints to it are a property of the moment, not a choice to made. Abstractly we may specify that moments proceed to further moments this way by positing further adjoints.

Definition

(opposition of unities of oppositions)

Given one opposition $\Box \dashv \bigcirc$, we say that on opposition of oppositions is a further left adjoint $\lozenge \dashv \Box$, which we may think of as constituting a system of adjoints of this form:

$$\array{ \lozenge &\overset{unity\;2}{\dashv}& \Box \\ \bot &\stackrel{opposition \atop {of\;unities}}{}& \bot \\ \Box &\underset{unity\;1}{\dashv}& \bigcirc } \,.$$

(Indeed, an adjoint triple is equivalently an adjunction of adjunctions, see here).

In principle this may go on, but in models one finds that there are essentially no examples with a fourth adjoint that do not degenerate to the ambidextrous situation where $\lozenge \simeq \bigcirc$.

This shows further how oppositions serve to further determine moments: while a bare $\Box$-operator has all kinds of unrelated interpretations in models, asking it to be in opposition with a $\bigcirc$-moment considerably constrains its possible interpretations, further asking it to participate in an opposition-of-oppositions constraints it much more still, and asking for yet one more opposition tends to overconstrain it such as to degenerate.

Progression II: Resolution of oppositions

There is another way for a system of moments to proceed, not by adding further oppositions, but by resolving them.

Definition

(resolution of unity of opposites)

Given an essential subtopos $\Box \dashv \bigcirc$ then one may ask if it sits inside a bigger essential subtopos, we write

$$\array{ \Box_2 &\dashv& \bigcirc_2 \\ \vee && \vee \\ \Box_1 &\dashv& \bigcirc_1 }$$

to indicate that the image of $\bigcirc_1$ is contained in the image of $\bigcirc_2$, and we say that $\bigcirc_2$ is at a higher level or in a higher sphere than $\bigcirc_1$.

If in addition $\Box_1 \lt \bigcirc_2$ then this means that the opposing moments of $\Box_1 \dashv \bigcirc_1$ both are of purely $\bigcirc_2$ nature, and hence we say that $\bigcirc_2$ resolves or lifts or sublates or is Aufhebung of this (unity of) oppostions. We might indicate this by:

$$\array{ \Box_2 &\dashv& \bigcirc_2 \\ \vee && \vee \\ \Box_1 & &\dashv& \bigcirc_1 }$$

Dually there may be Aufhebung of the form

$$\array{ & \Box_2 &\dashv& \bigcirc_2 \\ & \vee && \vee \\ \Box_1 &\dashv& & \bigcirc_1 }$$

Notice that for oppositions of the other form, given

$$\array{ \bigcirc_2 &\dashv& \Box_2 \\ \vee && \vee \\ \bigcirc_1 &\dashv& \Box_1 }$$

then resolution in the sense that $\bigcirc_2 \Box _1 \simeq \Box_1$ and $\Box_2 \bigcirc_1 \simeq \bigcirc_1$ is automatic.

These two kinds of progression, higher order opposition, def. , and resolution of oppositions, def. , may alternate to produce processes of oppositions of moments and of their resolutions of the form

$$\array{ \vdots &\dashv& \vdots \\ \bot && \bot \\ \lozenge_b &\dashv& \Box_b \\ \vee && \vee \\ \lozenge_a &\dashv& \Box_a \\ \bot && \bot \\ \Box_a &\dashv& \bigcirc_a }$$

Objective Logic

By the above discussion, we are led to add to homotopy type theory the axiom that there are various moments $\bigcirc$ or $\Box$. But which?

In the existing literature on modal logic it is tradition to consider unspecified idempotent (co-)monads to the formal system and have them acquire the intended meaning only via a specific choice of interpretation in a model. But here we are after developing genuine theory that works across all its possible interpretations, and hence we want an axiomatic determination of moments.

We observe now that there is a canonical starting point of two opposing moments that are secretly present in plain homotopy type theory. This hence constitutes a ground from which naturally a progression, as above, of determinations of further moments emanates.

The ground

The beginning

We observe now that in plain type theory already by itself carries one non-trivial unity of opposites.

There is the unit type $\ast$. As a concept, this is the concept with a unique instance (up to equivalence). As such this may be thought of as the concept of “pure being”: an instance of this concept just purely is, without having any further qualities, and hence two instances have no distinctions between them, both just purely are, nothing else, and so they are indistinguishlably the same.

Every type has a unique map $X\to \ast$ to that. Hence there is the monad which sends every type to $\ast$ and this is a moment

$$\bigcirc = \ast$$

according to def. .

Example

Every type is similar to every other, in the formal sense of def. , with respect to the $\ast$-moment. This says that all things are similar at least in that they are at all (§906).

Dually there is the empty type $\emptyset$. As a concept, this is the concept with no instance. As such this may be thought of as the concept of “not being”: since any instance of that concept would at least be (namely be an instance of the concept), but there is no such instance.

The empty type is such that it has a unique map $\emptyset \to X$ to any other type $X$, hence the comonad which sends every type to the empty type, and this is a moment

$$\Box = \emptyset \,.$$

It is immediate that:

Proposition

In plain homotopy type theory there is a unity of opposites, def. ,

$$\emptyset \dashv \ast \,.$$

We also call this the initial opposition.

Remark

It may be suggestive to think of this initial opposition in one of the following ways.

1. The initial opposition of prop. is (leaving context extension notationally implicit) the adjunction between dependent sum and dependent product over the context given by the empty type

   $$\underset{\emptyset}{\sum}(-) \;\vdash\; \underset{\emptyset}{\prod}(-) \,.$$

2. The initial opposition of prop. is the Cartesian product $\dashv$ internal hom-adjunction of the empty type

   $$\left( (-) \times \emptyset \right) \;\dashv\; \left( \emptyset \to (-) \right) \,.$$

On the other hand, the Cartesian product$\dashv$internal hom-adjunction of the unit type

$$\left( (-) \times \ast \right) \;\dashv\; \left( \ast \to (-) \right)$$

is the identity moment, in opposition with itself:

$$id \dashv \id \,.$$

This trivially resolves the initial opposition. Moreover, the negative, def. , of $id$ is $\ast$:

$$\overline{id} = \ast$$

So that we find

$$\array{ id &\dashv& id & = \overline{\ast} \\ \vee && \vee \\ \emptyset &\dashv& \ast & = \overline{id} } \,.$$

From this perspective it seems as if alternatively $(\id \dashv \id)$ could be referred to as the initial opposition.

Notice for completeness that the negative, def. , of $\emptyset$ is the maybe monad. (This is however not a moment in the sense of def. since it is not idempotent.)

Now we may find a progression of further moments by considering the resolution of this unity and then opposites to this resolution, and so forth.

Remark

Every essential subtopos level $\Box \dashv \bigcirc$ contains the initial opposition of prop. as the minimal one:

$$\array{ \Box &\dashv& \bigcirc \\ \vee && \vee \\ \emptyset &\dashv& \ast } \,.$$

Double negation

We are to demand that this provides a resolution, def. of the initial opposition $\empty \dashv \ast$, prop. , in that

$$\bigcirc \emptyset \simeq \emptyset \,.$$

In the categorical semantics this says equivalently that $(\Box \dashv \bigcirc)$ is a dense subtopos.

Proposition

The smallest dense subtopos of a topos is that of local types with respect to double negation $\sharp \coloneqq loc_{\neg \neg}$.

(Johnstone 02, corollary A4.5.20).

Therefore we may add the demand that the resolution of $(\emptyset \dashv \ast)$ be by $loc_{\neg \neg}$ (Lawvere 91, p. 8, Shulman 15). This equivalently means to demand that the double negation subtopos is essential .

Thus we have found the first step in the process by demanding resolution of the initial opposition. We will denote this by

$$\array{ \flat &\dashv& \sharp & = loc_{\neg \neg} \\ \vee && \vee \\ \emptyset &&\dashv& \ast }$$

Proposition

The double negation subtopos is Boolean topos.

(Johnstone 02, lemma A4.5.21)

This means that $(\flat \dashv \sharp)$ is naturally regarded as being the ground topos of the topos formed by the ambient type system, with the corresponding adjoint triple

$$\mathbf{H}_{\sharp} \stackrel{\hookrightarrow}{\stackrel{\stackrel{\Gamma}{\longleftarrow}}{\hookrightarrow}} \mathbf{H}$$

regarded as the termimal geometric morphism whose direct image $\Gamma$ forms global points (aka global sections).

Therefore we label the resolution of the initial opposition as “ground” for “ground topos”(base topos).

$$\array{ \flat &\dashv& \sharp & = loc_{\not\not} \\ \vee &\stackrel{ground}{}& \vee \\ \emptyset &\dashv& \ast } \,.$$

Cohesive substance

Quantity

This means then that $\flat$ is the operation of taking global points and regarding the collection of them as equipped with discrete structure. Hence $\flat$ is the moment of pure discreteness.

This in turn means that $\sharp$ is the moment of pure continuity (co-discreteness).

$$\array{ \stackrel{discreteness}{} & \flat &\dashv& \sharp &= loc_{\not\not}& \stackrel{continuity}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }$$

We may hence also say that $\flat X$ is the “point content” of $X$. If we regard the equivalence class of $\flat X$ then this is the cardinality of the point content of $X$, the Größe of the point content, the discrete quantity of $X$.

$$\array{ & && \flat && \stackrel{content}{} \\ & && \bot & \\ \stackrel{discreteness}{} & \flat &\dashv& \sharp & = loc_{\not \not}& \stackrel{continuity}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }$$

The types $X$ that are fully determined by their moment of continuity are those for which $X \to \sharp X$ is a monomorphism. In categorical semantics these are the concrete objects or equivalently the separated presheaves for $\sharp$: they are determined by their global points. These are the codomains of those functions which in thermodynamics one calls intensive quantities, functions whose value is genuinely given by their restriction to all possible points.

Contrary to that, objects which have purely the negative moment of continuity $\overline{\sharp}$ are codomains for “fuctions” which vanish on points and receive their contribution only from regions that extend beyond a single point. In thermodynamics these are called extensive quantities, (e.g. differential forms in positive degree). This concept of extension is precisely that which gave the name to Hermann Grassmann‘s Ausdehnungslehre that introduced the concept of exterior differential form.

In summary, we have found that $(\flat \dashv \sharp)$ expresses quantity, discrete quantity and continuous quantity, and that the latter is further subdivided into intensive and extensive quantity.

$$\array{ & && \flat & && \stackrel{content}{} \\ & && \bot & && \\ \stackrel{discrete}{} & \overline{\flat}/\flat &\stackrel{quantity}{\dashv}& \sharp & & & \stackrel{continuous\; (intensive/extensive)}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }$$

Quality

Proceeding, we next demand a second order opposition, def. , of the above opposition $(\flat \dashv \sharp)$, hence we posit a moment $ʃ$ such that

$$\array{ ʃ &\dashv& \flat \\ \bot && \bot \\ \flat &\dashv& \sharp } \,.$$

We ask this to have definite negation, def. . This means that

1. $ʃ \ast \simeq \ast$ — the shape of the point is trivial;

2. $\flat \to ʃ$ is epi on 0-types — the points-to-pieces transform is onto.

Together this are the axioms of cohesion as considered in (Lawvere 07). (There it is additionally asked that $ʃ$ preserves binary Cartesian products.)

The intuition is that positing these qualites on a type system makes it, or rather its types $X$, behave like a cohesive substance where points $\flat X$ are separate but held together by a cohesive attraction which, when the opposing repulsion is removed and only pure $ʃ$-moment is retained, makes them collapse to the components $ʃ X$.

The second clause here is closely related to $(\flat \dashv \sharp)$ providing Aufhebung for $(\emptyset \dashv \ast)$:

Proposition

If $\flat \to ʃ$ is epi on 0-types, then $\sharp \emptyset \simeq \emptyset$. Conversely, if $\sharp \emptyset \simeq \emptyset$ and $\mathbf{H}_{\sharp}$ is a Boolean topos, then $\flat \to ʃ$ is epi on 0-types.

(Lawvere-Menni 15, lemmas 4.1, 4.2).

In the more refined categorical semantics of homotopy toposes $\flat$ modulates locally constant infinity-stacks. The above adjunction then expresses the central statement of higher Galois theory (dcct):

$$\frac{X \to \flat Grpd_\infty}{ʃ X\to Grpd_\infty}$$

saying that locally constant $\infty$-stacks on $X$ are equivalent to infinity-permutation representations of $ʃ X$, and that $ʃ X$ therefore is the fundamental infinity-groupoid of $X$, the shape of $X$, both in the intuitive as well as in the technical sense of algebraic topology.

Therefore we further add labels as follows.

$$\array{ \stackrel{shape}{} && & ʃ &\stackrel{}{\dashv}& \flat & & & \stackrel{content}{} \\ && & \bot &\stackrel{}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

This means that in the presence of the further opposition $ʃ \dashv \flat$ the types $X$ which already had an underlying point content $\flat X$ now also have a shape determined by these points sticking together via a cohesive attraction. This is a qualitative aspect of the types in addition to their quantitative moments $\flat X$ and $\sharp X$.

Example

By remark the shape modality $ʃ$ determines a concept of similarity of types. This is a well known one: ʃ encodes that two types have the same shape. $X$ and $Y$ may look like different differential geometric spaces, but $(X \, similar_{ʃ} Y)$ holds if they have the same shape.

In the standard model given by smooth infinity-groupoids, discussed in some detail around theorem below there is for instance the circle $S^1$ and the cylinder $S^1 \times (0,1)$ over it, both regarded as smooth manifolds in the standard way. As such they are not equal (not diffeomorphic), but clearly they are similar in some sense. The shape modality makes one such sense precise: $ʃ (S^1) \simeq ʃ (S^1 \times (0,1) \simeq B \mathbb{Z}$ and hence

$$S^1 \, similar_{ʃ} \, (S^1 \times (0,1)) \,.$$

For instance there are now types for which $\flat X = \ast$ and yet they may be very different from the point $\ast$ themselves, hence while quantiatively these do not differ from the point, they must have some quality that distinguish them from the point. Hence this unity of opposites is geometric quality. In standard models this geometric quality is for instance topology or smooth structure or formal smooth structure or supergeometric structure.

Therefore we write:

$$\array{ \stackrel{shape}{} && & ʃ &\stackrel{quality}{\dashv}& \flat & & & \stackrel{content}{} \\ && & \bot &\stackrel{}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

Since with $(ʃ \dashv \sharp)$ we have arrived at an opposition of the form $(\bigcirc \dashv \Box)$, we should ask for further determination of these qualities by demanding via def. that $ʃ$ is exhibited by $\mathbb{R}$ (def. ):

$$ʃ = loc_{\mathbb{R}} \,.$$

In view of the above interpretation of $(ʃ\dashv \flat)$ via higher Galois theory, this comes with a clear meaning: this produces the A1-homotopy theory for $\mathbb{A}^1 = \mathbb{R}$. We may think of $\mathbb{R}$ as being the continuum, i.e. the real line which is the model for the geometric paths that make $ʃX$ be the fundamental infinity-groupoid of $X$.

Gauge (Measure)

With the concepts given by $(\flat \dashv \sharp)$ and by $(ʃ \dashv \flat)$ thus understood, it remains to find which concept the full unity of unities of opposites

$$\array{ ʃ &\dashv& \flat \\ \bot && \bot \\ \flat &\dashv& \sharp }$$

expresses.

Recall that the Brown representability theorem from stable homotopy theory:

Proposition

stable homotopy types$E$ are equivalently generalized cohomology theories $E^\bullet$ via

$$E^\bullet(X) = [X,S] \,.$$

Proposition

For the moments $(ʃ \dashv \flat)$ the exact hexagon of prop.

$$\array{ && \overline{ʃ} X && \stackrel{}{\longrightarrow} && \overline{\flat} X \\ & \nearrow & & \searrow & & \nearrow_{} && \searrow \\ \overline{ʃ} \flat X && && X && && ʃ \overline{\flat} X \\ & \searrow & & \nearrow & & \searrow && \nearrow_{} \\ && \flat X && \longrightarrow && ʃ X }$$

exhibits cohesive stable homotopy types $X$ as differential generalized cohomology theories.

Moreover, the existence of $\sharp$ means that the mapping stacks into these coefficients have differential concretification to moduli stacks of differential cocycles.

The first statement is the key insight in (Bunke-Nikolaus-Völkl 13). For more amplification of this point see at Differential cohomology is Cohesive homotopy theory.

Here the moments appearing in the hexagon have the following interpretation.

$$\array{ && {{connection\;forms}\atop{on\;trivial\;bundles}} && \stackrel{de\;Rham\;differential}{\longrightarrow} && {{curvature}\atop{forms}} \\ & \nearrow & & \searrow & & \nearrow_{\mathrlap{curvature}} && \searrow^{\mathrlap{de\;Rham\;theorem}} \\ {{flat}\atop{differential\;forms}} && && {{geometric\;bundles}\atop{with\;connection}} && && {{rationalized}\atop{bundle}} \\ & \searrow & & \nearrow & & \searrow^{\mathrlap{topol.\;class}} && \nearrow_{\mathrlap{Chern\;character}} \\ && {{geometric\;bundles}\atop{with\;flat\;connection}} && \underset{comparison/regulator\;map}{\longrightarrow} && {{shape}\atop{of\;bundle}} }$$

Now, cocycles in differential cohomology are the mathematical incarnation of physical fields in (stable) higher gauge theory (e.g. Freed 00). Hence the existence of the opposing moments $ʃ \dashv \flat \dashv \sharp$ means that types carry gauge measure.

From the gauge theoretic perpective the $\flat$-moment is that exhibited by flat infinity-connections, its negative $\overline{\flat}$ moment is that exhibited by infinity-connections given by just differential form data. For ordinary differential cohomology, differential K-theory etc. this is the “rational” aspect.

Hence in summary we have found determinations as follows.

$$\array{ \stackrel{shape}{} && loc_{\mathbb{R}} = & ʃ &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

Elastic substance

Étalé

Continuing the process, we posit a further opposition of moments lifting the previous ones.

$$\array{ \Im &\dashv& \& \\ \vee && \vee \\ ʃ &\dashv& \flat }$$

Since these are oppositions of the form $\bigcirc \dashv \Box$, Aufhebung is automatic here and not a further axiom.

To see what these new moments mean, observe that now

$$X \to \Im X \to ʃ X$$

is a factorization of the full shape projection through a finer approximation. Hence in addition to an intrinsic concept of path (a 1-morphism in the fundamental infinity-groupoid $ʃ X$) there is now an intrinsic concept of small path.

Accordingly, what were locally constant infinity-stacks in the higher Galois theory encoded by $\flat$ now become coverings that are constant on small scales. This is the concept of étale morphism as being a formally étale morphism with a condition of smallness on its fibers.

Hence we find that this further determination is that of the moment of being étalé.

$$\array{ \stackrel{infinitsimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} = & ʃ &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

Infinitesimal

Proceed by positing a further opposition $\Re \dashv \Im$.

To see what this moment means, observe that the “small shape” obtained above is representable by passing to pure $\Re$-moments

$$\frac{U \to \Im X}{\Re U \to X}$$

This has been understood in the 60s, in the context of crystalline cohomology, to be the characterization of paths that are so small that they are infinitesimal. The negative $Re$-moment is that of infinitesimal objects, the pure $\Re$-moment is that of “reduced objects” (“real” objects), those without infinitesimal extension.

In summary this gives:

$$\array{ \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\dashv& \Im & & & \\ && & \bot && \bot \\ \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} =& ʃ &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

More in detail, we may ask just how small these small paths are. Hence we demand more generally an infinite tower

$$ʃ \lt \Im = \Im_{(\infty)} \lt \cdots \lt \Im_{(3)} \lt \Im_{(2)} \lt \Im_{(1)} \lt id$$

of infinitesimal shape modalities, yielding a further factorization of the shape unit as

$$X \to \Im_{(1)}X \to \Im_{(2)}X \to \Im_{(3)} X \to \cdots \to \Im X \to ʃ X \,.$$

Differential

In total, so far these are the axioms of differential cohesion (dcct). Using these one may naturally axiomatize local diffeomorphism (def. below), jet bundles and related concepts.

Hence with these moments posited, types now now qualities of synthetic differential geometry. On top of just cohesively sticking to each other, the terms in the types now may feel a tighter differential connectedness, we have now a rigidly elastic substance.

Solid substance

Grading

Proceed to a new level of oppositions

$$\array{ \rightsquigarrow &\dashv& \R \\ \vee && \vee \\ \Re &\dashv& \Im } \,.$$

This gives for each type $X$ a factorization

$$\Re X \longrightarrow \stackrel{\rightsquigarrow}{X} \longrightarrow X$$

of the comparison map of the reduction modality $\Re$.

This hence means now that the purely $\rightsquigarrow$-types are in between reduced type and unreduced types, hence they are reduced in some sense, but possibly not properly. Hence there are now two kinds of infinitesimals, and the $\rightsquigarrow$-types have no extension by infinitesimals of one kind, but possibly infinitesimal extension of the other kind is left.

Hence there is now a kind of grading on the infinitesimals and $\rightsquigarrow$ quotients out everything not in degree 0.

The geometric quality of our formal substance that this encodes so far may hence be thought of as akin to Kapranov's noncommutative geometry, which is about ordinary spaces which however may have exotic noncommutative infinitesimal thickenings. We will find that the next two determinations in the progression of the moments refines this further to something of the quality of supergeometry, where the infinitesimal thickening satisfies some strong constraints.

Cyclic grading

The moments proceed by a further higher-oder opposition

$$\array{ \rightrightarrows &\dashv& \rightsquigarrow \\ \bot && \bot \\ \rightsquigarrow &\dashv& \R }$$

For this to have non-degenerate models one finds that infinitesimals in degree 0 must be allowed to map to products of infinitesimals in non-vanishing degree. This means that the grading is not by a free group, but for instance by a finite cyclic group $\mathbb{Z}/n\mathbb{Z}$-grading. The minimal choice is $\mathbb{Z}/2\mathbb{Z}$-grading.

Super

We are to require that this level provides Aufhebung of the previous oppositions, def. , in that

$$\stackrel{\rightsquigarrow}{\Im X} \simeq \Im X \,.$$

for all types $X$. By adjunction this means that

$$\Re \stackrel{\rightrightarrows}{U} \simeq \Re U$$

for a set of generators $U$, such as objects of a site.

This says that the reduced part of the even-graded part is the same as the reduced part of the original, hence that odd-grade is removed by reduction, hence that odd-graded moment is nilpotent. In superalgebra this is the key consequence of the super-sign rule (Hermann Grassmann, §37 in Ausdehnungslehre, 1844) which says that for odd coordinate functions $\theta_1$, $\theta_2$ we have

$$\theta_1 \theta_2 = -\theta_2 \theta_1 \,,$$

see prop. below.

Hence we think of the above Aufhebungs-condition as further determining the graded function algebras to actually be superalgebras.

By the Pauli exclusion principle/spin-statistics theorem, this is what characterizes fermions: the purely fermionic part is the negative moment $\overline{\rightsquigarrow}$.

We indicate this notationally by

$$\e \coloneqq \overline{\rightsquigarrow}$$

We may still further determine this, via def. , be requiring that there exists a type $\mathbb{R}^{0|1}$ which exhibits $\R$, in that $\R \simeq loc_{\mathbb{R}^{0|1}}$.

In summary we now have arrived at the following process of determinations.

$$\array{ && & \rightrightarrows &\dashv& \rightsquigarrow & / & \e & \stackrel{bosonic/fermionic}{} \\ && & \bot && \bot \\ && & \rightsquigarrow &\dashv& \R & = loc_{\mathbb{R}^{0|1}} \\ && & \vee &\stackrel{super}{}& \vee \\ \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\stackrel{}{\dashv}& \Im & & & \\ && & \bot && \bot \\ \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} =& ʃ &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} & \overline{\flat} & / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }$$

Prop. here gives a decomposition of types into their purely even-graded part and their purely fermionic part

$$\array{ && && && \stackrel{}{\e(X)} \\ & & & & & \nearrow_{} && \searrow \\ && && X && && \stackrel{\rightrightarrows}{\e(X)} \\ & & & & & \searrow && \nearrow_{} \\ && && && \stackrel{\rightrightarrows}{X} } \,.$$

A substance subject to the Pauli exclusion principle given by the above super-grading is yet more rigid than just by the elasticity we had before: it exhibits solidity.

$\,$

We conclude the process at this point. One may explore it further by continuing it with further resolutions and further oppositions, but for the applications to physics that we consider below the three stages beyond the ground that we have so far turn out to be sufficient.

Objectivity

It is a familiar tought in our age, in view of the intimate relation between physics and mathematics, that theories of physics have a natural mathematical formulation, that it is compelling to consider them also just from within mathematics itself. Famous examples include the formalization of classical mechanics by symplectic geometry, the formalization of Einstein gravity by pseudo-Riemannian geometry/Cartan geometry, the close relation of quantum mechanics and quantum field theory to representation theory (Wigner classification) and more recently the identification of local topological field theory with the theory of symmetric monoidal (infinity,n)-categories.

Hence while mathematics is part of the subjective logic in that it admits the freedom to consider any mathematical structure whatsoever, this suggests to identify among these the “objective” mathematical structures which are theories of physics and as such express a more objective reality than random mathematical structures do.

Classical mechanics (Mechanism)

Process

Given a logic of concepts as above, with its basic constructs of judgements of the form $f \colon X \to Y$, among the most natural structures to consider are correspondences, which go from a type $X_1$ to a type $X_2$ via an intermediate type $Y$ by maps

$$\array{ && Y \\ & {}^{\mathllap{i}}\swarrow && \searrow^{\mathrlap{o}} \\ X_1 && && X_2 } \,.$$

This is the immediate generalization of a relation as we pass from homotopy 0-types to general homotopy types and thereby allow monomorphisms to be replaced by general maps.

Now one observe that a correspondence is naturally interpreted as a process :

every instance/term $y\colon Y$ may be thought of as a process under which $i(y) \colon X_1$ turns into $o(y) \colon X_2$.

In traditional mathematical physics this is familiar from the concept of Lagrangian correspondences which serves to encoce much of classical mechanics.

Physical law

Or rather, classical mechanics is encoded by prequantized Lagrangian correspondences, the prequantization expressing the prequantum bundle, an action functional and hence the laws of motion.

By the discussion there, a prequantized Lagrangian correspondence is itself again just a correspondence, but now in context, hence between dependent types, namely depending on a type of phases.

A detailed discussion of how classical field theory is formalized via correspondences in cohesive homotopy type theory in the context of a type of phases is at

• Classical field theory via Cohesive homotopy types.

From the dicussion there one finds a picture of sliced correspondences interpreted as classical mechanics as follows.

$$\array{ && {{space\,of} \atop {trajectories}} \\ & {}^{\mathllap{{initial}\atop {values}}}\swarrow && \searrow^{\mathrlap{{Hamiltonian} \atop {evolution}}} \\ {{phase\,space} \atop {incoming}} && \swArrow_{{action} \atop {functional}} && {{phase\,space} \atop {outgoing}} \\ & {}_{\mathllap{{prequantum}\atop {bundle}_{in}}}\searrow && \swarrow_{\mathrlap{{prequantum} \atop {bundle}_{out}}} \\ && {{2-group} \atop {of\,phases}} } \,.$$

Quantum mechanics ((quantum-)Chemism)

Recall from remark that the initial opposition gave rise also to the maybe monad, as the negative of the empty moment: $\overline{\empty} = maybe$.

The negative of $\id$ is $\ast$.

The opposite of $\ast$ is $\empty$.

The negative of $\empty$ is $maybe$.

While $maybe$ is not idempotent, by remark we may still ask for the types which are pure with respect to it in that they they are objects in its Eilenberg-Moore category. These are precisely the pointed types.

On pointed types the smash product yields a symmetric monoidal structure which is not Cartesian, and we enter the realm of linear type theory in the generality of dependent linear type theory. As discussed there, dependent sum and dependent product here now naturally yield the concept of secondary integral transforms, across correspondences, which in view of the above interpretation of correspondences as spaces of trajectories are really path integrals. Developing this one finds that correspondences in linear homotopy type theory give rise to formalization of quantization and quantum mechanics.

For details see at Quantization via Linear homotopy types.

Boundary conditions (Teleology)

In this context a boundary condition is given by a (prequantized) correspondence which on one end is just the unit type

$$\array{ && Y \\ & {}^{\mathllap{b}}\swarrow && \searrow^{\mathrlap{o}} \\ \ast && && X } \,.$$

For more on this see at

• Cohomological quantization of local prequantum boundary field theory

• Local prequantum field theory

• Quantization via Linear homotopy types

The idea

Including in homotopy type theory the progression of modal operators that we have found above

$$\array{ &&& && & id &\dashv& id \\ &&& && & \vee && \vee \\ &&& && & \rightrightarrows &\dashv& \rightsquigarrow & / & \e & \stackrel{bosonic/fermionic}{} \\ \stackrel{solidity}{} &&& && & \bot && \bot \\ &&& && & \rightsquigarrow &\dashv& \R & = loc_{\mathbb{R}^{0\vert 1}}& & \stackrel{rheonomic}{} \\ &&& && & \vee &\stackrel{super}{}& \vee \\ &&& \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\dashv& \Im & & & \\ \stackrel{elasticity}{} &&& && & \bot && \bot \\ &&& \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ &&& && & \vee && \vee \\ &&& \stackrel{shape}{} && loc_{\mathbb{R}} = &ʃ &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ \stackrel{cohesion}{} &&& && & \bot &\stackrel{gauge\;measure}{}& \bot \\ &&& \stackrel{discrete}{} &\overline{\flat} & / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ &&& && & \vee &\stackrel{ground}{}& \vee \\ &&& && & \emptyset &\dashv& \ast & }$$

makes its term model richer: there are now true propositions and generally terms that may be constructed which are not constructible in plain homotopy type theory. These terms reflect the idea that is induced by these determinations, in that every interpretation of this modal type theory has to realize (externalize) these terms and make these propositions true.

We now indicate some of these new constructions.

Maurer-Cartan forms

Let $G$ be a an ∞-group type. This means that there is specified a pointed connected type $\mathbf{B}G$ and an equivalence $G\simeq \Omega \mathbf{B}G$ with its loop space object. We say that $\mathbf{B}G$ is the delooping of $G$. Notice that all this happens internal to the ambient cohesive homotopy type theory, which makes $\mathbf{B}G$ have the interpretation of the moduli ∞-stack of cohesive $G$-principal ∞-bundles, instead of just the bare homotopy type of the classifying space

$$B G \simeq ʃ \mathbf{B}G \,.$$

This richer geometric structure is what the boldface in $\mathbf{B}G$ is meant to remind us of.

Definition

Denote the first and second homotopy fiber of the comparison map $\flat \mathbf{B}\mathbb{G} \to \mathbf{B}\mathbb{G}$ of the flat moment of this as follows.

$$G \stackrel{\theta_G}{\longrightarrow} \flat_{dR}\mathbf{B}G \longrightarrow \flat \mathbf{B}G \longrightarrow \mathbf{B}G \,.$$

This double homotopy fiber $\theta_G$ has the interpretation of being the Maurer-Cartan form on $G$.

Differential cohomology

Let $\mathbb{G}$ be an abelian ∞-group type. The group of phases.

This being abelian just means that there is specified a delooping type $\mathbf{B} \mathbb{G}$ and an equivalence $\mathbb{G}\simeq \Omega \mathbf{B} \mathbb{G}$ with its loop space object, and that with $\mathbf{B}^0 \mathbb{G} \coloneqq \mathbb{G}$ we have inductively that $\mathbf{B}^n \mathbb{G}$ is itself equipped with the structure of an abelian ∞-group.

For the present purpose we will assume in addition that $\mathbb{G}$ is 0-truncated, which makes it simply an abelian group.

Definition

A Hodge filtration is a compatible system of filtrations of $\flat \mathbf{B}^2\mathbb{G}$ of the form

$$\mathbf{\Omega}^{2}_{cl} \to \cdots \to \flat_{dR} \mathbf{B}^2 \mathbb{G} \to \flat \mathbf{B}^2 \mathbb{G} \,.$$

with 0-truncated extensive $\mathbf{\Omega}^{2}_{cl}$.

Definition

Given a Hodge filtration, write $\mathbf{B}\mathbb{G}_{conn}$ for the homotopy fiber product

$$\mathbf{B}\mathbb{G}_{conn} \coloneqq \mathbf{B}\mathbb{G}\underset{\flat_{dR}\mathbf{B}^2\mathbb{G}}{\times} \mathbf{\Omega}^2_{cl}$$

of the Maurer-Cartan form $\theta_{\mathbf{B}\mathbb{G}}$ with the last Holdge filtration stage.

Proposition

The decomposition of $\mathbf{B}\mathbb{G}_{conn}$ into its $(ʃ, \overline{\flat})$-moments according to prop reproduces the defining Cartesian sqare of def. :

$$\array{ && \mathbf{\Omega}^2_{cl} \\ & \nearrow && \searrow \\ \mathbf{B}\mathbb{G}_{conn} && && \flat_{dR}\mathbf{B}^2\mathbb{G} \\ & \searrow && \nearrow && \searrow \\ && \mathbf{B}\mathbb{G} && && \flat_{dR}B \mathbb{G} \\ && & \searrow && \nearrow \\ && && B \mathbb{G} }$$

WZW terms

A map

$$\mathbf{c} \colon \mathbf{B}G \longrightarrow \mathbf{B}^{p+2} \mathbb{G}$$

is equivalently a cocycle of degree $p+2$ in the group cohomology of $G$.

Definition

Given a group cocycle $\mathbf{c}$ and a Hodge filtration, then a refinement of the Hodge filtration along the group cocycle is a chose of 0-trucated extensive $\mathbf{\Omega}^1_{flat}(-,\mathfrak{g})$ fitting into a square

$$\array{ \mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) &\stackrel{\mu}{\longrightarrow}& \mathbf{\Omega}^2_{cl} \\ \downarrow && \downarrow \\ \flat_{dR} \mathbf{B}G &\stackrel{\flat_{dR}\mathbf{c}}{\longrightarrow}& \flat_{dR} \mathbf{B}^2 \mathbb{G} } \,.$$

Given this, write

$$\tilde G \coloneqq G \underset{\flat_{dR}\mathbf{B}G}{\times} \mathbf{\Omega}^1_{flat}(-,\mathfrak{g})$$

Example

For $G$ 0-truncated, then the canonical choice is $\mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) = \flat_{dR}\mathbf{B}G$. With this one has $\tilde G \simeq G$.

On the other extreme, for $G = \mathbf{B}^{p+1}\mathbb{G}$ then the canonical choice is $\mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) = \mathbf{\Omega}^{p+2}_{cl}$. With this one has $\tilde G \simeq \mathbf{B}^{p+1}\mathbb{G}_{conn}$.

This means that in general $\tilde G$ is a homotopy fiber product of $G$ with $\mathbf{B}^{p+1}\mathbb{G}_{conn}$, hence that a map to out of some $\Sigma$ is a pair of a map $\Sigma \to G$ and of $(p+1)$-form data on $\Sigma$. This is the kind of field content of higher gauged WZW models.

Proposition

Given a group cocycle $\mathbf{c} \colon \mathbf{B}G \to \mathbf{B}^{p+2}$ and a form refinement $\mu$ as in def. , then there exists an essentially unique prequantization

$$\mathbf{L}_{WZW} \;\colon\; \tilde G \longrightarrow \mathbf{B}^{p+1}_{conn}$$

of $\mu(\theta_G)$ whose underlying $\mathbf{B}^p\mathbb{G}$-principal ∞-bundle is $\Omega \mathbf{c}$.

We call this the WZW term whose curvature is $\mu(\theta_G)$.

$V$-Manifolds

See also at geometry of physics – manifolds and orbifolds.

Definition

Given $X,Y\in \mathbf{H}$ then a morphism $f \;\colon\; X\longrightarrow Y$ is a local diffeomorphism if its naturality square of the infinitesimal shape modality

$$\array{ X &\longrightarrow& \Im X \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}} \\ Y &\longrightarrow& \Im Y }$$

is a pullback square.

Remark

The abstract definition comes down to being the appropriate synthetic differential supergeometry-version of the traditional statement that $f$ is a local diffeomorphism if the diagram of tangent bundles

$$\array{ T X &\longrightarrow& X \\ \downarrow^{\mathrlap{T f}} && \downarrow^{\mathrlap{f}} \\ T Y &\longrightarrow& Y }$$

To see this, notice by the discussion at synthetic differential geometry that for $D$ an infinitesimally thickened point, then for any $X \in \mathbf{H}$ the mapping space $[D,X]$ is the jet bundle of $X$ with jets of order as encoded by the infinitesimal order of $D$. In particular if $\mathbb{D}^1(1)$ is the first order infinitesimal interval defined by the fact that its algebra of functions is the algebra of dual numbers $C^\infty(\mathbb{D}^1(1)) = (\mathbb{R} \oplus \epsilon \mathbb{R})/(\epsilon^2)$, and $X$ is a smooth manifold, then

$$[\mathbb{D}^1(1), X]\simeq T X$$

is the ordinary tangent bundle of $X$. Now use that the internal hom $[D,-]$ preserves limits in its second argument, and that, by the hom-adjunction, $\mathbf{H}(U, [D,X]) \simeq \mathbf{H}(U \times D, X)$ and finally use that $\mathbf{H}(U \times D, \Im X)\simeq \mathbf{H}(\Re(U \times D), X)\simeq \mathbf{H}(U,X)$.

Let now $V \in \mathbf{H}$ be given, equipped with the structure of a group (infinity-group).

Definition

A $V$-manifold is an $X \in \mathbf{H}$ such that there exists a $V$-atlas, namely a correspondence of the form

$$\array{ && U \\ & \swarrow && \searrow \\ V && && X }$$

with both morphisms being local diffeomorphisms, def. , and the right one in addition being an epimorphism, hence an atlas.

Proposition

If $f \;\colon\; X \longrightarrow Y$ is a local diffeomorphism, def. , then so is image $\stackrel{\rightsquigarrow}{f}\colon \stackrel{\rightsquigarrow}{X} \longrightarrow \stackrel{\rightsquigarrow}{Y}$ under the bosonic modality.

Proof

Since the bosonic modality provides Aufhebung for $\Re\dashv \Im$ we have $\rightsquigarrow \Im \simeq \Im$. Moreover $\Im \rightsquigarrow \simeq \Im$ anyway. Finally $\rightsquigarrow$ preserves pullbacks (being in particular a right adjoint). Hence hitting a pullback diagram

$$\array{ X &\longrightarrow& \Im X \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}} \\ Y &\longrightarrow& \Im Y }$$

with $\rightsquigarrow\;\;$ yields a pullback diagram

$$\array{ \stackrel{\rightsquigarrow}{X} &\longrightarrow& \Im \stackrel{\rightsquigarrow}{X} \\ \downarrow^{\mathrlap{\stackrel{\rightsquigarrow}{f}}} && \downarrow^{\mathrlap{\Im \stackrel{\rightsquigarrow}{f}}} \\ \stackrel{\rightsquigarrow}{Y} &\longrightarrow& \Im \stackrel{\rightsquigarrow}{Y} }$$

Corollary

The bosonic space $\stackrel{\rightsquigarrow}{X}$ underlying a $V$-manifold $X$, def. , is a $\stackrel{\rightsquigarrow}{V}$-manifold

Frame bundles

Definition

Given $X \in \mathbf{H}$, its infinitesimal disk bundle $T_{inf} X\to X$ is the pullback of the unit of the infinitesimal shape modality along itself

$$\array{ T_{inf} X &\stackrel{}{\longrightarrow}& X \\ \downarrow && \downarrow \\ X &\longrightarrow& \Im X } \,.$$

Given a point $x \;\colon\; \ast \to X$, then the infinitesimal neighbourhood $\ast \to \mathbb{D}_x \to X$ of that point is the further pullback of the infinitesimal disk bundle to this point:

$$\array{ \mathbb{D}_x &\longrightarrow & T_{inf} X &\stackrel{}{\longrightarrow}& X \\ \downarrow && \downarrow && \downarrow \\ \ast &\stackrel{x}{\longrightarrow} & X &\longrightarrow& \Im X } \,.$$

More generally, for $k \in \mathbb{N}$ then the $k$th order infinitesimal disk bundle is

$$\array{ T_{(k)} X &\stackrel{}{\longrightarrow}& \Im_{(k)} X \\ \downarrow && \downarrow \\ X &\longrightarrow& \Im X }$$

and accordingly the $k$th order infinitsimal neighbourhood is

$$\array{ \mathbb{D}(k)_x &\longrightarrow & T_{(k)} X &\stackrel{}{\longrightarrow}& \Im_{(k)}X \\ \downarrow && \downarrow && \downarrow \\ \ast &\stackrel{x}{\longrightarrow} & X &\longrightarrow& \Im X } \,.$$

It is natural not to pick any point, but to collect all infinitesimal disks around all the points of a space:

Definition

The relative flat modality is the operation $\flat^{rel}$ that sends $X \in \mathbf{H}$ to the homotopy pullback

$$\array{ \flat^{rel} &\longrightarrow& X \\ \downarrow && \downarrow \\ \flat X &\longrightarrow& \Im X } \,.$$

More generally, for any $k \in \mathbb{N}$ then the order $k$ relative flat modality is the pullback in

$$\array{ \flat^{rel}_{(k)} &\longrightarrow& \Im_{(k)} X \\ \downarrow && \downarrow \\ \flat X &\longrightarrow& \Im X } \,.$$

Definition

The general linear group $GL(V)$ is the automorphism infinity-group of the infinitesimal neighbourhood $\mathbb{D}^V_e$, def. , of the neutral element $e \colon \ast \to \mathbb{D}^V_e \to V$:

$$GL(V) \coloneqq \mathbf{Aut}(\mathbb{D}^V_e) \,.$$

Proposition

For $X$ a $V$-manifold, def. , then its infinitesimal disk bundle $T_{inf} X \to X$, def. , is associated to a $GL(V)$-principal $Fr(X) \to X$ – to be called the frame bundle, modulated by a map to be called $\tau_X$, producing homotopy pullbacks of the form

$$\array{ T_{inf} X &\longrightarrow& V/GL(V) \\ \downarrow && \downarrow \\ X &\stackrel{\tau_X}{\longrightarrow}& \mathbf{B} GL(V) } \;\;\; \array{ Fr(X) &\longrightarrow& \ast \\ \downarrow && \downarrow \\ X &\stackrel{\tau_X}{\longrightarrow}& \mathbf{B} GL(V) } \,.$$

Definition

A framing of a $V$-manifold is a trivialization of its frame bundle, prop. , hence a diagram in $\mathbf{H}$ of the form

$$\array{ X && \longrightarrow && \ast \\ & \searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(V) }$$

Remark

It is useful to express def. in terms of the slice topos $\mathbf{H}_{/\mathbf{B}GL(V)}$. Write $V\mathbf{Frame}\in \mathbf{H}_{/\mathbf{B}GL(V)}$ for the canonical morphism $\ast \to \mathbf{B}GL(V)$ regarded as an object in the slice. Then a framing as in def. is equivalently a morphism

$$\phi \colon \tau_X \longrightarrow V\mathbf{Frame}$$

in $\mathbf{H}_{/\mathbf{B}GL(V)}$.

Proposition

The group object $V$, canonically regarded as a $V$-manifold, carries a canonical framing, def. , $\phi_{li}$, induced by left translation.

$G$-Structure

See also at geometry of physics – G-structure and Cartan geometry.

Definition

Given a homomorphism of groups $G \longrightarrow GL(V)$, a G-structure on a $V$-manifold $X$ is a lift $\mathbf{c}$ of the frame bundle $\tau_X$ of prop. through this map

$$\array{ X && \stackrel{}{\longrightarrow} && G \\ & {}_{\mathllap{\tau_X}}\searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(V) } \,.$$

Remark

As in remark , it is useful to express def. in terms of the slice topos $\mathbf{H}_{/\mathbf{B}GL(V)}$. Write $G\mathbf{Struc}\in \mathbf{H}_{/\mathbf{B}GL(V)}$ for the given map $\mathbf{B}G\to \mathbf{B}GL(V)$ regarded as an object in the slice. Then a $G$-structure according to def. is equivalently a choice of morphism in $\mathbf{H}_{/\mathbf{B}GL(V)}$ of the form

$$\mathbf{c} \;\colon\; \tau_X \longrightarrow G\mathbf{Struc} \,.$$

In other words, $G\mathbf{Struc} \in \mathbf{H}_{/\mathbf{B}GL(v)}$ is the moduli stack for $G$-structures.

Example

A choice of framing $\phi$, def. , on a $V$-manifold $X$ induces a G-structure for any $G$, given by the pasting diagram in $\mathbf{H}$

$$\array{ X &\longrightarrow& \ast &\longrightarrow& \\ & \searrow & \downarrow & \swarrow \\ && \mathbf{B}GL(V) }$$

or equivalently, via remark and remark , given as the composition

$$\mathbf{c}_{li} \;\colon\; \tau_X \stackrel{\phi}{\longrightarrow} V\mathbf{Frame} \longrightarrow G\mathbf{Struc}\,.$$

We call this the left invariant $G$-structure.

Definition

For $X$ a $V$-manifold, then a G-structure on $X$, def. , is integrable if for any $V$-atlas $V \leftarrow U \rightarrow X$ the pullback of the $G$-structure on $X$ to $V$ is equivalent there to the left-inavariant $G$-structure on $V$ of example , i.e. if we have an correspondence in the double slice topos $(\mathbf{H}_{/\mathbf{B}GL(V)})_{/G\mathbf{Struc}}$ of the form

$$\array{ && \tau_U \\ & \swarrow && \searrow \\ \tau_V && \swArrow && \tau_X \\ & {}_{\mathllap{\mathbf{c}_{li}}}\searrow && \swarrow_{\mathrlap{\mathbf{c}}} \\ && G \mathbf{Struc} } \,.$$

The $G$-structure is infintesimally integrable if this holds true after restriction along the relative shape modality $\flat^{rel} U \to U$, def. , to all the infinitesimal disks in $U$:

$$\array{ && \tau_{\flat^{rel}U} \\ & \swarrow && \searrow \\ \tau_V && \swArrow && \tau_X \\ & {}_{\mathllap{\mathbf{c}_{li}}}\searrow && \swarrow_{\mathrlap{\mathbf{c}}} \\ && G \mathbf{Struc} } \,.$$

Finally, the $G$-structure is order $k$ infinitesimally integrable if this holds for the order-$k$ relative shape modality $\flat^{rel}_{(k)}$.

Definition

Consider an infinity-action of $GL(V)$ on $V$ which linearizes to the canonical $GL(V)$-action on $\mathbb{D}^V_e$ by def. . Form the semidirect product $GL(V) \rtimes V$. Consider any group homomorphism $G\to GL(V)$.

A $(G\to G\rtimes V)$-Cartan geometry is a $V$-manifold $X$ equipped with a $G$-structure, def. . The Cartan geometry is called (infinitesimally) integrable if the $G$-structure is so, according to def. .

Remark

For $V$ an abelian group, then in traditional contexts the infinitesimal integrability of def. comes down to the torsion of a G-structure vanishing. But for $V$ a nonabelian group, this definition instead enforces that the torsion is on each infinitesimal disk the intrinsic left-invariant torsion of $V$ itself.

Traditionally this is rarely considered, matching the fact that ordinary vector spaces, regarded as translation groups $V$, are abelian groups. But super vector spaces regarded (in suitable dimension) as super translation groups are nonabelian groups. Therefore super-vector spaces $V$ may carry intrinsic torsion, and therefore first-order integrable $G$-structures on $V$-manifolds are torsion-ful.

Indeed, this is a phenomenon known as the torsion constraints in supergravity. Curiously, as discussed there, for the case of 11-dimensional supergravity the equations of motion of the gravity theory are equivalent to the super-Cartan geometry satisfying this torsion constraint. This way super-Cartan geometry gives a direct general abstract route right into the heart of M-theory.

Definite forms

Definition

Given a group cocycle $\mathbf{c} \colon \mathbf{B}G\to\mathbf{B}^{p+2}\mathbb{G}$ with WZW term, prop. , of the form

$$\mathbf{L}_{WZW}^V \colon V \longrightarrow \mathbf{B}^{p+1}\mathbb{G}$$

and given a $V$-manifold $X$ we say that an integrable globalization of $\mathbf{L}_{WZW}^V$ over $X$ is a WZW on on $X$

$$\mathbf{L}_{WZW}^X \;\colon\;X \longrightarrow \mathbf{B}^{p+1}\mathbb{G}_{conn}$$

such that there is a $V$-atlas for $X$

$$\array{ && U \\ & \swarrow && \searrow \\ V && && X }$$

which extends to a correspondence between $\mathbf{L}_{WZW}$ and $\mathbf{L}_{WZW}^X$

$$\array{ && U \\ & \swarrow && \searrow \\ V && \swArrow && X \\ & {}_{\mathllap{\mathbf{L}_{WZW}^V}}\searrow && \swarrow_{\mathrlap{\mathbf{L}_{WZW}^X}} \\ && \mathbf{B}^{p+1}\mathbb{G}_{conn} } \,.$$

Accordingly, as in def. we say that $\mathbf{L}_{WZW}^X$ is an infinitesimally integrable globalization if this correspondence exists after restriction along the inclusion $\flat^{rel} U \to U$ of the infinitesimal disks in $X$ and such that

1. the induced section of the associated $[\mathbb{D}(1)^V,\mathbf{B}^{p+1}\mathbb{G}_{conn}]$-fiber infinity-bundle is definite on the restriction $\mathbf{L}_{WZW}^{\mathbb{D}}$ of $\mathbf{L}_{WZW}^V$ to the infinitesimal disk;

2. also the underlying cocycle is definite, in that the infinitesimal disk bundle lifts to an $\mathbb{D}^V(1)$-gerbe (for the induced group structure on $\mathbb{D}^V(1)$).

If $\mathbf{B}^{p+1}\mathbb{G}_{conn}$ had no higher gauge transformations, then this would already ensure that such a globalization globalizes $\mathbf{L}_{WZW}^V$ locally cohesively, but here in higher differential geometry this property becomes genuine structure and hence we need to demand it. There is an axiomatic way to say this (see dcct for details) and if this is imposed then we say that $\mathbf{L}_{WZW}^X$ is a definite globalization of $\mathbf{L}_{WZW}^V$.

Proposition

There is a canonical (∞,1)-functor from (infinitesimally integrable) definite globalizations of $\mathbf{L}_{WZW}^X$ over a $V$-manifold $X$ to (infinitesimally integrable) $G$-structures on $X$, def. , for

$$G = intens(\mathbf{Stab}_{GL(V)}(\mathbf{L}_{WZW}^{\mathbb{D}^V}))$$

the intensification (in the sense above) of the stabilizer ∞-group of the restriction of $\mathbf{L}_{WZW}^V$ along the inclusion of the typical infinitesimal disk $\mathbb{D}^V \to V$.

Nature

Given a theory of physics, made sufficiently precise in formal logic, then an interpretation of the theory by a model “is” nature as predicted by this theory.

For instance if we considered Einstein gravity to be the theory of pseudo-Riemannian manifolds subject to some energy condition, then a model for this theory is one concrete particular spacetime.

Above we saw that cohesive (elastic) homotopy type theory contains Cartan geometry, hence in particular pseudo-Riemannian geometry in its idea, as well as gauge theory and hence we accordingly find models of nature here.

Recall specifically that

1. From prop. we have that group cocycles $\mathbf{c}\colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G}$ of degree $p+2$ induce WZW terms in that degree and hence the WZW sigma model prequantum field theory on the worldvolume of a p-brane propagating on the “model spacetime” $V$.

2. A second cocycle on the infinity-group extension classified by $\mathbf{c}$ yields a type of $\tilde p$-brane on which these $p$-branes may end;

3. This structure is naturally generalized to $V$-manifolds $X$ equipped with definite globalizations of these WZW terms, defining $p$-branes propagating on $X$.

4. The definite globalization of the WZW term $\mathbf{L}_{\mathrm{WZW}}$ induces a $Stab(\mathbf{L}_{WZW})$ structure on $X$ and the requirement that this be infinitesimally integrable is a torsion constraint on $X$.

We now find an externalization of the idea such that

1. There is a canonical bouquet of higher group cocycles and their ∞-group extensions emanating from the unique 0-truncated purely fermionic type – the superpoint.

2. The resulting branes and their intersection laws are those seen in string theory;

3. The resulting spacetimes are superspacetimes as in the relevant supergravity theories;

4. The resulting torsion constraints, namely the supergravity torsion constraints, imply, in the maximally extended situation, the Einstein equations of motion of 11-dimensional supergravity, specifically of d=4 N=1 supergravity arising in the guise of M-theory on G2-manifolds.

This is a “theory of everything” in the sense of modern fundamental physics, which is beeing argued to have viable phenomenology, see at G2-MSSM for more on this. Even if it turns out that there are no models in this theory which match quantitative measurements in experiment, it is noteworthy that the qualitative structure of this theory is that of Einstein-Yang-Mills-Dirac-Higgs theory and hence matches faithfully the qualitative features of nature that is in experiment. Given our starting point above this is maybe not to be lightly dismissed.

Externalization

Theorem

The cohesive+elastic+solid homotopy type theory above has a faithful (i.e. non-degenerate) categorical semantics in the homotopy topos $SuperFormalSmooth\infty Grpd$ of super formal smooth infinity-groupoids.

We now spell out the construction of this model and indicate the proof of this statement.

Definition

Write

• CartSp for the site of Cartesian spaces;

• $InfPoint \coloneqq WAlg^{op}$ for the category of first-order infinitesimally thickened points (i.e. the formal duals of commutative algebras over the real numbers of the form $\mathbb{R}\oplus V$ with $V$ a finite-dimensional square-0 nilpotent ideal).

• $SuperPoint \coloneqq WAlg_{super}^{op}$ for the category of superpoints, by which we here mean the formal duals to commutative superalgebras which are super-Weil algebras.

There are then “semidirect product” sites $CartSp \rtimes InfinPoint$ and $CartSp \rtimes SuperPoint$ (whose objects are Cartesian products of the given form inside synthetic differential supergeometry and whose morphisms are all morphisms in that context (not just the product morphisms)).

Set then

$$Smooth \infty Grpd \coloneqq Sh_\infty(CartSp)$$

for the collection of smooth ∞-groupoids;

$$FormalSmooth\infty Grpd \coloneqq Sh_\infty(CartSp \rtimes InfPoint)$$

for the collection of formal smooth ∞-groupoids (see there) and finally

$$SuperFormalSmooth\infty Grpd \coloneqq Sh_\infty(CartSp \rtimes SuperPoint)$$

for that of super formal smooth ∞-groupoids.

Proposition

The sites in question are alternatingly (co-)reflective subcategories of each other (we always display left adjoints above their right adjoints)

$$\ast \stackrel{\longleftarrow}{\hookrightarrow} CartSp \stackrel{\hookrightarrow}{\longleftarrow} CartSp\rtimes InfPoint \stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}} CartSp \rtimes SuperPoint \,.$$

Here

• the first inclusion picks the terminal object $\mathbb{R}^0$;

• the second inclusion is that of reduced objects; the coreflection is reduction, sending an algebra to its reduced algebra;

• the third inclusion is that of even-graded algebras, the reflection sends a $\mathbb{Z}_2$-graded algebra to its even-graded part, the co-reflection sends a $\mathbb{Z}_2$-graded algebra to its quotient by the ideal generated by its odd part, see at superalgebra – Adjoints to the inclusion of plain algebras.

Passing to (∞,1)-categories of (∞,1)-sheaves, this yields, via (∞,1)-Kan extension, a sequence of adjoint quadruples as follows:

$$\array{ & && && &\longleftarrow& \\ & && &\hookrightarrow& &\hookrightarrow& \\ & &\longleftarrow& &\longleftarrow& &\longleftarrow& \\ \Delta \colon & \infty Grpd &\hookrightarrow& Smooth \infty Grpd &\hookrightarrow& FormalSmooth \infty Grpd &\hookrightarrow& SuperFormalSmooth \infty Grpd \\ & &\longleftarrow& &\longleftarrow& \\ & &\hookrightarrow& }$$

the total composite labeled $\Delta$ is indeed the locally constant infinity-stack-functor.

Forming adjoint triples from these adjoint quadruples gives idempotent (co-)monads

$$ʃ \dashv \flat \dashv \ast$$

$$\Re \dashv \Im \dashv \&$$

$$\rightrightarrows \dashv \rightsquigarrow \dashv \Re$$

satisfying the required inclusions of their images.

Proof

All the sites are ∞-cohesive sites, which gives that we have an cohesive (infinity,1)-topos. The composite inclusion on the right is an ∞-cohesive neighbourhood site, whence the inclusion $Smooth\infty Gpd\hookrightarrow SuperFormalSmooth\infty Grpd$ exhibits differential cohesion.

With this the rightmost adjoint quadruple gives the Aufhebung of $\Re \dashv \Im$ by $\rightsquigarrow \dashv \R$ and the further opposition $\rightrightarrows \dashv \rightsquigarrow$.

Remark

The model in def. admits also the refinement of the infinitesimal shape modality to an infinite tower

$$ʃ \lt \Im = \Im_{(\infty)} \lt \cdots \lt \Im_{(3)} \lt \Im_{(2)} \lt \Im_{(1)} \lt id$$

characterizing $k$th order infinitesimals. Let

$$\ast = InfPoint_{(0)} \hookrightarrow InfPoint_{(1)} \hookrightarrow InfPoint_{(2)} \hookrightarrow InfPoint_{(3)} \hookrightarrow \cdots InfPoint$$

be the stratification of $InfPoint$ by its full subcategories on those objects whose coresponding Weil algebras/local Artin algebras are of the form $\mathbb{R} \oplus V$ with $V^k = 0$. Each of these inclusions has coreflection, given by projection onto the quotient by the ideal $V^k$, as $k$ ranges

Proposition

The model in def. verifies the required determinate negations

1. determinate negations I:

   • $ʃ \ast \simeq \ast$;

   • $\flat \to ʃ$ is epi restricted to 0-types;

2. determinate negations II:

   • $ʃ \simeq loc_{\mathbb{R}}$ for $\mathbb{R} \in SmoothMfd \hookrightarrow SuperFormalSmooth\infty Grpd$ the ordinary real line;

   • $\R \simeq loc_{\mathbb{R}^{0|1}}$ for $\mathbb{R}^{0|1} \in SuperMfd \hookrightarrow SuperFormalSmooth\infty Grpd$ the odd line.

Proof

The first two items follow with the discussion at ∞-cohesive site. The second two by dcct, prop. 5.2.51.

Proposition

The model in def. verfies the required Aufhebungen

1. $\sharp \emptyset \simeq \emptyset$;

2. $\rightsquigarrow \Im \simeq \Im$.

Proof

For the statement $\sharp \emptyset \simeq \emptyset$ consider the following:

Since the site $S$ of $\mathbf{H} \coloneqq SuperFormalSmooth\infty Grpds$ has a terminal object $\ast$, it follows that for $X\in \mathbf{H}$ any sheaf $X \colon \mathcal{S}^{op}\to Set$ then

$$\flat X \simeq X(\ast)$$

(where we may leave the constant re-embedding implicit, due to it being fully faithful).

Moreover, for every object $U\in \mathcal{S}$ there exists a morphism $i \colon \ast \to U$ hence for every $X\in \mathbf{H}$ and every $U$ there exists a morphism $i^\ast \colon X(U)\to \flat X$. This means that if $\flat X \simeq \emptyset$ then $X(U) \simeq \emptyset$ for all $U \in \mathcal{S}$ and hence $X\simeq \emptyset$.

We now show that this condition is equivalent to the required Aufhebung:

Generally, given a topos equipped with a level of a topos given by an adjoint modality $(\Box\dashv \bigcirc) \coloneqq (\flat \dashv \sharp)$, then the condition $\sharp \emptyset \simeq \emptyset$ is equivalent to $(\flat X \simeq \emptyset) \Leftrightarrow (X \simeq \emptyset)$.

Because: in a topos the initial object $\emptyset$ is a strict initial object, and hence $(X \simeq \emptyset) \simeq (X \to \emptyset)$. Therefore in one direction, assuming $\sharp \emptyset \simeq \emptyset$ then

$$\begin{aligned} (X \simeq \emptyset) & \simeq (X \to \emptyset) \\ & \simeq (X \to \sharp \emptyset) \\ & \simeq (\flat X \to \emptyset) \\ & \simeq (\flat X \simeq \emptyset) \end{aligned} \,.$$

Conversely, assuming that $(\flat X \simeq \emptyset) \Leftrightarrow (X \simeq \emptyset)$, then for all $X$

$$\begin{aligned} (X\to \emptyset) & \simeq (X\simeq \emptyset) \\ & \simeq (\flat X \simeq \emptyset) \\ & \simeq (\flat X \to \emptyset) \\ & \simeq (X\to \sharp \emptyset) \end{aligned}$$

and hence by the Yoneda lemma $\emptyset \simeq \sharp \emptyset$.

$\,$

Second, for the statement $\rightsquigarrow \Im \simeq \Im$ consider the following:

For any $X \in \mathbf{H}$ and any $U \times D_s\in CartSp \rtimes SuperInfPoint \hookrightarrow \mathbf{H}$ we have by adjunction natural equivalences

$$\begin{aligned} \mathbf{H}(U \times D_s , \stackrel{\rightsquigarrow}{\Im X}) & \simeq \mathbf{H}(\stackrel{\rightrightarrows}{U \times D_s} , \Im X) \\ &\simeq \mathbf{H}(\Re(\stackrel{\rightrightarrows}{U \times D_s}) , X) \\ & \simeq \mathbf{H}(U, X) \\ & \simeq \mathbf{H}(\Re(U \times D_s), X) \\ & \simeq \mathbf{H}(U \times D_s, \Im X) \end{aligned} \,.$$

Here the crucial step is the observation that on representables, by construction, the reduced part of the even part is the reduced part of the original object.

But observe that

Proposition

While, due to prop. , in the model of def.

• the opposition $ʃ \dashv \sharp$ has determinate negation in the sense of def. ;

on the other hand

• the opposition $\rightrightarrows \dashv \rightsquigarrow$ does not have definite negation in the sense of def. .

Proof

The definition would require that

$$\stackrel{\rightsquigarrow}{\mathbb{R}^{0|2}} \longrightarrow \stackrel{\rightrightarrows}{\mathbb{R}^{0|2}}$$

is an epimorphism. But this is equivalent to the point inclusion

$$\ast \longrightarrow \mathbb{D}(1)$$

into the formal dual of the algebra of dual numbers.

Space-Time-Matter

We discuss now how in the externalization of the theory given by theorem there naturally appears spacetime from the idea.

The progressive system of moments above, yields, by prop. , two god-given objects:

real line	superpoint
$\mathbb{R} = \mathbb{R}^{1\vert 0}$	$\mathbb{R}^{0\vert 1}$
$ʃ \simeq loc_{\mathbb{R}}$	$\R \simeq loc_{\mathbb{R}^{0\vert 1}}$

Both have familiar structure of an abelian group object, $\mathbb{R}$ being the additive group, hence there are arbitrary deloopings $\mathbf{B}^n \mathbb{R}^{0|1}$ and $\mathbf{B}^{n}\mathbb{R}$.

Given two types, there are the judgements in which these appear as subject and as predicate, in the sense discussed above.

There are no non-trivial judgements with (a delooping of) $\mathbb{R}$ as the subject and (a delooping of) $\mathbb{R}^{0|1}$ as the predicate. But there turn out to be some exceptional judgements with subject $\mathbb{R}^{0|q}$ and predicate $\mathbf{B}^d \mathbb{R}$.

By example this leads to the deduction of the object which is the homotopy fibers of the corresponding maps. From these one obtains further judgements, then further objects, and so forth. This way a “bouquet” of objects is induced from the initial ones.

We now discuss how this bouquet first of all yields super Minkowski spacetime (Huerta-Schreiber 17) and then further the extended super Minkowski spacetimes arising from super p-brane condensates (FSS).

Minkowski spacetime

Consider first the superpoint $\mathbb{R}^{0|1}$.

Remark

This is the unique 0-truncated object which is

1. purely negative to bosonic moment;

2. purely opposite to bosonic moment;

in that

$$\e(\mathbb{R}^{0|1})\simeq \mathbb{R}^{0|1}$$

$$\stackrel{\rightrightarrows}{\mathbb{R}^{0|1}} \simeq \ast \,.$$

Since $\mathbb{R}^{0|1}$ (and the other objects obtained in a moment) are contractible as super Lie groups, we may use the van Est isomorphism to conveniently discuss them as super Lie algebras. Regarding $\mathbb{R}^{0\vert 1}$ as a super Lie algebra, then its Chevalley-Eilenberg algebra is freely generated from a $(1,odd)$-bigraded element $d\theta$

$$CE(\mathbb{R}^{0\vert 1}) = \left( \wedge^\bullet \langle d\theta \rangle, d_{CE} = 0 \right) \,.$$

It is evident that

Proposition

The second super Lie algebra cohomology of $\mathbb{R}^{0\vert 1}$ is

$$H^{2}(\mathbb{R}^{0\vert 1}, \mathbb{R}) = \mathbb{R}$$

represented by the 2-cocycles of the form

$$d\theta\wedge d\theta \in CE(\mathbb{R}^{0\vert 1}) \,.$$

The Lie algebra extension

$$\array{ \mathbb{R}^{1|\mathbf{1}} \\ \downarrow \\ \mathbb{R}^{0|1} &\stackrel{}{\longrightarrow}& \mathbf{B}^1 \mathbb{R} }$$

classified by this is the super translation group in 1-dimension.

This is the worldline of the superparticle.

There are no further non-trivial cocycles here giving further extensions.

Hence next consider the Cartesian product of the initial superpoint with itself.

$$\mathbb{R}^{0|2} = \mathbb{R}^{0|1}\times \mathbb{R}^{0|1} \,.$$

Remark

This is still purely of negative bosonic moment in that $e(\mathbb{R}^{0|2}) \simeq \mathbb{R}^{0|2}$, but it no longer has purely no moment opposed to bosonic moment (witnessing that the fermionic opposition is not complete, lemma ), instead

$$\stackrel{\rightrightarrows}{\mathbb{R}^{0|2}} \simeq \mathbb{D}(1)$$

is the first-order infinitesimal interval (the formal dual of the “algebra of dual numbers”).

Proposition

The second super Lie algebra cohomology of $\mathbb{R}^{0\vert 2}$ is

$$H^2(\mathbb{R}^{0\vert 2}, \mathbb{R}) \simeq \mathbb{R}^3$$

represented by the cocycles of the form

$$a_{11} \, d\theta_1 \wedge d\theta_1 + a_{22} \, d\theta_2 \wedge d\theta_2 + a_{12} \, d\theta_1 \wedge d\theta_2 \,.$$

The extension classified by this

$$\array{ \mathbb{R}^{2,1|\mathbf{2}} \\ \downarrow \\ \mathbb{R}^{0|2} &\stackrel{}{\longrightarrow}& \mathbf{B} \mathbb{R}^3 }$$

is 3-dimensional super Minkowski spacetime.

Proof

This follows by inspection of the real spin representations in dimension 3, see the details spelled out at spin representation – via division algebras – Example d=3).

For more on this see at geometry of physics – supersymmetry the section Supersymmetry from the Superpoint.

Now the old brane scan gives:

Proposition

The $Spin(2,1)$-invariant third Lie algebra cohomology of 3d Minkowski super-spacetime is

$$H^3(\mathbb{R}^{2,1\vert \mathbf{2}})^{Spin(2,1)} = \mathbb{R}$$

represented by the 3-cocycle which, as a left invariant super differential form on $\mathbb{R}^{2,1\vert \mathbf{2}}$ is the WZW term in the Green-Schwarz action functional for the super 1-brane in 3d.

$$\array{ \mathfrak{string}_{het \, on \, G_2} \\ \downarrow \\ \mathbb{R}^{2,1\vert \mathbf{2}} &\stackrel{}{\longrightarrow}& \mathbf{B}^2 \mathbb{R} }$$

A definite globalization, of this 3-cocycle over a $\mathbb{R}^{3\vert \mathbf{2}}$-manifold requires, by def. , that the tangent bundle is a bundle of super Lie algebras and that the cocycle extends to a definite form. This imposes G-structure for $G$ the Lorentz group (or rather its spin group double cover).

Proposition

The joint stabilizer of $GL(\mathbb{R}^{2,1\vert 2})$ of the Lie bracket and the 3-cocycle is the pin group $Pin(2,1)$, the unoriented generalization of the spin group $Spin(2,1)$, the double cover of the Lorentz group $SO(2,1)$.

This is one special case of a more general statement which we come to as prop. below.

Consider then $\mathbb{R}^{2,1\vert 4}$

$$\array{ && \mathbb{R}^{2,1\vert 4} \\ & \swarrow && \searrow \\ \mathbb{R}^{0 \vert 2} && && \mathbb{R}^{0\vert 2} \\ & \searrow && \swarrow \\ && \mathbf{B} \mathbb{R}^3 } \,.$$

Proposition

There is a 1-dimensional space of $Spin(2,1)$-invariant 2-cocycles on $\mathbb{R}^{2,1\vert \mathbf{2} + \mathbf{2}}$. The Lie algebra extension classified by that is 4d super Minkowski spacetime

$$\array{ \mathbb{R}^{3,1\vert 4} \\ \downarrow \\ \mathbb{R}^{2,1\vert \mathbf{2}+{\mathbf{2}}} &\longrightarrow& \mathbf{B}\mathbb{R} }$$

Proof

By inspection of the real spin representations in dimension 4.

Now the old brane scan gives:

Proposition

$$H^4(\mathbb{R}^{3,1\vert \mathbf{4}}) = \mathbb{R}$$

represented by the 4-cocycle which, as a left invariant super differential form on $\mathbb{R}^{3,1\vert \mathbf{2}}$ is the WZW term in the Green-Schwarz action functional for the super 2-brane in 4d.

$$\array{ \mathfrak{m}2\mathfrak{brane}_{on\,G_2} \\ \downarrow \\ \mathbb{R}^{3,1\vert \mathbf{4} } &\stackrel{}{\longrightarrow}& \mathbf{B}^3 \mathbb{R} } \,.$$

Lorentz symmetry

Notice that so far we have obtained 3-dimensional and 4-dimensional Minkowski spacetime and the WZW-term for the superstring and the membrane propagating on it without assuming knowledge of the Lorentz group. In fact we assumed nothing but the presence of the real line $\mathbb{R}$ and the odd line $\mathbb{R}^{0|1}$ and we have simply investigated their cohomology.

The following proposition shows that the Lorentz group, in fact its universal cover by the pseudo-Riemannian spin group is deduced from this.

Proposition

Let $\mathbb{R}^{d-1,1,N}$ be super Minkowski spacetime in dimension $d \in \{3,4,6,10\}$ and let $\phi \in \Omega^{3}(\mathbb{R}^{d-1,1|N})$ the corresponding 3-form characterizing the super-1-brane (superstring) in this dimension, according to the brane scan . Then the stabilizer subgroup of both the super Lie bracket and the cocycle is the Spin group $Spin(d-1,1)$:

$$Stab_{GL(\mathbb{R}^{d-1,1|N})}([-,-], \phi) \simeq Spin(d-1,1) \hookrightarrow GL(\mathbb{R}^{d-1,1|N}) \,.$$

Proof

It is clear that the spin group fixes the cocycle, and by the discussion at spin representation it preserves the bracket. Therefore it remains to be seen that the Spin group already exhausts the stabiizer group of bracket and cocycle. For that observe that the 3-cocycle is

$$(\psi,\phi, v) \mapsto \eta( [\psi,\phi], v ) \,,$$

where $\eta(-,-)$ is the given Minkowski metric, and that the bilinear map

$$[-,-]\colon S \otimes S\to V$$

is surjective. This imples that if $g \in GL(\mathbb{R}^{d-1,1|N})$ preserves both the bracket and the cocycle for all $\psi, \phi \in S$ and $v \in V$ to

$$\eta( [g(\psi),g(\phi)], g(v) ) = \eta( g([\psi,\phi]), g(v) ) = \eta( [\psi,\phi], v )$$

then it preserves the Minkowski metric for all $w,v$

$$\eta(g(w), g(v)) = \eta(w,v) \,.$$

This means that $\mathbb{R}^{2,1|2}$-manifolds $X$ equipped with the 3-cocycle as a definite form such that the resulting G-structure according to prop. also preserves the the group structure on $\mathbb{R}^{2,1|2}$, then this is equivalent to equipping $X$ with Lorentzian orthogonal structure, hence with super-pseudo-Riemannian metric, hence with a field-configuration for 3d supergravity.

Fundamental branes

The brane bouquet that we find…

$$\array{ && \mathfrak{m}2\mathfrak{brane}_{on\,G_2} \\ && \downarrow \\ && \mathbb{R}^{3,1|\mathbf{4}} && \mathbb{R}^{2,1|\overline{\mathbf{2}}} \\ && \downarrow & \nearrow& & \searrow \\ \mathfrak{string}_{IIA\,on\,G_2} &\longrightarrow& \mathbb{R}^{2,1|\mathbf{2}+\overline{\mathbf{2}}} && && \mathbb{R}^{3} \\ && \downarrow &\searrow& & \nearrow \\ && \mathbb{R}^{0|\mathbf{2}+\overline{\mathbf{2}}} && \mathbb{R}^{2,1|\mathbf{2}} \\ && && \downarrow \\ && && \mathbb{R}^{0|\mathbf{2}} \\ && & \swarrow && \searrow \\ && \mathbb{R}^{0|1} && && \mathbb{R}^{0|1} }$$

this is equivalently the physics coming from M-theory on G2-manifolds, given by the extensions that emanate from 32 copies of the smallest superpoint:

$$\array{ && && \mathfrak{m}5\mathfrak{brane} \\ && && \downarrow \\ && && \mathfrak{m}2\mathfrak{brane} \\ && && \downarrow \\ && \underset{p}{\coprod} \mathfrak{d}{2p}\mathfrak{brane} && \mathbb{R}^{10,1|\mathbf{32}} \\ && \downarrow && \downarrow \\ && \mathfrak{string}_{IIA} &\longrightarrow & \mathbb{R}^{9,1|\mathbf{16}+\overline{\mathbf{16}}} \\ && && \downarrow \\ && && \mathbb{R}^{0|\mathbf{16}+\overline{\mathbf{16}}} \\ && & \swarrow && \searrow \\ && \mathbb{R}^{0|1} && \cdots && \mathbb{R}^{0|1} }$$

These are branches of The brane bouquet of string theory, see there for more. By prop. each branch here gives the WZW form for the corresponing Green-Schwarz super p-brane sigma model.

Gravity

Above we have found two interlocking ingredients arising from the axiomatics:

1. abstract generals – Given any group object $V$, then there is an abstract general concept of $V$-manifolds $X$, def. . Given furthermore a WZW term $\mathbf{L}_{WZW}^V$ on $V$, then there is an abstract general concept of definite globalizations of this term over these manifolds $X$, inducing G-structures on $X$, prop. .

2. concrete individuals – We have found concrete individual $V$s: extended super Minkowski spacetimes, prop. , prop. emanating from the objects which represent the moments $ʃ$ and $\rightrightarrows$, and we have further found individual $\mathbf{L}_{WZW}^V$: the super p-brane WZW terms, prop. etc., forming The brane bouquet.

Plugging the concrete individuals into the general abstract theory, we hence obtain particular phenomena.

$$\array{ && \flat^{rel}_{(1)} U \\ & \swarrow && \searrow \\ \mathbb{R}^{d-1,1|\mathbf{N}} && \swArrow && X \\ & {}_{\mathllap{\mathbf{L}_{WZW}^{brane}}}\searrow && \swarrow_{\mathrlap{\mathbf{L}_{WZW}^X}} \\ && \mathbf{B}^{p+2}\mathbb{G}_{conn} }$$

Specifically there is 11-dimensional super Minkowski spacetime $V = \mathbb{R}^{10,1\vert \mathbf{32}}$ carrying the WZW term $\mathbf{L}_{WZW}^{M2}$ for the M2-brane, in some sense the endpoint of the bouquet of super-spacetimes. The KK-compactification of this on a 7-dimensional G2-manifold yields the 4-dimensional super-Minkowski spacetime discussed above, with the WZW term for the super 2-brane in 4d.

The 11-dimensional super-Minkowski spacetime is special in many ways, one of which is that in this dimension the equations of motion of 11-dimensional supergravity on a $(Spin(10,1)\hookrightarrow Iso(\mathbb{R}^{10,1\vert \mathbf{32}}))$-super Cartan geometry $X$ modeled on $\mathbb{R}^{10,1\vert \mathbf{32}}$ are already captured by just a constraint on the torsion tensor. But by remark this means that in dimension 11 the equations of motion of supergravity have an immediate axiomatization in our objective logic.

equivalent to just the condition that the of $X$ is at each point and to first infinitesimal order the intrinsic torsion of $\mathbb{R}^{10,1\vert \mathbf{32}}$

Proposition

First-order integrable $(Spin(10,1)\hookrightarrow Iso(\mathbb{R}^{10,1\vert \mathbf{32}}))$-super-Cartan geometries, def. , on $\mathbb{R}^{10,1\vert\mathbf{32}}$-manifolds $X$, def. , which are first-order integrable with respect to the intrinsic left-invariant torsion of $\mathbb{R}^{10,1\vert \mathbf{32}}$, remark , are equivalent to vacuum solutions to the equations of motion of 11-dimensional supergravity, i.e. to solutions for which the field strength of the gravitino and of the supergravity C-field vanishes identically, hence to solutions to the ordinary vacuum Einstein equations in 11d.

Proof

(Howe 97) shows that imposing (on some chart) $\mathbf{d} E^a + \omega^{a}{}_b \wedge E^b - \bar \psi \Gamma^a \psi = 0$ implies (and hence is equivalent to) the equations of motion of 11d supergravity. These equations (see e.g. D’Auria-Fré 82, p. 31) then show that furthermore requiring $\mathbf{d} \psi + \tfrac{1}{2}\omega_{a b} \Gamma^{a b}\psi = 0$ (and hence requiring the full supertorsion tensor to be that of super-Minkowski spacetime) puts the field strength of the gravitino and of the supergravity C-field to 0.

Remark

Vacuum Einstein solutions as in prop. , are considered notably in the context of M-theory on G2-manifolds (e.g. Acharya 02, p. 9). See also at M-theory on G2-manifolds – Details – Vacuum solution and torsion constraints.

Proposition

Given a definite globalization $\mathbf{L}_{WZW}^X$ of a super $p$-brane WZW term $\mathbf{L}_{WZW}^V$, then the stabilizer infinity-group of $\mathbf{L}_{WZW}$ is the integrated BPS charge algebra of this solution of supergravity.

See at BPS charge – Formalization in higher differential geometry.

Acknowledgements

These notes benefited from discussion with Dave Carchedi, David Corfield, Thomas Holder, John Huerta and Mike Shulman.

References

• Ulrich Bunke, Thomas Nikolaus, Michael Völkl, Differential cohomology theories as sheaves of spectra, Journal of Homotopy and Related Structures, October 2014 (arXiv:1311.3188)

• Domenico Fiorenza, Hisham Sati, Urs Schreiber, Super Lie n-algebra extensions, higher WZW models and super p-branes with tensor multiplet fields, Volume 12, Issue 02 (2015) 1550018

• John Huerta, Urs Schreiber, M-Theory from the Superpoint (arXiv:1702.01774)

• Peter Johnstone, Sketches of an Elephant – A Topos Theory Compendium, Oxford 2002.

• James Ladyman, Stuart Presnell, Does Homotopy Type Theory Provide a Foundation for Mathematics?, 2014 (web)

• William Lawvere, Some Thoughts on the Future of Category Theory in A. Carboni, M. Pedicchio, G. Rosolini, Category Theory , Proceedings of the International Conference held in Como, Lecture Notes in Mathematics 1488, Springer (1991)

• William Lawvere, Toposes of laws of motion, Sept. 1997 (pdf)

• William Lawvere, Axiomatic cohesion Theory and Applications of Categories, Vol. 19, No. 3, 2007, pp. 41-49. (web, pdf)

• Dan Licata, Mike Shulman, Adjoint logic with a 2-category of modes, Logical Foundations of Computer Science, Volume 9537 of the series Lecture Notes in Computer Science pp 219-235, 2015 (pdf)

• Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)

• Thomas Nikolaus, Urs Schreiber, Danny Stevenson, Principal ∞-Bundles – General theory, Journal of Homotopy and Related Structures, June 2014 (arXiv:1207.0248)

• Arhtur Sale, Primitive data types, The Australian Computer Journal, Vol. 9, No. 2, July 1977 (pdf)

• Urs Schreiber, differential cohomology in a cohesive topos

• Michael Shulman, Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science, Volume 25, Issue 5 ( From type theory and homotopy theory to Univalent Foundations of Mathematics ) June 2015 (arXiv:1203.3253, doi:/10.1017/S0960129514000565)

• Michael Shulman, Inductive and higher inductive types (2012) (pdf)

• Michael Shulman, model of type theory in an (infinity,1)-topos

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics, 2013

$\,$

Related talks include

1. Quantum gauge field theory in Cohesive homotopy type theory,

2. Synthetic Quantum Field Theory,

3. Classical field theory via Cohesive homotopy types,

4. Quantization via Linear homotopy types

5. Duality of Monads in Geometric Homotopy Theory