After that, it was only homological algebra of abelian groups, which was fully constructive, and hence formalizable using sets in homotopy type theory, with higher inductive types for quotients and images. The only homotopical input required was the long exact sequences of homotopy groups associated to the iterated fibration sequence, which as we’ve seen applies just as well to spectra as to types. (There are fancier sorts of convergence that apply to more general situations, but I don’t want to get into that right now.) One writes this as In which the terms occurring are precisely the nonzero ones on the diagonal of the page. for it becomes ) and eventually becomes zero at each homotopy group separately as, then this spectral sequence “converges” to the homotopy groups of Y, in the sense that for each n we have a finite iterated extension Moreover, if the iterated fibration sequence stabilizes as (i.e. Now in part one, I explained how from an iterated fibration sequence Which is infinite in both directions, with all entries being abelian groups. Moreover, the long exact sequences of homotopy groups for the fiber sequences splice together into a long exact sequence It’s easy to see that this inherits a spectrum structure. Similarly, the fiber of such a map is defined levelwise, with. A map of spectra is, of course, a fiberwise pointed map such that the evident squares commute relating it to the equivalences and. In general, we can “do homotopy theory” with spectra just as we can with types. Again, the definition of a spectrum makes this independent of k. Where is the mapping spectrum defined by, and the homotopy groups of a spectrum Z are defined byįor any and any k sufficiently large that. Last time I defined the cohomology of a type X with coefficients in a spectrum Y to beįor k sufficiently large that. A version that includes the intended math displays can be found here.)įirst recall that a spectrum is a family of pointed types such that for all n. (Note: the quicklatex images originally included in this post are now broken. The first part, in which I attempted to motivate the notion of spectral sequence, and constructed the basic example that we’ll be using, is at the n-Category Cafe here. This is the second part of a two-part blog post. Last time we defined cohomology in homotopy type theory in this post I want to construct the cohomological Serre spectral sequence of a fibration (i.e.
0 Comments
Leave a Reply. |