Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to circle the (a) definition as a homotopy type and formalized in homotopy type theory
The HoTT links at circle were very out of date, so I have updated them.
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).
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.
just to provide the link, for definiteness: your addition is this here
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.
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$?
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?
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.
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$.
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
1 to 14 of 14