The n-Category Café

Preliminaries and reminder

Recall from HoTT Cohesion - Exercise I and Exercise II that one of the fundamental consequences of cohesion in homotopy type theory is that for every $\mathrm{\infty }$-group $G$ – defined to be the identity type $G≔({\mathrm{pt}}_A\simeq {\mathrm{pt}}_A)$ for some inhabited connected type $A$ which we will write $BG:=A$ – we have a long fiber sequence like this:

$$G\stackrel{\theta }{\to }{♭}_{\mathrm{dR}}BG\to ♭BG\stackrel{F}{\to }BG.$$

Here $BG$ is the type of $G$-principal bundles (a dependent term $x:X⊢P(x):BG$ is interpreted as a $G$-principal bundle over $X$) and similarly $♭BG$ is that of $G$-principal bundles with flat connection. The function $F:♭BG\to BG$ forgets the flat connection and just remembers the underlying bundle. Next, ${♭}_{\mathrm{dR}}BG$ is the type of flat (closed) $\mathrm{Lie}(G)$-valued differential forms, in that a dependent term $x:X⊢A(x):{♭}_{\mathrm{dR}}BG$ is a flat $𝔤$-valued differential form $A$ on $X$.

Accordingly, the function

$$\theta :G\to {♭}_{\mathrm{dR}}BG$$

is such a flat $𝔤$-valued form: the Maurer-Cartan form on $G$. Here we see it arise canonically as the homotopy fiber of the function ${♭}_{\mathrm{dR}}BG\to ♭BG$ that regards a flat $𝔤$-valued differential form as a flat connection on the trivial $G$-principal $\mathrm{\infty }$-bundle.

All these items are discussed in more detail in the $n$Lab entry cohesive (∞,1)-topos – structures.

Flat connections

We will now use the first stage of the above long fiber sequence and regard it as a local coefficient bundle, for that purpose suggestively drawn like this:

$$\begin{array}{ccc}{♭}_{\mathrm{dR}}BG& \to & ♭BG\\ & & {\downarrow }^F\\ & & BG\end{array}.$$

In the sense of section 4.1 of NSSa this exhibits the universal associated $\mathrm{\infty }$-bundle for the canonical $G$-$\mathrm{\infty }$-action by gauge transformations on $𝔤$-valued differential forms.

Suppose we start with a $G$-principal bundle over some $X$, modulated by the function

$x:X⊢P(x):BG$. $$\begin{array}{c}P\\ \downarrow \\ X& \to & BG\end{array}.$$

Then we can ask for a lift of this through $F$.

$$\begin{array}{ccc}& & ♭BG\\ & {}^{\nabla }\nearrow & {\downarrow }^F\\ X& \stackrel{}{\to }& BG\end{array}$$

such a lift is a choice of flat connection $x:X⊢\nabla (x):♭BG$ on $P$. Or rather, it classifies such a flat connection. Or better: it modulates a flat connection on $P$.

Namely, by the discussion in section 4.2 of NSSa, $\nabla$ is a cocycle in $P$-twisted de Rham cohomology: there exists a cover

$$p:U\to X$$

(a function such that ${\sum }_{x:X}\mathrm{isInhab}(p^{-1}(x))$ ) over which $\nabla$ lifts to a function with values in ${♭}_{\mathrm{dR}}BG$, hence to a differential form ${\nabla }_{\mid U}$ on the cover

$$\begin{array}{ccccc}& & {♭}_{\mathrm{dR}}BG& \to & ♭BG\\ & {}^{{\nabla }_{\mid U}}\nearrow & & & \downarrow \\ U& \stackrel{p}{\to }& X& \to & BG\end{array}.$$

So $\nabla$ is a flat $𝔤$-valued form on $X$ TWISTED by the $G$-principal bundle $P$ .

Traditionally we might say: “Yes, that’s a useful heuristics for thinking about flat connections”. In cohesive HoTT this statement is a formal fact.

Flat Ehresmann connections

There are many equivalent traditional incarnations of the notion of a connection on a bundle. One of them is that of an Ehresmann connection. This is the definition where a flat connection on the bundle $P\to X$ as above is exhibited by a flat $𝔤$-valued differential form $A$ on $P$ that satisfies two conditions:

1. E I: The restriction of $A$ to any fiber is the Maurer-Cartan form $\theta$;

2. E II: Translating $A$ by $g\in G$ under the $G$-action on $P$ is the same as applying the adjoint action of $g$ on $A$.

With the above cohesive homotopy type theory, we can naturally obtain such a structure from the connection $\nabla :X\to ♭BG$. For if we regard this as a $P$-twisted $𝔤$-valued de Rham cocycle, then by the discussion in section 4.3 of NSSa we are to consider the pasting of homotopy pullbacks

$$\begin{array}{ccccc}P& \stackrel{A}{\to }& {♭}_{\mathrm{dR}}BG& \to & *\\ \downarrow & & \downarrow & & \downarrow \\ X& \stackrel{\nabla }{\to }& ♭BG& \stackrel{F}{\to }& BG\end{array}$$

and regard the function

$$A:P\to {♭}_{\mathrm{dR}}BG$$

that appears here as modulating the geometric structure over $P$ which reflects the lift $\nabla$ down on base space $X$: the $P$-twisted infinity-bundle corresponding to $\nabla$.

The way that this $A$ appears it is a morphism of $G$-actions: it intertwines the $G$-actions on $P$ and on ${♭}_{\mathrm{dR}}BG$. An $A:X\to {♭}_{\mathrm{dR}}BG$ with such properties we may call a flat Ehresmann connection on $P$ in cohesive homotopy type theory.

If the cohesive homotopy type theory is taken to be the internal language of Smooth∞Grpd and if $G$ happens to be an ordinary Lie group, then one can check that such $A$ are indeed Ehresmann connection 1-forms in the traditional sense. It is intuitively clear that the respect for the $G$-action of $A$ corresponds to the second Ehresmann condition. In fact it also implies the first. This we can see manifestly already in the abstract language:

Let $⊢x:X$ be any point of $X$. Then we can form the pasting of homotopy pullbacks on the left of this equivalence

$$\begin{array}{ccccccc}G& \to & P& \stackrel{A}{\to }& {♭}_{\mathrm{dR}}BG& \to & *\\ \downarrow & & \downarrow & & \downarrow & & \downarrow \\ *& \stackrel{x}{\to }& X& \stackrel{\nabla }{\to }& ♭BG& \stackrel{F}{\to }& BG\end{array}\simeq \begin{array}{ccc}G& \stackrel{\theta }{\to }& {♭}_{\mathrm{dR}}BG\\ \downarrow & & \downarrow \\ *& \to & BG\end{array},$$

where the pasting law for pullbacks, this identifies on the right the restriction of $A$ to the fiber $P_x\simeq G$

$$A_{\mid P_x\simeq }=\theta$$

with the Maurer-Cartan form.