### Flat Ehresmann connections in Cohesive HoTT

#### Posted by Urs Schreiber

This is to share a little observation about the formulation of *flat Ehresmann connections* in *cohesive homotopy type theory*.

For context, this can be understood as following up on two different threads on this blog:

You may think of this as part IV of the little series

*HoTT Cohesion*(part I: de Rham cohomology, part II: differential cohomology, part III: geometric prequantization) in which we discussed very simple constructions in homotopy type theory that exist as soon as the axiom of*cohesion*is added and which, simple as they are, are interpreted as fundamental constructions in higher differential geometry.You may think of this as a curious example of the theory of

*twisted principal ∞-bundles*discussed in the previous entry. For I will describe how a flat Ehresmann connection on a $G$-principal $\infty$-bundle is formalized as a $\flat G$-twisted $\infty$-bundle on its total space, where $\flat$ (“flat”) is one of the two reflectors in the definition of cohesive homotopy type theory.

## 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 *$\infty$-group* $G$ – defined to be the identity type $G \coloneqq (pt_A \simeq pt_A)$ for some inhabited connected type $A$ which we will write $\mathbf{B}G := A$ – we have a long fiber sequence like this:
$G \stackrel{\theta}{\to} \flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G \stackrel{F}{\to} \mathbf{B}G
\,.$

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

Accordingly, the function

$\theta : G \to \flat_{dR}\mathbf{B}G$

is such a flat $\mathfrak{g}$-valued form: the *Maurer-Cartan form* on $G$. Here we see it arise canonically as the homotopy fiber of the function $\flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G$ that regards a flat $\mathfrak{g}$-valued differential form as a flat connection on the trivial $G$-principal $\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:

$\array{ \flat_{dR} \mathbf{B}G &\to& \flat \mathbf{B}G \\ && \downarrow^{\mathrlap{F}} \\ && \mathbf{B}G } \,.$

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

Suppose we start with a $G$-principal bundle over some $X$, modulated by the function $x : X \vdash P(x) : \mathbf{B} G$.

$\array{ P \\ \downarrow \\ X &\to& \mathbf{B}G } \,.$

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

$\array{ && \flat \mathbf{B}G \\ & {}^{\mathllap{\nabla}}\nearrow & \downarrow^{\mathrlap{F}} \\ X &\stackrel{}{\to}& \mathbf{B}G }$

such a lift is a choice of flat connection $x : X \vdash \nabla(x) : \flat \mathbf{B}G$ 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} isInhab( p^{-1}(x) )$ ) over which $\nabla$ lifts to a function with values in $\flat_{dR} \mathbf{B}G$, hence to a differential form $\nabla_{|U}$ on the cover

$\array{ && \flat_{dR}\mathbf{B}G &\to& \flat \mathbf{B}G \\ & {}^{\mathllap{\nabla_{|U}}}\nearrow && & \downarrow \\ U &\stackrel{p}{\to}& X &\to& \mathbf{B}G } \,.$

So $\nabla$ is a *flat $\mathfrak{g}$-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 $\mathfrak{g}$-valued differential form $A$ on $P$ that satisfies two conditions:

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

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 \flat \mathbf{B}G$. For if we regard this as a $P$-twisted $\mathfrak{g}$-valued de Rham cocycle, then by the discussion in section 4.3 of NSSa we are to consider the pasting of homotopy pullbacks

$\array{ P &\stackrel{A}{\to}& \flat_{dR} \mathbf{B}G &\to& * \\ \downarrow && \downarrow && \downarrow \\ X &\stackrel{\nabla}{\to}& \flat \mathbf{B}G &\stackrel{F}{\to}& \mathbf{B}G }$

and regard the function

$A : P \to \flat_{dR}\mathbf{B}G$

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 $\flat_{dR} \mathbf{B}G$. An $A : X \to \flat_{dR} \mathbf{B}G$ 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 $\vdash x : X$ be any point of $X$. Then we can form the pasting of homotopy pullbacks on the left of this equivalence

$\array{ G &\to& P &\stackrel{A}{\to}& \flat_{dR} \mathbf{B}G &\to& * \\ \downarrow && \downarrow && \downarrow && \downarrow \\ * &\stackrel{x}{\to}& X &\stackrel{\nabla}{\to}& \flat \mathbf{B}G &\stackrel{F}{\to}& \mathbf{B}G } \;\;\; \simeq \;\;\; \array{ G &\stackrel{\theta}{\to}& \flat_{dR}\mathbf{B}G \\ \downarrow && \downarrow \\ * &\to& \mathbf{B}G } \,,$

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

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

with the Maurer-Cartan form.

## Re: Flat Ehresmann connections in Cohesive HoTT

This may have been addressed elsewhere, but how does one define $\mathfrak{g}$ given $\mathbf{B}G$ in a general cohesive $\infty$-topos? How much does $\mathfrak{g}$ look like a Lie algebra (or vector space with extra structure)?