# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 2nd 2011

added to circle the (a) definition as a homotopy type and formalized in homotopy type theory

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeJan 6th 2014

The HoTT links at circle were very out of date, so I have updated them.

• CommentRowNumber3.
• CommentAuthorColin Tan
• CommentTimeJul 17th 2014
Mentioned that Daniel and Mike's paper in fact proves that the loop space of the circle is the free group on one generator.
• CommentRowNumber4.
• CommentAuthorColin Tan
• CommentTimeJul 17th 2014
Is it (unconditionally) true that the loop space of the circle in every Grothendieck (oo,1)-topos is the free oo-group on one generator? This is true conditionally on the folklore claim that homotopy type theory is the internal language of every Grothendieck (oo,1)-topos.
• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJul 17th 2014

Let

$\mathbf{H} \stackrel{\overset{\Delta}{\longleftarrow}}{\underset{\Gamma}{\longrightarrow}} \infty Grpd$

be any Grothendieck $\infty$-topos.

Then if by “the circle” in $\mathbf{H}$ one means the image under $\Delta$ of the circle in $\infty Grpd \simeq L^s_{whe} Top$, then the answer is “yes”: because the inverse image $\Delta$ preserves finite $\infty$-limits and hence preserves the looping relation in $\infty Grpd$. Also the natural numbers object is preserved by $\Delta$ (see here).

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeJul 17th 2014

Note that one can also mean by “the circle” the object freely generated by a point and a loop, e.g. the (homotopy) coequalizer of $1\rightrightarrows 1$. This is the same as what Urs said since $\Delta$ is cocontinuous.

• CommentRowNumber7.
• CommentAuthorColin Tan
• CommentTimeJul 19th 2014
• (edited Jul 19th 2014)
I've included a proof that the loop space of the circle is the free group on one generator. I'm hoping that this proof can be modified to give a proof internal to a general Grothendieck (oo,1)-topos.
• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJul 19th 2014

• CommentRowNumber9.
• CommentAuthorColin Tan
• CommentTimeJul 20th 2014

Wrote up a proof sketch at suspension object that more generally, for X a pointed object in a Grothendieck (oo,1)-topos, suspending is homotopy equivalent to smashing with the classifying space of the discrete group of integers. Removed my earlier addition at circle and replaced it by appealing to this general result in the particular case when X is the two-point space.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeJul 21st 2014

That seems to me like a very roundabout argument. Isn’t it easier to prove that $\Omega S^1 = \mathbb{Z}$ directly and then observe that suspension is the same as smashing with $S^1$?

• CommentRowNumber11.
• CommentAuthorColin Tan
• CommentTimeJul 21st 2014

Probably my attempt was to argue from the oo-categorial Giruad axioms. Could one prove $\Omega S^1 \simeq {\mathbb{Z}}$ directly from these axioms?

• CommentRowNumber12.
• CommentAuthorColin Tan
• CommentTimeJul 21st 2014
• (edited Jul 21st 2014)

On reflection, it does seem my manner of argument is rather roundabout (although I hope it is not circular).

To spell it out: 1) Prove that $\Sigma X \simeq K({\mathbb{Z}},1) \wedge X$. 2) In particular, when setting $X = S^0$, this gives $S^1 \simeq K(\mathbb{Z},1)$. Deduce the following two corollaries: A) Looping 2) gives $\Omega S^1 \simeq {\mathbb{Z}}$. B) Substituting 2) into 1) gives $\Sigma X \simeq S^1 \wedge X$.

Is there a way to prove (axiomatically) A without first proving 1?

Some logical dependencies: 2 and A are logically equivalent. 1+A implies B, as you noted.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeJul 22nd 2014

Perhaps the simplest $(\infty,1)$-categorical argument is to note the (homotopy) coequalizer diagrams $1 \rightrightarrows 1 \to S^1$ and $\mathbb{Z} \rightrightarrows \mathbb{Z} \to 1$, where one map $\mathbb{Z}\to \mathbb{Z}$ is the identity and the other is the successor. Then observe that you have a natural transformation from the latter to the former which is equifibered on restriction to the parallel pairs. Hence by descent, the whole diagrams are also equifibered, so $\mathbb{Z}$ is the pullback of $1\to S^1$ along $1\to S^1$, i.e. $\Omega S^1$.