Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

June 28, 2012

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:

  1. 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.

  2. 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 GG-principal \infty-bundle is formalized as a G\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 GG – defined to be the identity type G(pt Apt A)G \coloneqq (pt_A \simeq pt_A) for some inhabited connected type AA which we will write BG:=A\mathbf{B}G := A – we have a long fiber sequence like this: Gθ dRBGBGFBG. G \stackrel{\theta}{\to} \flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G \stackrel{F}{\to} \mathbf{B}G \,.

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

Accordingly, the function

θ:G dRBG \theta : G \to \flat_{dR}\mathbf{B}G

is such a flat 𝔤\mathfrak{g}-valued form: the Maurer-Cartan form on GG. Here we see it arise canonically as the homotopy fiber of the function dRBGBG\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 GG-principal \infty-bundle.

All these items are discussed in more detail in the nnLab 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:

dRBG BG F BG. \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 GG-\infty-action by gauge transformations on 𝔤\mathfrak{g}-valued differential forms.

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

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

Then we can ask for a lift of this through FF.

BG F X BG \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(x):BGx : X \vdash \nabla(x) : \flat \mathbf{B}G on PP. Or rather, it classifies such a flat connection. Or better: it modulates a flat connection on PP.

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

p:UX p : U \to X

(a function such that x:XisInhab(p 1(x)) \sum_{x : X} isInhab( p^{-1}(x) ) ) over which \nabla lifts to a function with values in dRBG\flat_{dR} \mathbf{B}G, hence to a differential form |U\nabla_{|U} on the cover

dRBG BG |U U p X BG. \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 XX TWISTED by the GG-principal bundle PP .

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 PXP \to X as above is exhibited by a flat 𝔤\mathfrak{g}-valued differential form AA on PP that satisfies two conditions:

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

  2. E II: Translating AA by gGg \in G under the GG-action on PP is the same as applying the adjoint action of gg on AA.

With the above cohesive homotopy type theory, we can naturally obtain such a structure from the connection :XBG\nabla : X \to \flat \mathbf{B}G. For if we regard this as a PP-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

P A dRBG * X BG F BG \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 dRBG A : P \to \flat_{dR}\mathbf{B}G

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

The way that this AA appears it is a morphism of GG-actions: it intertwines the GG-actions on PP and on dRBG\flat_{dR} \mathbf{B}G. An A:X dRBGA : X \to \flat_{dR} \mathbf{B}G with such properties we may call a flat Ehresmann connection on PP in cohesive homotopy type theory.

If the cohesive homotopy type theory is taken to be the internal language of Smooth∞Grpd and if GG happens to be an ordinary Lie group, then one can check that such AA are indeed Ehresmann connection 1-forms in the traditional sense. It is intuitively clear that the respect for the GG-action of AA 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\vdash x : X be any point of XX. Then we can form the pasting of homotopy pullbacks on the left of this equivalence

G P A dRBG x X BG F BGG θ dRBG * BG, \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 AA to the fiber P xGP_x \simeq G

A |P x=θ A_{|P_x \simeq} = \theta

with the Maurer-Cartan form.

Posted at June 28, 2012 4:13 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2537

5 Comments & 0 Trackbacks

Re: Flat Ehresmann connections in Cohesive HoTT

This may have been addressed elsewhere, but how does one define 𝔤\mathfrak{g} given BG\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)?

Posted by: David Roberts on June 29, 2012 1:14 AM | Permalink | Reply to this

Re: Flat Ehresmann connections in Cohesive HoTT

how does one define 𝔤\mathfrak{g} given BG\mathbf{B}G in a general cohesive ∞-topos?

This is discussed a bit at structures in a cohesive ∞-topos in the section exponentiated Lie algebras.

Posted by: Urs Schreiber on June 29, 2012 9:07 AM | Permalink | Reply to this

Re: Flat Ehresmann connections in Cohesive HoTT

With every new piece of structure you find for cohesive \infty-toposes, doesn’t it seem less likely that an unsuspected new \infty-topos will be found, as with all that structure it must possess, wouldn’t it have shown itself already?

Posted by: David Corfield on June 29, 2012 7:33 AM | Permalink | Reply to this

Re: Flat Ehresmann connections in Cohesive HoTT

David asks:

With every new piece of structure you find for cohesive ∞-toposes, doesn’t it seem less likely that an unsuspected new ∞-topos will be found

For bystanders we should briefly explain what this refers to:

David, with his uncanny ability to keep pushing for the next important conceptual question, has long been wanting to get a better grasp of the general nature, or just the scope, of the space of models for higher cohesion. What I had and have to offer is a handful of examples, which happen to be those that I care about for the applications that I have in mind.

So the question is: what would be other interesting examples, if any, of cohesive \infty-toposes?

I feel pretty certain that there are many more, and that the only reason they haven’t shown up yet is that nobody is sitting down to work out the evident guesses (I feel that I need to currently concetrate my attention on other aspects).

But this is the context in which David here wonders whether:

with all that structure it must possess, wouldn’t it have shown itself already?

So if I understand your question correctly, you are saying in paraphrase something like:

If a cohesive \infty-topos comes intrinsically with all these structures – de Rham cohomology, differential cohomology, Ehresmann connections, prequantization, etc. – it has to model a notion of geometry in which all these structures exist, and of these there may not be that many.

Right?

If so then: I wouldn’t think so.

On the one hand, these structures may well happen to be trivial in a given cohesive \infty-topos. For instance ETop∞Grpd has trivial differential structure, nevertheless it is a cohesive \infty-topos.

On the other hand, the above list of structures – de Rham cohomology, differential cohomology, Ehresmann connections, prequantization, etc. – is considered in many geometric contexts for which cohesive models were not written down yet. First and foremost algebraic geometry, arithmetic geometry. Also non-comutative geometry in all its flavours. There will be many more.

I don’t think there will turn out to be scarcity of examples. It will just take a Master- or PhD-thesis to crank them out.

Posted by: Urs Schreiber on June 29, 2012 9:30 AM | Permalink | Reply to this

Re: Flat Ehresmann connections in Cohesive HoTT

Yes, that paraphrase captured the thought.

It will just take a Master- or PhD-thesis to crank them out.

Seems to me like a rewarding project in reverse engineering. From a manifestion in, say, the case of p-adic cohomology, I wonder how hard it is to crank out the result.

Posted by: David Corfield on June 30, 2012 1:23 PM | Permalink | Reply to this

Post a New Comment