Egbert Rijke
|
55b831d713
|
Merge branch 'master' of https://github.com/cmu-phil/Spectral
|
2017-06-28 17:53:22 +01:00 |
|
Egbert Rijke
|
d3f42e5a3c
|
starting to think about equivalences of prespectra
|
2017-06-28 17:53:09 +01:00 |
|
Ulrik Buchholtz
|
9934c9c73d
|
trivial homotopy groups of truncated spectra
|
2017-06-28 17:19:23 +01:00 |
|
Egbert Rijke
|
2092e4a83b
|
resolve merge conflict
|
2017-06-28 15:53:27 +01:00 |
|
Egbert Rijke
|
f4e74687f9
|
conjecture about prespectrification
|
2017-06-28 15:49:46 +01:00 |
|
Ulrik Buchholtz
|
1c07806726
|
work on strunc
|
2017-06-28 15:22:45 +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
|
635b10821f
|
temporarily disable proof, which caused error after redefinition of phomotopy
|
2017-06-28 11:08:41 +01:00 |
|
Floris van Doorn
|
cfdfa0f22a
|
Work on the fact that pointed dependent products preserve fibration sequences
We now define pointed homotopies as dependent pointed maps, and have some properties about pointed sigmas
|
2017-06-19 02:03:54 -04:00 |
|
Floris van Doorn
|
a2c4e0858d
|
clean up computation of fiber of postnikov tower
|
2017-06-15 17:49:48 -04:00 |
|
Floris van Doorn
|
0885a7ef4a
|
renamed pequiv.MK2 to pequiv.MK
|
2017-06-14 22:56:03 -04:00 |
|
Floris van Doorn
|
b6fa4e8716
|
compute fibers of postnikov tower
|
2017-06-14 22:56:03 -04:00 |
|
Floris van Doorn
|
b8de7ffd80
|
work on functorial action of prespectrum homotopy groups
|
2017-06-09 17:42:10 -04:00 |
|
|
|
d057ddec51
|
Add Hpwedge.
|
2017-06-09 15:01:21 -06:00 |
|
Robert Rose
|
9cfc13d4cf
|
naturality for wedge elimination
|
2017-06-09 16:51:13 -04:00 |
|
Yuri Sulyma
|
c8043a6f9f
|
Merge branch 'master' of github.com:fpvandoorn/Spectral
|
2017-06-09 12:24:58 -06:00 |
|
Yuri Sulyma
|
39883fd3ee
|
A bit of code for incoherent homotopies between maps of spectra
|
2017-06-09 12:24:33 -06:00 |
|
|
|
0acc5c786d
|
Add fwedge_down_left.
|
2017-06-09 11:55:59 -06:00 |
|
spiceghello
|
2e55a4a4ef
|
fwedge_prespectrum
|
2017-06-09 11:51:04 -06:00 |
|
|
|
88dc53d113
|
Add the missing 'p'.
|
2017-06-09 11:22:52 -06:00 |
|
Floris van Doorn
|
61e3a9ce0e
|
redefine homology to use smash with prespectra
|
2017-06-09 12:25:21 -04:00 |
|
|
|
f098063d96
|
More lemmas about fwedge.
|
2017-06-09 06:35:56 -06:00 |
|
Yuri Sulyma
|
5826288a48
|
composition/inverse for homotopies of pointed spaces and spectra
|
2017-06-08 20:07:46 -06:00 |
|
Yuri Sulyma
|
cf3dec8fb9
|
Merge branch 'master' of github.com:fpvandoorn/Spectral
|
2017-06-08 20:01:47 -06:00 |
|
Yuri Sulyma
|
aa54adf770
|
Use psquare/phsquare in spectrum
|
2017-06-08 20:01:41 -06:00 |
|
spiceghello
|
b2ab29c3c3
|
on colim.elim o pinclusion, and corollary on spectra
|
2017-06-08 18:28:25 -06:00 |
|
Floris van Doorn
|
e4168439c0
|
work on homotopy group of prespectrum
|
2017-06-08 20:09:48 -04:00 |
|
|
|
4165f9a613
|
Add pwedge_pequiv and plift_pwedge.
|
2017-06-08 16:44:02 -06:00 |
|
spiceghello
|
a06ecd4523
|
part of spectrify_elim
|
2017-06-08 15:08:22 -06:00 |
|
Yuri Sulyma
|
3fd6e8e852
|
Merge branch 'master' of github.com:fpvandoorn/Spectral
|
2017-06-08 14:04:58 -06:00 |
|
Yuri Sulyma
|
7f637206a0
|
Add a few spectrification things
|
2017-06-08 14:03:10 -06:00 |
|
Yuri Sulyma
|
ec852ca73f
|
Merge branch 'master' of github.com:fpvandoorn/Spectral
|
2017-06-07 09:39:46 -06:00 |
|
Yuri Sulyma
|
abe46fd211
|
Functoriality of smashing a pointed space with a prespectrum
|
2017-06-07 09:39:26 -06:00 |
|
Floris van Doorn
|
3881982774
|
small changes to spectrum
|
2017-06-07 00:54:52 -04:00 |
|
Floris van Doorn
|
5e4c536d27
|
progress on spectrify
|
2017-06-06 17:07:22 -04:00 |
|
Yuri Sulyma
|
7125413a9a
|
Renamed homology file + fixed a superfluous hypothesis in spectrify_map
|
2017-06-06 12:08:37 -06:00 |
|
|
|
76a0f5a683
|
Add plift_psusp.
|
2017-06-06 11:55:21 -06:00 |
|
Floris van Doorn
|
aef91cd344
|
fix error when compiling
|
2017-06-06 13:26:30 -04:00 |
|
Yuri Sulyma
|
3f62c7b500
|
Define a homology theory in hlean
|
2017-06-06 10:26:35 -06:00 |
|
Floris van Doorn
|
dc2c697885
|
fix error
|
2017-06-06 12:00:08 -04:00 |
|
spiceghello
|
56f7ea093e
|
smash_prespectrum
|
2017-06-06 09:41:51 -06:00 |
|
Floris van Doorn
|
6ded2b94d7
|
give type to (pre)spectrum.mk
|
2017-06-06 00:43:11 -04:00 |
|
Floris van Doorn
|
6e6fad5cb2
|
fix error
|
2017-06-05 17:09:48 -04: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
|
c7fb842124
|
checkpoint EM
|
2017-06-01 10:57:15 -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
|
9ad673682d
|
add stuff about Postnikov towers, EM-spaces and components
|
2017-05-26 05:17:02 -04:00 |
|
Floris van Doorn
|
6fbbc051e2
|
postnikov tower WIP
|
2017-05-25 22:51:11 -04:00 |
|
Floris van Doorn
|
a7b746c813
|
define parametrized cohomology
|
2017-05-24 08:27:06 -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 |
|
