Processing math: 100%
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

Discussion Tag Cloud

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 2014

    I have added pointer to Mike’s discussion of spectral sequences here at “homotopy spectral sequence” and in related entries.

    But now looking at this I am unsure what the claim is: has this been formalized in HoTT?

    (Clearly a question for Mike! :-)

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    Not in the sense of being implemented in a proof assistant, no.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2014

    Okay, thanks.

    How about the long homotopy fiber sequences of homotopy groups? I hear that Voevodsky has formalized this? Is the code publically available?

    I was wondering, more specifically, what’s the status in HoTT of computing, in principle, homotopy groups of finite cell complexes (i.e. of HITs) more general than spheres.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    I’m not well-up on what Voevodsky has done, but you could look through the UniMath library that he works on.

    I don’t know of much work on finite cell complexes other than spheres; I think most everyone has considered that spheres are hard enough to start with. Except for the really easy cases like a finite wedge of circles.

    • CommentRowNumber5.
    • CommentAuthorCharles Rezk
    • CommentTimeNov 3rd 2014

    What is a “finite cell complex” in HoTT? What does “finite cell complex” correspond to in terms of an -topos model?

    • CommentRowNumber6.
    • CommentAuthorCharles Rezk
    • CommentTimeNov 3rd 2014

    I’m really asking: how do you construct the “type” of finite cell complexes in HoTT?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2014

    One definition is that a finite cell complex is a non-recursive HIT whose constructors take no inputs. That’s a meta-theoretic definition, so it doesn’t let you construct “the type of finite cell complexes”. Another definition is that a finite cell complex is an iterated pushout of maps Sn1. That can be internalized, e.g. the type of k-cell complexes is defined recursively on k where a (k+1)-cell complex is specified by choosing a k-cell complex X, a natural number n, and a map SnX.

    Either way, the finite cell complexes in an -topos model will be the tensors of 1 by ordinary finite cell complexes in Gpd, or equivalently the images of ordinary finite cell complexes under the left adjoint Δ:GpdH to the global sections functor.

    • CommentRowNumber8.
    • CommentAuthorCharles Rezk
    • CommentTimeNov 4th 2014

    I don’t think that can be right. Maps SpSq in H need not always arise from Gpd.

    For instance, consider H=Gpd/T for some space T. The internal mapping object MapT(Sk,Sn) is the projection map Map(Sk,Sn)×TT. It’s 0-truncation is (πkSn)×TT, so the “homotopy group” is what you expect. But the space of sections of MapT(Sk,Sn)T is equivalent to Map(Sk×T,Sn), so its π0 could be much bigger. (Or smaller, if T=.)

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    Oh, yes, you’re right. So there could be more finite cell complexes in some model than there are in Gpd.

    • CommentRowNumber10.
    • CommentAuthorCharles Rezk
    • CommentTimeNov 4th 2014

    I guess it’s complicated. There is a type Fin which is the recursive type you alluded to. An F:Fin knows all about its own attaching maps and stuff. This type comes with a “realization” map R:Fin𝒰 to the type of types, which you can then factor through its (1)-truncation: Fin𝒰Fin𝒰. You might think of 𝒰Fin as the type of “types having the homotopy type of a finite complex”, except that there is the odd problem that I can’t necessarily lift a map 1𝒰Fin to a map 1Fin. I would guess that in a sheaf model, 𝒰Fin corresponds to objects which are “locally” finite complexes, e.g., whose stalks are equivalent to finite complexes.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    Right, exactly. In fact Fin and R have to be defined mutually, either by mutual recursion or induction-recursion, since the type of attaching maps at stage n+1 depends on knowing the realization of stage n. Your guess about models seems plausible.