35
$\begingroup$

From a recent answer by Mike Shulman, I read:

"HoTT is (among other things) a foundational theory, on roughly the same ontological level as ZFC, whose basic objects can be regarded as $\infty$-groupoids"

Now, $\infty$-groupoids are the same thing as spaces, and I have a couple of spaces which I like.
Here's one which I like a lot: the Lie group $SU(n)$.

Question:
How do I say "let $X:=SU(n)$" in HoTT?

Here, $n$ can be either a variable, or a definite number (say $3$).

Disclaimer: I (unfortunately) don't know much about HoTT. So please be gentle.

$\endgroup$
  • 3
    $\begingroup$ Well, for starters, $SU(2)$ is a $3$-sphere $S^3$, and my understanding is that spheres can be presented in HoTT as higher inductive types: the $3$-sphere in particular I think can be presented in a way that amounts to saying "the free $\infty$-groupoid on a $3$-automorphism" (although I don't actually know enough about HoTT to verify this). $\endgroup$ – Qiaochu Yuan Jan 2 '18 at 0:47
  • 2
    $\begingroup$ Thank you Qiaochu. Yes, I was aware of that. But $SU(2)$ is quite special, and I was conscious not to say "(say $n=2$)" in my formulation of the question. $\endgroup$ – André Henriques Jan 2 '18 at 1:27
  • 2
    $\begingroup$ Another option is to try defining $BSU(n)$ instead of $SU(n)$, then taking loop spaces. Naively (probably I know even less about HoTT than you) this comes down to defining its functor of points, so defining complex vector bundles equipped with a complex orientation. $\endgroup$ – Qiaochu Yuan Jan 2 '18 at 2:16
  • 1
    $\begingroup$ There are two big problems with defining geometric objects like $SU(n)$ in HoTT. The first is that HoTT works only up to homotopy equivalence, so many basic objects like $\mathbb R^n$ are not natively definable (other than by a verbatim reproduction of set-theoretic definitions). The second is that HoTT is the language of higher topoi, so if you can define things like K-theory, bordisms and chromatic filtration, then you know how to do it in arbitrary topos, including examples like equivariant and motivic topoi. I don't know what should be complex bordism in those categories. $\endgroup$ – Anton Fetisov Jan 2 '18 at 4:26
  • 3
    $\begingroup$ In particular, if $\mathbb{S}^1= \{ (x,y) \mid x^2+y^2=1\}$ denotes the topological circle in cohesive HoTT, and $\mathrm{Vect}$ is the type of vector spaces defined naively, with no explicit attention paid to "topology" or "groupoid" information in either case, then it happens automatically in cohesive HoTT that maps $\mathbb{S}^1 \to \mathrm{Vect}$ represent (not necessarily flat or trivial) continuous vector bundles over the topological circle. So I believe that (cohesive) HoTT really does do what you want. $\endgroup$ – Mike Shulman Jan 2 '18 at 18:28
23
$\begingroup$

This isn't easy to do, and the reason it isn't easy is because of the step "$\infty$-groupoids are the same thing as spaces." Of course the homotopy hypothesis tells you that any $\infty$-groupoid is equivalent to the fundamental $\infty$-groupoid of a space, but that doesn't mean that they're literally the same thing. The way that HoTT approaches about $\infty$-groupoids is not by thinking of them as spaces. What's easy in HoTT is to do something like, "consider the $\infty$-groupoid freely generated by a single point and a single 1-path from that point to itself." This $\infty$-groupoid is equivalent to the fundamental $\infty$-groupoid of classical circle, but we haven't constructed it that way, instead we've constructed it algebraically via generators/relations.

Ok, so the first thing you could do is find an "algebraic" description of the fundamental $\infty$-groupoid of $\mathrm{SU}(n)$. Essentially this is giving an explicit CW-decomposition of $\mathrm{SU}(n)$. I'm not sure how hard this is off the top of my head, but one needs to be a bit careful with such an approach to make sure to get something that's just as useful as $\mathrm{SU}(n)$ in practice. For example, as suggested in comments it would be better to construct $B\mathrm{SU}(n)$ instead so that when you take the loop space you know you have a group structure. But you also want to be able to handle things like the relationship between $\mathrm{SU}(n)$ and complex vector bundles, and if your construction is sufficiently messy and computational then it might not be good enough.

Instead, you could try to build up the theory of manifolds (or something similar) inside HoTT and then define a notion of fundamental $\infty$-groupoid. If I understand things right, this is something that real cohesive type theory will let you do. But there's a lot you need to do in order to get there, for a first step you need to define $\mathbb{R}$ inside HoTT which has some tricky points because HoTT is naturally constructive, but the Cauchy reals and the Dedekind reals are different constructively. In HoTT $\infty$-groupoids are foundational native objects, but $\mathbb{R}$ is still just as complicated (well, slightly more complicated) as it was classically. From there you can start trying to define manifolds (or some more general notion of a topological space of similar flavor to manifolds) and then defining the fundamental $\infty$-groupoid of such a space. All of this is done in Mike's paper where he develops a type-theory for topological $\infty$-groupoids. The theory there is developed to the point where he shows that $\{(x,y)\in \mathbb{R}^2: x^2+y^2=1\}$ is something that you can take the fundamental $\infty$-groupoid (or "shape") which outputs an $\infty$-groupoid and that the answer you get is equivalent to the type-theoretic circle. If I understand everything correctly, you should be able to use this to define the shape of any real algebraic manifold (including $\mathrm{SU}(n)$), as well as many other "geometrically" defined topological spaces.

In conclusion, HoTT does let you deal with $\infty$-groupoids nicely and directly, but doesn't easily give you access to $\infty$-groupoids that are of a topological nature rather than an algebraic nature. In order to access those you still need to build up real analysis and topology or some replacement for them, which takes a bit of work (as it does classically) and also has a few tricky points due to the constructive nature of HoTT.

$\endgroup$
  • 8
    $\begingroup$ If this is true, then this sounds like a HUGE drawback of HoTT. One of the strengths of algebraic topology is that spaces come from so many different types of constructions: there's Eilenberg MacLane space (among other spaces defined via their Postnikov towers), there's spheres (and other spaces defined via their cell structures), but then there's many more spaces which are defined by ways which are not directly related to their Postnikov towers, nor to their cell structures. $SU(n)$ is just the first example: I would call them "God given spaces" $\endgroup$ – André Henriques Jan 2 '18 at 1:44
  • 5
    $\begingroup$ I'd like to point and that it's by relying on the information given by those "God given spaces" that some of the deepest results of homotopy theory have been achieved. For example, the chromatic filtration in stable homotopy theory relies heavily on the existence of complex cobordism $MU$. And the latter is constructed by using, at its very base, the unitary groups... Similarly for $K$-theory: it's constructed using the unitary groups. So if we can't define the groups $U(n)$, then that sounds really bad. $\endgroup$ – André Henriques Jan 2 '18 at 1:48
  • 3
    $\begingroup$ Yes it's a drawback, and one certainly needs to eventually be able to talk about $SU(n)$. No approach is going to make everything easy, and the price of making some things easier is making other things harder. So I don't think it's terrible that talking about $SU(n)$ is harder in HoTT than it is from a topological viewpoint, so long as it's not too hard. $\endgroup$ – Noah Snyder Jan 2 '18 at 1:52
  • 7
    $\begingroup$ I really shouldn't rant before learning the subject (I use this opportunity to apologise). The answer to my question might actually be contained in what you wrote, in the form of real cohesive type theory. So my question then becomes: "How does one define $SU(n)$ in real cohesive type theory?" Or possibly: "Is real cohesive type theory already developed enough so that one can use it to define $SU(n)$?" $\endgroup$ – André Henriques Jan 2 '18 at 1:57
  • 2
    $\begingroup$ This answer reinforces my outsider's impression that HoTT is more oriented toward making the theory easier than illuminating concrete examples - I regret lacking the courage to ask a naive question like this one. But you also make it sound as though there are other examples which are more natural in this language; do these examples correspond to familiar constructions in "ordinary" mathematics? $\endgroup$ – Paul Siegel Jan 2 '18 at 7:52
24
$\begingroup$

I think Noah's answer is mostly right, but partly misleading, and explaining why will take too much space for a comment, so I'm posting a separate answer.

As Noah says, the main conceptual point is that HoTT forces us to un-confuse ourselves about the difference between a topological space and an $\infty$-groupoid, which are conceptually distinct but historically have been conflated in algebraic topology. (Actually, higher topos theory already pushes us in that direction, but HoTT is more insistent.)

On the other hand, the main technical point is that in "Book HoTT" we don't know how to define the "fundamental $\infty$-groupoid" functor that takes a topological space to its associated $\infty$-groupoid. Two important things to emphasize about this sentence are (1) it's a statement about a particular formal system (the one used in the HoTT Book), which is just one piece of the subject area of HoTT, and (2) it's (currently) a statement about ignorance rather than impossibility. However, it does have two important upshots:

  1. In Book HoTT, to define a particular $\infty$-groupoid, you have to define it as an $\infty$-groupoid, i.e. using purely $\infty$-groupoidal notions; you can't "cheat" by defining it to be the fundamental $\infty$-groupoid of some topological space. (The definition also has to be "finitary" in some sense — it can use infinitary constructions, but they have to be finitely expressible such as by induction over the internal natural numbers.)

  2. In Book HoTT, you are out of luck if you want to use topological spaces to prove things about their fundamental $\infty$-groupoids, or use fundamental $\infty$-groupoids to prove things about their originating topological spaces.

These problems, though significant, are part of the reason I said in the linked-to answer that "the promise of HoTT is not yet fully realized". Keep in mind that HoTT is only a few years old; we are already working on various ways to solve them.

The first of them is much less of an an insurmountable obstacle than you might think. Quite often, it turns out that an $\infty$-groupoid that's classically defined from some topological space also has a very natural presentation in purely $\infty$-categorical language, which can sometimes yield important new insight about it and enables new clean proofs in synthetic homotopy theory. The simplest example is the spheres: as Qiaochu mentioned in a comment, $S^n$ can be defined as freely generated by a point and an $n$-automorphism. Any CW-complex decomposition of a space is also a free presentation of its fundamental $\infty$-groupoid, though to be expressible in HoTT such a decomposition must be finite or "finitarily definable" (by internal induction). And classifying spaces can easily be defined using the univalent universe; see this blog post for instance. And recently, Ulrik Buchholtz and Egbert Rijke have made an important advance in unifying the latter two approaches to classifying spaces, using classification information as a way to finitarily present a CW-complex decomposition; in this paper they apply it to real projective spaces, but I think similar ideas should work rather more generally.

I don't know whether anyone has written down a definition of the $\infty$-groupoid $SU(n)$ in particular, but I'm confident that it will be possible. In fact it will probably be better to directly construct its classifying space $BSU(n)$ and then define $SU(n) = \Omega BSU(n)$, since that way the group structure of $SU(n)$ will arise automatically (delooping arbitrary $\infty$-groupoids is another thing we don't know how to do inside Book HoTT). I disagree with Noah that this would "not be constructing $SU(n)$ but something else equivalent to it": it would be a perfectly valid construction of the $\infty$-groupoid $SU(n)$, and an $\infty$-groupoid is only defined up to equivalence. What it wouldn't be is a proof that that $\infty$-groupoid is the fundamental $\infty$-groupoid of some topological space. Of course the name "$SU(n)$" for this $\infty$-groupoid is derived from the topological space of which classically it is the fundamental $\infty$-groupoid, but that accident of history is no reason to denigrate the existence of the $\infty$-groupoid in its own right.

The second problem above is rather more problematic, and there are various ways one might try to solve it. To start with, one might hope to prove that fundamental $\infty$-groupoids are definable in Book HoTT; but I don't know of anyone working on this, and I think the general feeling seems to be that it's probably not possible.

The other possibility is to introduce formal systems that are better than Book HoTT. Since the obstacle to defining fundamental $\infty$-groupoids in Book HoTT is their infinitary nature (you have to say "continuous maps $D^k \to X$ induce $k$-dimensional paths in $\Pi_\infty(X)$" for all $k$, coherently), the "obvious" way to proceed is to enhance it with ways to talk about infinitary things more cleanly. Here I think the state of the art is two-level type theory, a constellation of formal systems and ideas revolving around the idea of re-introducing (in a controlled way) the sort of "strict point-set-level equality" that Book HoTT mostly eschews. I don't think anyone has just yet applied this to defining fundamental $\infty$-groupoids, but it should be quite possible.

Another possibility is cohesive HoTT, which is less obvious and requires more re-training of our intuition, but in my opinion yields a more elegant result. Contrary to the former approach (and what Noah implied), cohesive HoTT does not require you to explicitly define manifolds, topological spaces, or even fundamental $\infty$-groupoids! In fact this is precisely the point: just as "plain" HoTT is a foundational theory whose basic objects can be regarded as $\infty$-groupoids, cohesive HoTT is a foundational theory whose basic objects can be regarded as topological $\infty$-groupoids (the motivating model consists of $\infty$-stacks on the site of Euclidean spaces $\mathbb{R}^n$). So just as in plain HoTT you don't need to define all the "$k$-simplices" of $S^n$ separately but they arise automatically from its presentation via generators and relations, in cohesive HoTT you don't need to define the topology of $\mathbb{R}^n$ explicitly but it arises automatically from the definition of the set $\mathbb{R}$ using Dedekind cuts. Moreover, you don't need to define the fundamental groupoid functor by explicitly specifying its $k$-paths either; it has a simple universal property relating this sort of "intrinsic topology" to the "intrinsic $\infty$-groupoidness" of plain HoTT.

So in conclusion, in cohesive HoTT you can define the $\infty$-groupoid $SU(n)$ more easily than in classical algebraic topology. Define $\mathbb{R}$ using Dedekind cuts, define $\mathbb{C}$ in the obvious way, and define the set $SU(n) \subseteq \mathbb{C}^{n^2}$ using the usual algebraic formulas, then apply the fundamental $\infty$-groupoid functor (which in cohesive HoTT is called its "shape", written ʃ $SU(n)$). You don't need to think about the topology of $\mathbb{C}$ or the manifold structure of $SU(n)$ at all; that gets carried along for the ride automatically. (You do, however, need to be a little careful to do things in the correct "constructive" way, which for instance means using the correct constructive notion of "Dedekind cut".)

$\endgroup$
  • 3
    $\begingroup$ Another request for clarification: From your words "I don't know whether anyone has written down a definition of the ∞-groupoid SU(n) in particular, but I'm confident that it will be possible", I'm not able to tell whether [a] this is something which is in principle easy, but no one happens to have done it, or [b] this is something for which you have essentially no idea how to do it, but you're optimistic about the future. Could you please comment. $\endgroup$ – André Henriques Jan 2 '18 at 13:24
  • 2
    $\begingroup$ @AndréHenriques Noah's answer to the question about the cohesive approach is correct. For instance, $\mathbb{C} = \mathbb{R}\times\mathbb{R}$ with $(x,y)\cdot (u,v) = (x u - y v , x v + y u)$ and so on. Since this is all happening at set-level (before step (4)), there is no coherence to worry about, and one can treat $n$ as a variable in type theory just the way one does it in set theory. $\endgroup$ – Mike Shulman Jan 2 '18 at 17:00
  • 2
    $\begingroup$ As for the $\infty$-groupoid $SU(n)$, I would say the situtaion is in between [a] and [b]. Before the Buchholtz-Rijke paper I would have said [b], but now we have a general technique that should be applicable to constructions of this sort, so I would say it's no longer the case that we have "no idea" how to do it: we do have ideas. However, neither would I say it's "easy" since some additional thought and ideas will probably be required: it'll be a new application of a not-yet-fully-explored technique. (It could also be that I'm wrong and their technique won't help so much.) $\endgroup$ – Mike Shulman Jan 2 '18 at 17:02
  • 3
    $\begingroup$ There's a short description of our HoTT version of the Milnor construction of projective spaces for any $\infty$-group in these talk notes. We thought a bit about using the Schubert calculus to define at least the types SU(n), but one really wants the deloopings. It's still an open problem to define the delooping BSU(2), or any other delooping of $S^3$, in Book HoTT. Egbert has a different approach using $\infty$-equivalence relations, but no construction yet. I like Mike's cohesive approach as the most elegant way. $\endgroup$ – Ulrik Buchholtz Jan 2 '18 at 17:22
  • 5
    $\begingroup$ By the way, I regret that my real-cohesion paper is so long. It's that long because I tried to be fairly comprehensive about describing the behavior of the modalities, so the paper could function as a reference for future work in cohesive HoTT. But the basic ideas can be described much more briefly; check out the long and chatty introduction to the paper, and these talk slides: home.sandiego.edu/~shulman/papers/realcohesion-cmu2017.pdf . $\endgroup$ – Mike Shulman Jan 2 '18 at 18:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.