Floris van Doorn
63ec1b8d37
progress on atiyah-hirzebruch and serre spectral sequences
...
Note: the Serre spectral sequence only works for unreduced cohomology, so we need some results for that
For reduced homology we might get a similar result if we replace the sigma in the RHS by a dependent version of the smash product
2017-07-02 01:14:18 +01:00
Floris van Doorn
f54011335d
define atiyah-hirzebruch exact couple
...
this commit also defines str and strunc_elim
proving that the exact couple is bounded, and that it converges to the right this is still todo
2017-07-01 20:02:31 +01:00
Floris van Doorn
4ba4929cd7
simplify definition of loop_ptrunc_maxm2_pequiv
2017-06-30 15:29:52 +01:00
Floris van Doorn
dce2832ead
redefine maxm2 in strunc
2017-06-30 15:16:53 +01:00
Floris van Doorn
057980ca1f
start on postnikov tower of spectra
2017-06-30 15:16:38 +01:00
Floris van Doorn
d814c472ab
add strunc file for truncatedness/truncations of spectra
2017-06-28 13:15:49 +01:00
Floris van Doorn
b8de7ffd80
work on functorial action of prespectrum homotopy groups
2017-06-09 17:42:10 -04:00
spiceghello
a06ecd4523
part of spectrify_elim
2017-06-08 15:08:22 -06:00
spiceghello
db6fccc971
pmap_eta
2017-06-08 15:08:22 -06:00
Floris van Doorn
ed7de51d02
move basic lemmas from the spectral repository to the main repository
2017-06-02 12:15:31 -04:00
Floris van Doorn
9a3eed11bb
move some stuff to more appropriate places (before big move to HoTT library)
2017-05-26 17:32:42 -04:00
Floris van Doorn
73a34e9edf
finish construction of exact couple from a sequence of spectrum maps
2017-05-21 00:39:53 -04:00
Floris van Doorn
91931ca338
generalize is_exact
2017-03-30 17:05:32 -04:00
Floris van Doorn
3cd846a757
checkpoint, smash susp
2017-03-30 17:05:32 -04:00
Floris van Doorn
773e9f9a2e
susp and other things
2017-03-30 17:00:15 -04:00
Floris van Doorn
b781de8473
simplify smash proof
2017-03-30 17:00:15 -04:00
Floris van Doorn
9cf51e98cd
start on notes
2017-03-30 17:00:15 -04:00
Floris van Doorn
47532e4315
Prove the naturality of the smash-pmap adjunction, and hence of the associativity of the smash product
2017-03-07 22:40:24 -05:00
