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.

July 10, 2013

Synthetic ∞-Groupoid Theory

Posted by Mike Shulman

This week I’m at the 2013 International Category Theory conference in Syndey, Australia, along with our co-hosts Tom and Emily (and a bunch of other people (-: ). There’s a lot of interesting stuff being said that I don’t have time to write about right now, but I thought I would go ahead and post the slides for my own talk that I gave yesterday, since I’ve had one or two requests:

  • Homotopy type theory: towards Grothendieck’s dream (pdf slides)

I’m not sure how comprehensible the slides will be on their own, but you can probably get the general idea. The point I was trying to make was that if you want to, you can ignore all the business about computation, proof assistants, etc. and view homotopy type theory as a synthetic theory of \infty-groupoids — which happens to use slightly odd notation and terminology. The meaning of “synthetic” is by contrast with “analytic”, as in Euclid’s synthetic geometry (with undefined notions of points, lines, etc. satisfying axioms) versus cartesian analytic geometry (where points and lines are defined using pairs of real numbers).

Moreover, from this point of view, we can think of homotopy type theory as a solution to the homotopy hypothesis: its \infty-groupoids are algebraic and globular (in fact, as Guillaume Brunerie realized this past year, they’re very close to Grothendieck’s original definition of \infty-groupoid!), and via the model of homotopy type theory in “analytic” Kan complexes, we can use them to do homotopy theory. The classical homotopy hypothesis asks for an equivalence between \infty-groupoids and homotopy theory, but having the former be simply a model of the latter seems good enough for many purposes, and has the additional advantage that there are many other useful models (e.g. higher toposes).

Posted at July 10, 2013 1:14 AM UTC

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

14 Comments & 0 Trackbacks

Re: Synthetic ∞-Groupoid Theory

To kick things off, here’s one thing I learned from Mike’s really excellent talk: the univalence axiom is what allows us to form the (synthetic) \infty-groupoid of (synthetic) \infty-groupoids.

Posted by: Tom Leinster on July 10, 2013 2:48 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

A little more precisely, the univalence axiom is what identifies the hom-types of the universe type as consisting of equivalences, and therefore allows us to think of it as the \infty-groupoid of \infty-groupoids. Type theory before the univalence axiom already had universe types (types of types), but their hom-types were not really specified.

Posted by: Mike Shulman on July 10, 2013 9:46 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Mike,

The notions of “synthetic” and “analytic” are quite interesting here, though I only understood one tenth of your slides. Still, it reminds me of Tarski’s representation theorem for the (first-order) axiom system EG 2EG_2 of 2-dimensional synthetic Euclidean geometry, in Tarski’s 1959 paper “What is elementary geometry?”, which is available here:

http://www.corelab.ntua.gr/studygroup/Tarski_ElGeom.pdf

The primitive concepts of Tarski’s geometry are

x=yx = y

Bet(x,y,z)Bet(x,y,z): “yy lies between xx and zz

Cong(x,y,z,w)Cong(x,y,z,w): “the segment xyxy is congruent to the segment zwzw

The representation theorem is:

EG 2\mathcal{M} \models EG_2 iff 𝒞 2(𝔽)\mathcal{M} \cong \mathcal{C}_2(\mathbb{F}), where 𝔽\mathbb{F} is a real-closed field.

Here 𝒞 2(𝔽)\mathcal{C}_2(\mathbb{F}) is what Tarski calls the 2-dimensional “Cartesian space over the field 𝔽\mathbb{F}”. That is, its carrier set is 𝔽 2\mathbb{F}^2, and its distinguished relations are Betweenness (𝔽 3\subseteq \mathbb{F}^3) and Congruence (𝔽 4\subseteq \mathbb{F}^4), defined using 𝔽\mathbb{F} instead of \mathbb{R}. So, the standard case–for standard 2-dimensional 2\mathbb{R}^2–is:

𝒞 2()=( 2,Bet ,Cong )\mathcal{C}_2(\mathbb{R}) = (\mathbb{R}^2, Bet_{\mathbb{R}}, Cong_{\mathbb{R}}).

But the models 𝒞 2(𝔽)\mathcal{C}_2(\mathbb{F}) of geometry can be non-standard, e.g., if 𝔽\mathbb{F} is the countable real-closed field of algebraic reals.

So, considering HoTTHoTT is to be a “synthetic” theory, then what you’d like is some kind of representation theorem for HoTTHoTT.

Jeff

Posted by: Jeffrey Ketland on July 10, 2013 7:25 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Indeed. The expected “representation theorem” is that the models of HoTT are “elementary (,1)(\infty,1)-toposes”. However, we don’t yet have a definition of those. (-:

Posted by: Mike Shulman on July 10, 2013 9:25 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Oh good! I was going to ask for these too…

Can you say about more about the last slide in the first section? How would this give a recipe for computing unstable homotopy groups of spheres? And could you remind me what you said about the dependency of this on the meaning of “small”?

Posted by: Emily Riehl on July 10, 2013 11:56 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

I don’t think Jacob’s comment was intended to mean anything especially precise (although if he’s listening, he could clarify it himself). I figured he just meant that calculating homotopy groups of spheres involves “computing” with (the fundamental \infty-groupoid of) spheres, so if you had an “easy” way to do such “computing” then it could be used for such calculations, thereby making them also “easy”. Of course, this wouldn’t necessarily imply an algorithm for such calculations, so one might take exception to the word “recipe”.

In fact, one might argue that homotopy type theory does give us an “easy”, or at least “easier”, way to compute with things like homotopy groups of small cell complexes — namely, the encode-decode method, of which the first example was Dan Licata’s version of the proof of Ω(S 1)=\Omega(S^1)=\mathbb{Z}, which I sketched in the talk. It certainly isn’t a “recipe”, though — it still requires thought and work, and (so far) often the same or similar ideas to those that go into the classical calculations.

The point about “small” is just that whether or not “a formalism to compute easily with small examples” would tell you anything about spheres depends on whether or not spheres are “small”. They are “small” in terms of discs (being presented by a cell decomposition with only two discs in general), but not necessarily “small” in terms of morphisms (and indeed, the way to describe them in terms of morphisms is exactly what is difficult to compute about them).

Analytic \infty-groupoid theory seems, at least a priori, to deal more easily with morphisms than with discs, and hence might not consider spheres to be “small” examples — whereas both classical homotopy theory and homotopy type theory do consider spheres to be “small”, the one by using discs and the other by using freely-generating morphisms. I figure this is another advantage of homotopy type theory over analytic \infty-groupoid theory for purposes of doing homotopy theory: it’s better-adapted to describe the same sorts of spaces that homotopy theorists care about.

Posted by: Mike Shulman on July 10, 2013 12:17 PM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

I’m not sure if Mike mentioned this in his talk, but the “almost” next to Guillaume Brunerie’s proof that pi4(S^3) = Z2 is an intriguing first example of how we might actually “compute” homotopy groups in an algorithmic sense.

For most of the proofs we’ve done, we need to know the answer, and then we prove it’s correct—e.g., we need to know that pi_1(S^1) should turn out to be Z, and then we do a proof of this fact.

What Guillaume proved is that there exists a k such that pi4(S^3) = Zk. But, assuming univalence and higher inductives can be made constructive (currently a big open problem, but many people think it will turn out to be true), the proof is constructive. So we can run the proof and check that k is indeed 2. This is the first example we have where an algorithm would be computing some of the information.

Posted by: Dan Licata on July 10, 2013 4:17 PM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Thanks! I didn’t actually have time to mention that.

Posted by: Mike Shulman on July 11, 2013 7:13 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

The meaning of “synthetic” is by contrast with “analytic”, as in Euclid’s synthetic geometry (with undefined notions of points, lines, etc. satisfying axioms) versus cartesian analytic geometry (where points and lines are defined using pairs of real numbers).

The striking thing about Book I of The Elements as we read it today is that notions of points and lines are defined.

Definition 1. A point is that which has no part.

Definition 2. A line is breadthless length.

Definition 3. The ends of a line are points.

With Hilbert, we lose the definitions.

But you can’t keep a good concept down, and there on our nLab point entry is

As a topological space, the point is the usual point from geometry: that which has no part. In more modern language, we might say that it has no structure – except that something exists.

I would imagine that there’s an interesting history to the analytic/synthetic distinction. At the nLab page, we have Klein drawing attention to figures, rather than implicit definitions:

Synthetic geometry is that which studies figures as such, without recourse to formulas, whereas analytic geometry consistently makes use of such formulas as can be written down after the adoption of an appropriate system of coordinates.

He’s thinking of the likes of Jakob Steiner. Was it he who taught his students geometry in pitch darkness?

This in itself is a change from Greek conceptions of analysis and synthesis. I remember Lakatos had an interesting paper on the ‘Method of Analysis-Synthesis’ (in Vol. 2 of his Collected Papers). It was conceived originally more as a process, where one used both analysis and synthesis.

I rather suspect that your use here of the analytic/synthetic distinction marks a further development.

Posted by: David Corfield on July 19, 2013 10:23 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Hmm, okay, maybe I shouldn’t credit Euclid with this. But I think this meaning of synthetic/analytic has been used by others before, e.g. synthetic differential geometry is “synthetic” in the sense meant here.

Posted by: Mike Shulman on July 20, 2013 1:20 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

I certainly see the affinity with SDG. It might be worth someone taking the time to see how these terms have been adapted through time. The nLab page you mention has Sophus Lie using ‘synthetic’ presumably in Klein’s way. At one point it certainly had the sense of being more intuitive, coordinatisation distancing you from this. Kant must surely figure in the story.

On the subject of differential geometry, do you want slide 63 to give the impression that homotopy type theory will deal with manifolds by way of 0-truncation to sets, when we know the ‘natural’ path takes us via cohesive homotopy type theory and differential homotopy type theory?

Posted by: David Corfield on July 20, 2013 9:35 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Well, I really didn’t want to get into that for time reasons. Maybe it would have been better to choose a different example of set-theoretic mathematics than “manifolds”, but I’m not going to change the slides now.

Posted by: Mike Shulman on July 20, 2013 4:39 PM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

I wonder what the panorama of mathematics will look like from the point of view of HoTT. Will there be extensions other than ‘cohesive’ and ‘differential’, to make varieties of

*** homotopy type theory?

Posted by: David Corfield on July 21, 2013 9:48 AM | Permalink | Reply to this

Re: Synthetic ∞-Groupoid Theory

Well, we already have a proposal for directed homotopy type theory. I wouldn’t be surprised if other synthetic theories in 1-topos theory have higher topos versions, such as synthetic domain theory.

Posted by: Mike Shulman on July 21, 2013 6:00 PM | Permalink | Reply to this

Post a New Comment