Floris van Doorn
b251465e72
continue on gysin sequence
2018-11-12 13:02:20 -05:00
Floris van Doorn
da033c0f4c
work on dependent smash and cup product on EM-spaces
...
also many small fixes
2018-09-20 02:08:45 +02:00
Floris van Doorn
68345f75ce
move more and update after changes
2018-09-11 19:24:51 +02:00
Floris van Doorn
c3650048f0
fixes and additions
...
add some properties about pointed maps and groups
2018-09-10 18:04:28 +02:00
Floris van Doorn
e4db64ae9a
fixes after changes in the library
2018-09-10 18:04:28 +02:00
Floris van Doorn
d2c7eb2368
generalize the spectral sequence of a sequence of spectrum maps
2018-09-07 11:55:24 +02:00
Floris van Doorn
fffc3cd03a
fix after moving stuff to library
...
also cleanup spectrum.basic a little
2018-09-05 22:56:40 +02:00
Floris van Doorn
9b624edb9f
fix indexing for homotopy group of presprectrum
2018-03-24 17:08:41 -04:00
Floris van Doorn
743985e3d8
Work on pointed naturality of smash-C
2018-01-17 19:17:05 -05:00
Floris van Doorn
cca1279f45
remove colim file from Spectral
2017-11-22 16:30:58 -05:00
Floris van Doorn
12a9345df1
Restructure spectral sequences, compute cohomology of projective space
...
This is still work in progress. Spectral sequences should be more usable, and probably the degrees of graded maps should be group homomorphisms so that we can reindex spectral sequences.
2017-11-22 16:14:07 -05:00
Floris van Doorn
9a693f1ee3
define pmap in terms of ppi. Also move many facts about ppi to the standard library
2017-07-21 15:55:27 +01:00
Floris van Doorn
a6d621c6f3
rename ppi_gen to ppi
2017-07-20 22:04:21 +01:00
Floris van Doorn
3367c20f9d
make pointed suspension and spheres the default
...
There is one proof in realprojective which I couldn't quite fix, so for now I left a sorry
2017-07-20 18:03:13 +01:00
Floris van Doorn
5e27ef6c3e
remove incoherent homotopies, we should use families of pointed homotopies instead.
...
Also improve performance a bit
2017-07-17 16:00:16 +01:00
Floris van Doorn
ead933e0a9
move spectrum files to separate directory
2017-07-17 15:54:05 +01:00
