Defining $SU(n)$ in HoTT

Question

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.

Answer 1

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".)

Answer 2

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.

Answer 3

As time passes I've become increasingly unhappy with my original answer, so I want to give a new one.

One of the most interesting things about HoTT is that it lets you ask questions of a logical flavor about homotopy theory. For example, I was on Robert Rose's defense committee where the thesis problem was suppose you look at a version of HoTT where you don't assume you have the natural numbers, but you do have the circle, what can you still say? Can you still show that you have infinite sets? In what sense of the word infinite? How much number theory do you still get? These are interesting questions about the logic of homotopy theory that you can't even ask in the usual space-based foundations (classically how are you going to even define the circle without having access to infinite sets?).

So what I'd say now is that the question of whether (and how) you can define BSU(n) in book HoTT is an extremely interesting "logical" question about homotopy theory. As Mike explains you can certainly do this if you give yourself a stronger type theory than book HoTT, so if your goal is to just give yourself these tools you can do so, but it's still interesting to ask whether you can do this with the weaker book HoTT.

In particular, as you well know, classically there's a homotopy coherent action of SO(n) on n-loops via the geometric action on $E_n$-algebras. But this definition is highly geometric, which makes it difficult in practice to understand what this action actually looks like. For example, you might want to understand the action of $SO(4)$ on 4-loops in an $\infty$-groupoid well enough to be able to write down the generator of $\pi_7(S^4)$ algebraically. Furthermore, you might want to know whether you can keep doing this in general. The question of whether you can define the group $SO(n)$ in book HoTT and define its action on $\Omega^n S^n$ in book HoTT gives you a logical framework for asking this question! So the fact that you can't easily define the group $SO(n)$ in book HoTT is a feature, not a bug, because it lets you precisely phrase this very interesting mathematical question. (Of course, since it's an interesting difficult question, simply stating the question doesn't get you very far towards solving it.)