Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 2nd 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded to [[circle]] the (a) definition as a homotopy type and formalized in homotopy type theory

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

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 6th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe HoTT links at [[circle]] were very out of date, so I have updated them.

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

3. • CommentRowNumber3.
   • CommentAuthorColin Tan
   • CommentTimeJul 17th 2014
   • PermaLink
   Author: Colin Tan
   Format: TextMentioned that Daniel and Mike's paper in fact proves that the loop space of the circle is the free group on one generator.

   Mentioned that Daniel and Mike's paper in fact proves that the loop space of the circle is the free group on one generator.
4. • CommentRowNumber4.
   • CommentAuthorColin Tan
   • CommentTimeJul 17th 2014
   • PermaLink
   Author: Colin Tan
   Format: TextIs 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.

   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.
5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJul 17th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexLet $$ \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](http://ncatlab.org/nlab/show/natural+numbers+object#ExamplesInASheafTopos)).

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

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJul 17th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexNote 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorColin Tan
   • CommentTimeJul 19th 2014
   • (edited Jul 19th 2014)
   • PermaLink
   Author: Colin Tan
   Format: TextI'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.

   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.
8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJul 19th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexjust to provide the link, for definiteness: your addition is [this here](http://ncatlab.org/nlab/show/diff/circle#properties)

   just to provide the link, for definiteness: your addition is this here

9. • CommentRowNumber9.
   • CommentAuthorColin Tan
   • CommentTimeJul 20th 2014
   • PermaLink
   Author: Colin Tan
   Format: MarkdownItexWrote up a proof sketch at [suspension object](http://ncatlab.org/nlab/show/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](http://ncatlab.org/nlab/show/circle) and replaced it by appealing to this general result in the particular case when X is the two-point space.

   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.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJul 21st 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThat 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$?

    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$?

11. • CommentRowNumber11.
    • CommentAuthorColin Tan
    • CommentTimeJul 21st 2014
    • PermaLink
    Author: Colin Tan
    Format: MarkdownItexProbably my attempt was to argue from the oo-categorial Giruad axioms. Could one prove $\Omega S^1 \simeq {\mathbb{Z}}$ directly from these axioms?

    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?

12. • CommentRowNumber12.
    • CommentAuthorColin Tan
    • CommentTimeJul 21st 2014
    • (edited Jul 21st 2014)
    • PermaLink
    Author: Colin Tan
    Format: MarkdownItexOn 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.

    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.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJul 22nd 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexPerhaps 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$.

    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$.

14. • CommentRowNumber14.
    • CommentAuthornLab edit announcer
    • CommentTimeDec 10th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded a paragraph in "as a topological space" section on how in constructive mathematics there are multiple definitions of real numbers and thus complex numbers, and the two definitions cannot be proven to be the same if the real numbers are not sequentially Cauchy complete. Anonymous <a href="https://ncatlab.org/nlab/revision/diff/circle/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/circle/24">v24</a>, <a href="https://ncatlab.org/nlab/show/circle">current</a>

    added a paragraph in “as a topological space” section on how in constructive mathematics there are multiple definitions of real numbers and thus complex numbers, and the two definitions cannot be proven to be the same if the real numbers are not sequentially Cauchy complete.

    Anonymous

    diff, v24, current