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.

January 19, 2015

The Univalent Perspective on Classifying Spaces

Posted by Mike Shulman

I feel like I should apologize for not being more active at the Cafe recently. I’ve been busy, of course, and also most of my recent blog posts have been going to the HoTT blog, since I felt most of them were of interest only to the HoTT crowd (by which I mean, “people interested enough in HoTT to follow the HoTT blog” — which may of course include many Cafe readers as well). But today’s post, while also inspired by HoTT, is less technical and (I hope) of interest even to “classical” higher category theorists.

In general, a classifying space for bundles of XX’s is a space BB such that maps YBY\to B are equivalent to bundles of XX’s over YY. In classical algebraic topology, such spaces are generally constructed as the geometric realization of the nerve of a category of XX’s, and as such they may be hard to visualize geometrically. However, it’s generally useful to think of BB as a space whose points are XX’s, so that the classifying map YBY\to B of a bundle of XX’s assigns to each yYy\in Y the corresponding fiber (which is an XX). For instance, the classifying space BOB O of vector bundles can be thought of as a space whose points are vector spaces, where the classifying map of vector bundle assigns to each point the fiber over that point (which is a vector space).

In classical algebraic topology, this point of view can’t be taken quite literally, although we can make some use of it by identifying a classifying space with its representable functor. For instance, if we want to define a map f:BOBOf:B O\to B O, we’d like to say “a point vBOv\in B O is a vector space, so let’s do blah to it and get another vector space f(v)BOf(v)\in B O. We can’t do that, but we can do the next best thing: if blah is something that can be done fiberwise to a vector bundle in a natural way, then since Hom(Y,BO)Hom(Y,B O) is naturally equivalent to the collection of vector bundles over YY, our blah defines a natural transformation Hom(,BO)Hom(,BO)Hom(-,B O) \to Hom(-,B O), and hence a map f:BOBOf:B O \to B O by the Yoneda lemma.

However, in higher category theory and homotopy type theory, we can really take this perspective literally. That is, if by “space” we choose to mean “\infty-groupoid” rather than “topological space up to homotopy”, then we can really define the classifying space to be the \infty-groupoid of XX’s, whose points (objects) are XX’s, whose morphisms are equivalences between XX’s, and so on. Now, in defining a map such as our ff, we can actually just give a map from XX’s to XX’s, as long as we check that it’s functorial on equivalences — and if we’re working in HoTT, we don’t even have to do the second part, since everything we can write down in HoTT is automatically functorial/natural.

This gives a different perspective on some classifying-space constructions that can be more illuminating than a classical one. Below the fold I’ll discuss some examples that have come to my attention recently.

All of these examples have to do with the classifying space of “types equivalent to XX” for some fixed XX. Such a classifying space, often denoted BAut(X)B Aut(X), has the property that maps YBAut(X)Y \to B Aut(X) are equivalent to maps (perhaps “fibrations” or “bundles”) ZYZ\to Y all of whose fibers are equivalent (a homotopy type theorist might say “merely equivalent”) to XX. The notation BAut(X)B Aut(X) accords with the classical notation BGB G for the delooping of a (perhaps \infty-) group: in fact this is a delooping of the group of automorphisms of XX.

Categorically (and homotopy-type-theoretically), we simply define BAut(X)B Aut(X) to be the full sub-\infty-groupoid of Gpd\infty Gpd (the \infty-groupoid of \infty-groupoids) whose objects are those equivalent to XX. You might have thought I was going to say the full sub-\infty-groupoid on the single object XX, and that would indeed give us an equivalent result, but the examples I’m about to discuss really do rely on having all the other equivalent objects in there. In particular, note that an arbitrary object of BAut(X)B Aut(X) is an \infty-groupoid that admits some equivalence to XX, but no such equivalence has been specified.

Example 1: BAut(2)B Aut(2)

As the first example, let X=2={0,1}X = 2 = \{0,1\}, the standard discrete space with two points. Then Aut(2)=C 2Aut(2) = C_2, the cyclic group on 2 elements, and so BAut(2)=BC 2=K(C 2,1)B Aut(2) = B C_2 = K(C_2,1). Since C 2C_2 is an abelian group, BC 2B C_2 again has a (2-)group structure, i.e. we should have a multiplication operation BC 2×BC 2BC 2B C_2 \times B C_2 \to B C_2, an identity, inversion, etc.

Using the equivalence BC 2BAut(2)B C_2 \simeq B Aut(2), we can describe all of these operations directly. A point ZBAut(2)Z \in B Aut(2) is a space that’s equivalent to 22, but without a specified equivalence. Thus, ZZ is a set with two elements, but we haven’t chosen either of those elements to call “00” or “11”. As long as we perform constructions on ZZ without making such an unnatural choice, we’ll get maps that act on BAut(2)B Aut(2) and hence BC 2B C_2 as well.

The identity element of BAut(2)B Aut(2) it’s fairly obvious: there’s only one canonical element of BAut(2)B Aut(2), namely 22 itself. The multiplication is not as obvious, and there may be more than one way to do it, but after messing around with it a bit you may come to the same conclusion I did: the product of Z,WBAut(2)Z,W\in B Aut(2) should be Iso(Z,W)Iso(Z,W), the set of isomorphisms between ZZ and WW. Note that when ZZ and WW are 2-element sets, so is Iso(Z,W)Iso(Z,W), but in general there’s no way to distinguish either of those isomorphisms from the other one, nor is Iso(Z,W)Iso(Z,W) naturally isomorphic to ZZ or WW. It is, however, obviously commutative: Iso(Z,W)Iso(W,Z)Iso(Z,W) \cong Iso(W,Z).

Moreover, if Z=2Z=2 is the identity element, then Iso(2,W)Iso(2,W) is naturally isomorphic to WW: we can define Iso(2,W)WIso(2,W) \to W by evaluating at 020\in 2. Similarly, Iso(Z,2)ZIso(Z,2)\cong Z, so our “identity element” has the desired property.

Furthermore, if Z=WZ=W, then Iso(Z,Z)Iso(Z,Z) does have a distinguished element, namely the identity. Thus, it naturally equivalent to 22 by sending the identity to 020\in 2. So every element of BAut(2)B Aut(2) is its own inverse. The trickiest part is proving that this operation is associative. I’ll leave that to the reader (or you can try to decipher my Coq code).

(We did have to make some choices about whether to use 020\in 2 or 121\in 2. I expect that as long as we make those choices consistently, making them differently will result in equivalent 2-groups.)

Example 2: An incoherent idempotent

In 1-category theory, an idempotent is a map f:AAf:A\to A such that ff=ff \circ f = f. In higher category theory, the equality ff=ff \circ f = f must be weakened to an isomorphism or equivalence, and then treated as extra data on which we ought to ask for additional axioms, such as that the two induced equivalences fffff \circ f \circ f \simeq f coincide (up to an equivalence, of course, which then satisfies its own higher laws, etc.).

A natural question is if we have only an equivalence ffff \circ f \simeq f, whether it can be “improved” to a “fully coherent” idempotent in this sense. Jacob Lurie gave the following counterexample in Warning of Higher Algebra:

let GG denote the group of homeomorphisms of the unit interval [0,1][0,1] which fix the endpoints (which we regard as a discrete group), and let λ:GG\lambda : G \to G denote the group homomorphism given by the formula

λ(g)(t)={12g(2t) if0t12 t if12t1. \lambda(g)(t) = \begin{cases} \frac{1}{2} g(2t) & \quad if\; 0\le t \le \frac{1}{2}\\ t & \quad if\; \frac{1}{2}\le t \le 1. \end{cases}

Choose an element hGh\in G such that h(t)=2th(t)=2t for 0t140\le t\le \frac{1}{4}. Then λ(g)h=hλ(λ(g))\lambda(g)\circ h = h\circ \lambda(\lambda(g)) for each gGg\in G, so that the group homomorphisms λ,λ 2:GG\lambda,\lambda^2 : G\to G are conjugate to one another. It follows that the induced map of classifying spaces e:BGBGe:B G \to B G is homotopic to e 2e^2, and therefore idempotent in the homotopy category of spaces. However… ee cannot be lifted to a [coherent] idempotent in the \infty-category of spaces.

Let’s describe this map ee in the more direct way I suggested above. Actually, let’s do something easier and just as good: let’s replace [0,1][0,1] by Cantor space 2 2^{\mathbb{N}}. It’s reasonable to guess that this should work, since the essential property of [0,1][0,1] being used in the above construction is that it can be decomposed into two pieces (namely [0,12][0,\frac{1}{2}] and [12,1][\frac{1}{2},1]) which are both equivalent to itself, and 2 2^{\mathbb{N}} has this property as well:

2 2 +12 ×2 12 +2 .2^{\mathbb{N}} \cong 2^{\mathbb{N}+1} \cong 2^{\mathbb{N}} \times 2^1 \cong 2^{\mathbb{N}} + 2^{\mathbb{N}}.

Moreover, 2 2^{\mathbb{N}} has the advantage that this decomposition is disjoint, i.e. a coproduct. Thus, we can also get rid of the assumption that our automorphisms preserve endpoints, which was just there in order to allow us to glue two different automorphisms on the two copies in the decomposition.

Therefore, our goal is now to construct an endomap of BAut(2 )B Aut(2^{\mathbb{N}}) which is incoherently, but not coherently, idempotent. As discussed above, the elements of BAut(2 )B Aut(2^{\mathbb{N}}) are spaces that are equivalent to 2 2^{\mathbb{N}}, but without any such specified equivalence. Looking at the definition of Lurie’s λ\lambda, we can see that intuitively, what it does is shrink the interval to half of itself, acting functorially, and add a new copy of the interval at the end. Thus, it’s reasonable to define e:BAut(2 )BAut(2 )e:B Aut(2^{\mathbb{N}}) \to B Aut(2^{\mathbb{N}}) by

e(Z)=Z+2 .e(Z) = Z + 2^{\mathbb{N}}.

Here ZZ is some space equivalent to 2 2^{\mathbb{N}}, and in order for this map to be well-defined, we need to show is that if ZZ is equivalent to 2 2^{\mathbb{N}}, then so is Z+2 Z + 2^{\mathbb{N}}. However, the decomposition 2 2 +2 2^{\mathbb{N}} \cong 2^{\mathbb{N}} + 2^{\mathbb{N}} ensures this. Moreover, since our definition didn’t involve making any unnatural choices, it’s “obviously” (and in HoTT, automatically) functorial.

Now, is ee incoherently-idempotent, i.e. do we have e(e(Z))e(Z)e(e(Z))\cong e(Z)? Well, that is just asking whether

(Z+2 )+2 is equivalent toZ+2 (Z + 2^{\mathbb{N}}) + 2^{\mathbb{N}} \quad\text{is equivalent to}\quad Z + 2^{\mathbb{N}}

but this again follows from 2 2 +2 2^{\mathbb{N}} \cong 2^{\mathbb{N}} + 2^{\mathbb{N}}! Showing that ee is not coherent is a bit harder, but still fairly straightforward using our description; I’ll leave it as an exercise, or you can try to decipher the Coq code.

Example 3: Natural pointed sets

Let’s end by considering the following question: in what cases does the natural map BS n1BS nB S_{n-1} \to B S_{n} have a retraction, where S nS_n is the symmetric group on nn elements? Looking at homotopy groups, this would imply that S n1S nS_{n-1} \hookrightarrow S_n has a retraction, which is true for n<5n\lt 5 but not otherwise. But let’s look instead at the map on classifying spaces.

The obvious way to think about this map is to identify BS nB S_n with BAut(n)B Aut(\mathbf{n}), where n\mathbf{n} is the discrete set with nn elements, and similarly BS n1B S_{n-1} with BAut(n1)B Aut(\mathbf{n-1}). Then an element of BAut(n1)B Aut(\mathbf{n-1}) is a set ZZ with n1n-1 elements, and the map BS n1BS nB S_{n-1} \to B S_{n} takes it to Z+1Z+1 which has nn elements.

However, another possibility is to identify BS n1B S_{n-1} instead with the classifying space of pointed sets with nn elements. Since an isomorphism of pointed sets must respect the basepoint, this gives an equivalent groupoid, and now the map BS n1BS nB S_{n-1} \to B S_{n} is just forgetting the basepoint. With this identification, a putative retraction BS nBS n1B S_{n} \to B S_{n-1} would assign, to any set ZZ with nn elements, a pointed set (r(Z),r 0)(r(Z),r_0) with nn elements. Note that the underlying set r(Z)r(Z) need not be ZZ itself; they will of course be isomorphic (since both have nn elements), but there is no specified or natural isomorphism. However, to say that rr is a retraction of our given map says that if ZZ started out pointed, then (r(Z),r 0)(r(Z),r_0) is isomorphic to (Z,z 0)(Z,z_0) as pointed sets.

Let’s do some small examples. When n=1n=1, our map rr has to take a set with 1 element and assign to it a pointed set with 1 element. There’s obviously a unique way to do that, and just as obviously if we started out with a pointed set we get the same set back again.

The case n=2n=2 is a bit more interesting: our map rr has to take a set ZZ with 2 elements and assign to it a pointed set with 2 elements. One option, of course, is to define r(Z)=2r(Z)=2 for all ZZ. Since every pointed 2-element set is uniquely isomorphic to every other, this satisfies the requirement. Another option motivated by example 1, which is perhaps a little more satisfying, would be to define r(Z)=Iso(Z,Z)r(Z) = Iso(Z,Z), which is pointed by the identity.

The case n=3n=3 is more interesting still, since now it is not true that any two pointed 3-element sets are naturally isomorphic. Given a 3-element set ZZ, how do we assign to it functorially a pointed 3-element set? The best way I’ve thought of is to let r(Z)r(Z) be the set of automorphisms fIso(Z,Z)f\in Iso(Z,Z) such that f 3=idf^3 = id. This has 3 elements, the identity and two 3-cycles, and we can take the identity as a basepoint. And if ZZ came with a point z 0z_0, then we can define an isomorphism Zr(Z)Z \cong r(Z) by sending zZz\in Z to the unique fr(Z)f\in r(Z) having the property that f(z 0)=zf(z_0)= z.

The case n=4n=4 is somewhat similar: given a 4-element set ZZ, define r(Z)r(Z) to be the set of automorphisms fIso(Z,Z)f\in Iso(Z,Z) such that f 2=idf^2 = id and whose set of fixed points is either empty or all of ZZ. This has 4 elements and is pointed by the identity; in fact, it is the permutation representation of the Klein four-group. And once again, if ZZ came with a point z 0z_0, we can define Zr(Z)Z \cong r(Z) by sending zZz\in Z to the unique fr(Z)f\in r(Z) such that f(z 0)=zf(z_0)= z.

I will end with a question that I don’t know the answer to: is there any way to see from this perspective on classifying spaces that such a retraction doesn’t exist in the case n=5n=5?

Posted at January 19, 2015 6:25 PM UTC

TrackBack URL for this Entry:

15 Comments & 0 Trackbacks

Re: The Univalent Perspective on Classifying Spaces

(typography: the later C nC_ns … did we mean S nS_n or 𝔖 n&#120086;_n, perhaps? Of course we want to avoid Σ in the present context)

Posted by: Jesse C. McKeown on January 20, 2015 3:48 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Duhh, yes. Thanks, fixed.

Posted by: Mike Shulman on January 20, 2015 11:23 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

I don’t think Iso(Z,W)\text{Iso}(Z, W) is morally correct, among other things because it’s naturally a contravariant functor in the first variable. Consider, for example, the case of invertible modules over a commutative ring RR; the 22-group structure here comes not from the hom (which fails even to be commutative) but instead the tensor product, which gives us B 2B \mathbb{Z}_2 when R=𝔽 3R = \mathbb{F}_3. This operation is covariant in both variables, clearly commutative, and clearly associative, even coherently.

Let’s take a closer look at the tensor product of 11-dimensional vector spaces over 𝔽 3\mathbb{F}_3 to see what this construction is actually doing. Such a vector space can be identified with the two nonzero elements in it, which are swapped with each other under multiplication by 2=1𝔽 32 = -1 \in \mathbb{F}_3. If {0,v 1,v 2}\{ 0, v_1, v_2 \} and {0,w 1,w 2}\{ 0, w_1, w_2 \} are two such vector spaces, with v 2=2v 1=v 1,w 2=2w 1=w 1v_2 = 2 v_1 = - v_1, w_2 = 2 w_1 = -w_1, then their tensor product is {0,v 1w 1,v 2w 1}\{ 0, v_1 \otimes w_1, v_2 \otimes w_1 \} where v 1w 1=v 2w 2v_1 \otimes w_1 = v_2 \otimes w_2 and v 2w 1=v 1w 2v_2 \otimes w_1 = v_1 \otimes w_2.

So, as an operation on 22-element sets, the tensor product of 11-dimensional vector spaces over 𝔽 3\mathbb{F}_3 corresponds to the following construction: take the cartesian product, which is a 44-element set, then take orbits under the diagonal action of 2\mathbb{Z}_2, which is a 22-element set. In other words, we are thinking of 22-element sets as 2\mathbb{Z}_2-torsors and the 22-group structure on B 2B \mathbb{Z}_2 comes from taking the tensor product of 2\mathbb{Z}_2-torsors. This description generalizes to the case that 2\mathbb{Z}_2 is replaced by any abelian group and should work internally to many contexts.

Posted by: Qiaochu Yuan on January 20, 2015 7:31 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Well, I don’t really find the fact that groupoids are self-dual to be morally wrong. (-: In fact, it’s a big part of the reason why homotopy type theory is easier than directed type theory. I also believe the definition as Iso(Z,W)Iso(Z,W) should work for torsors over any abelian group, and it has the advantage of not requiring any colimits — so, for instance, we can define it in HoTT without HITs (other than propositional truncation to define BAutB Aut).

But your alternative description is also nice to have; thanks!. It’s not hard to see that it’s isomorphic to the definition I gave: a pair zwZWz\otimes w \in Z\otimes W corresponds to the unique isomorphism ZWZ\cong W that sends zz to ww. This isomorphism is natural on the groupoids of 2-element sets or 1-dimensional 𝔽 3\mathbb{F}_3-modules, and unless I’m mistaken is moreover dinatural on the category of the latter — and this should also generalize to torsors over any abelian group.

Posted by: Mike Shulman on January 20, 2015 11:50 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

This is a minor point, but… it doesn’t seem to me that Iso(Z, W) is naturally a contravariant functor in the first variable. An arbitrary map from Z’ to Z doesn’t give us a map from Iso(Z, W) to Iso(Z’, W). Rather, it seems to me Iso(Z, W) is naturally an “isovariant” functor in both variables, and I would not normally think of “isovariance” as having separate co- and contra-variant flavors; my own morals are to view the situation with respect for its complete symmetry.

(This isn’t to quibble with anything else; I do often think of the group structure on 2-element sets in terms of tensor products of 2\mathbb{Z}_2-torsors)

Posted by: Sridhar Ramesh on January 23, 2015 10:31 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

I mean it’s a contravariant functor on the groupoid, of course. I think identifying left and right actions of groups or groupoids without explicitly saying that you’re doing so is bad categorical hygiene in the same way that identifying the tangent and cotangent bundles of a Riemannian manifold without explicitly saying that you’re doing so is bad categorical hygiene.

Posted by: Qiaochu Yuan on February 2, 2015 9:36 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

This is actually a really interesting point. What you say about categorical hygiene is very natural from the perspective of a category theorist, who thinks of groupoids as special categories. But from the perspective of a homotopy theorist, who thinks of groupoids as special homotopy types (1-types), there is no sense in asking whether a map between them is “contravariant or covariant”; all maps are just “isovariant” in the same way.

Posted by: Mike Shulman on February 2, 2015 11:50 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Hm… I often would not identify tangent and cotangent bundles because I often am not in a context where there is a canonical isomorphism between them (e.g., in ordinary space in the physical universe, we do not have a “dimensionless” dot product, but rather, a dot product valued in squared distances, which have no distinguished unit, and thus there is no canonical isomorphism between vectors and covectors). It is good hygiene to not introduce a non-canonical identification, thus reminding oneself of the symmetries of the situation (between the various different non-canonical identifications possible).

But in a situation where there is a canonical isomorphism (e.g., between a groupoid and its dual), it seems to me much less “unhygienic” to construe such an isomorphism as an identification. In fact, in this case, it would be the drawing of distinctions between a supposedly contravariant first argument and covariant second argument in Iso(V, W) which would be obscuring the symmetries of the situation!

[But, again, I agree that the group structure on 2-element sets is more naturally understood in terms of tensor products than the Iso functor, making associativity, etc., obvious. This irrelevant quibbling is just as to the side issue of how to think hygienically about the Iso functor.]

Posted by: Sridhar Ramesh on February 12, 2015 11:17 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Okay, I’m confused by a lot of things now:

  1. Why should BAut(X)\mathbf{B}\mathrm{Aut}(X) have terms given by types merely isomorphic to XX? I would have thought that BG\mathbf{B}G would have terms given by GG-torsors, since BG\mathbf{B}G classifies GG-principal bundles and a fiber of a GG-principal bundle is a GG-torsor. If that’s right, then I’m confused because typically an Aut(X)\mathrm{Aut}(X)-torsor is a very different thing from a type merely isomorphic to XX: for example, a 3-element set doesn’t carry a natural action of S 3S_3, and 3-element sets don’t even have the same number of elements as S 3S_3-torsors. If there’s an equivalence of types here, then it’s “non-concrete” and I don’t see it. In the case X=2X=2, I suppose these descriptions are the same because a 2-element set is naturally an S 2S_2-torsor.

  2. Qiaochu, how does your construction generalize to arbitrary abelian groups? I must be misunderstanding something because it seems to me that it only generalizes to groups which are the multiplicative group of a field.

  3. Mike, are you claiming that your definition of multiplication generalizes to other groups? I haven’t looked at your code, but the associativity proof I came up with Iso(Iso(A,B),C)Iso(A,Iso(B,C))\mathrm{Iso}(\mathrm{Iso}(A,B),C) \to \mathrm{Iso}(A,\mathrm{Iso}(B,C)) was gλa.λb.g(h a,b)g \mapsto \lambda a.\lambda b. g(h_{a,b}) where h a,bh_{a,b} is the unique isomorphism mapping aa to bb. This doesn’t look like it will readily generalize, regardless of how BG\mathbf{B}G is defined.

Posted by: Tim Campion on January 23, 2015 1:28 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

The torsor construction works very nicely for groups we already know as groups, and even better for discrete groups with solvable word problem; but that doesn’t mean other constructions are wrong! The example of BAut(X){Y&YX 0}\mathbf{B} Aut(X) \simeq \{ Y \& \| Y \simeq X \|_0 \} is a case of on the other hand, starting from something XX from which a canonical group Aut(X)Aut (X) can be constructed. The equivalence is essentially just the content of the univalence axiom specialized to types isomorphic to XX. If you like, that’s why you can’t see it: it’s an independent axiom.

Posted by: Jesse C. McKeown on January 23, 2015 4:06 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Right, there can be lots of different-looking ways to define BGB G. An Aut(X)Aut(X)-torsor doesn’t look the same as a set merely isomorphic to XX, but the groupoid of Aut(X)Aut(X)-torsors is equivalent to the groupoid of sets merely isomorphic to XX. One way to define such an equivalence is that if ZZ is merely isomorphic to XX, then Iso(Z,X)Iso(Z,X) is an Aut(X)Aut(X)-torsor.

It’s easy to get confused when the group is C 2=S 2=Aut(2)C_2 = S_2 = Aut(2), since C 2C_2 itself has two elements and hence is merely isomorphic to 22, and moreover any set merely isomorphic to 22 comes itself with a canonical C 2C_2-action. Neither of those is true for the group G=Aut(X)G = Aut(X) for other values of XX.

Another way to define BGB G, which works for any group GG, is the obvious one: it has one object with GG as its automorphisms. (That doesn’t work in HoTT in exactly the same way, but there is a similar definition using a HIT.)

Qiaochu’s construction generalizes to arbitrary groups by using torsors rather than vector spaces, as Jesse said. (I’m not actually sure why he brought vector spaces into it at all.)

The definition of multiplication that I gave above does not generalize directly to other groups, and it had better not, because Aut(X)Aut(X) is not generally abelian, so that BAut(X)B Aut(X) doesn’t generally have a group structure! What I meant to say is that if we instead use torsors for an arbitrary abelian group GG, then we can define the multiplication using the hom just as well as with the tensor.

Posted by: Mike Shulman on January 23, 2015 7:01 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

I brought in vector spaces in part because I thought they would be more familiar than torsors and in part because looking for a construction that makes sense on the category of vector spaces rather than on the groupoid of 11-dimensional vector spaces makes it easier to notice the tensor product as a good candidate.

Posted by: Qiaochu Yuan on February 2, 2015 9:40 PM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

The link to the Coq code given in Example 1 doesn’t work, but this link seems to do the right thing:

Posted by: Dan Christensen on January 30, 2015 12:06 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

Thanks, fixed. Sorry about that; the pull request to the main library got merged, but I hadn’t managed to update the link yet.

Posted by: Mike Shulman on January 30, 2015 5:54 AM | Permalink | Reply to this

Re: The Univalent Perspective on Classifying Spaces

I hope someday someone writes an introductory text on homotopy theory which takes the HoTT perspective throughout. If it were written well it might be easier than the usual approach.

Posted by: John Baez on February 4, 2015 1:22 AM | Permalink | Reply to this

Post a New Comment