Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

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

    be any Grothendieck \infty-topos.

    Then if by “the circle” in H\mathbf{H} one means the image under Δ\Delta of the circle in GrpdL whe sTop\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 Grpd\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 111\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

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

    • 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 ΩS 1=\Omega S^1 = \mathbb{Z} directly and then observe that suspension is the same as smashing with S 1S^1?

    • CommentRowNumber11.
    • CommentAuthorColin Tan
    • CommentTimeJul 21st 2014

    Probably my attempt was to argue from the oo-categorial Giruad axioms. Could one prove ΩS 1\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 ΣXK(,1)X\Sigma X \simeq K({\mathbb{Z}},1) \wedge X. 2) In particular, when setting X=S 0X = S^0, this gives S 1K(,1)S^1 \simeq K(\mathbb{Z},1). Deduce the following two corollaries: A) Looping 2) gives ΩS 1\Omega S^1 \simeq {\mathbb{Z}}. B) Substituting 2) into 1) gives ΣXS 1X\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 (,1)(\infty,1)-categorical argument is to note the (homotopy) coequalizer diagrams 11S 11 \rightrightarrows 1 \to S^1 and 1\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 1S 11\to S^1 along 1S 11\to S^1, i.e. ΩS 1\Omega S^1.

  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

    diff, v24, current