Floris van Doorn
36cce7acda
work on translation from reduced cohomology to unreduced cohomology
2017-07-04 12:57:46 +01:00
Floris van Doorn
a34a639e80
dependent spectrum over X_+
2017-07-03 13:37:02 +01:00
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
d23466396d
fix some errors
2017-07-01 20:00:40 +01:00
Egbert Rijke
9d562c1e5d
working on the left inverse of a spectral equivalence
2017-07-01 17:13:29 +01:00
Egbert Rijke
eed538eb8f
simplify shomotopy
2017-07-01 16:23:50 +01:00
Egbert Rijke
ed2ff9f113
simplify szero
2017-07-01 15:42:49 +01:00
Egbert Rijke
dd18b3a72a
squares with two constant maps
2017-07-01 15:39:25 +01:00
Egbert Rijke
4033195ce3
simplified scompose
2017-07-01 15:15:29 +01:00
Egbert Rijke
c71e275dcd
Merge branch 'master' of https://github.com/cmu-phil/Spectral
2017-07-01 14:47:17 +01:00
Egbert Rijke
958d7f72df
add ptd cubes
2017-07-01 14:47:06 +01:00
Egbert Rijke
8561c20aa6
redefine sid
2017-07-01 14:46:38 +01:00
Ulrik Buchholtz
9b895beeee
add simpler versions of is_trunc_ppi and is_strunc_spi
2017-07-01 14:26:49 +01:00
Egbert Rijke
aa1d1bd333
Merge branch 'master' of https://github.com/cmu-phil/Spectral
2017-07-01 13:06:53 +01:00
Egbert Rijke
dffe842061
working on spectral equivalences
2017-07-01 13:06:47 +01:00
Ulrik Buchholtz
3cf424ef27
add is_strunc_spi
2017-07-01 13:02:23 +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
0d48402927
add explanation of universal property of cofiber
2017-06-30 13:55:39 +01:00
Floris van Doorn
00d02ecacf
add authors of mrc projects to files with major contributions
2017-06-30 13:55:39 +01:00
Ulrik Buchholtz
52dda63e4d
refactor strunc
2017-06-29 20:06:47 +01:00
Ulrik Buchholtz
79d13fd0d2
start map from spectrum to its truncation
2017-06-28 23:02:14 +01:00
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
Floris van Doorn
cea1250ca6
Work on the construction of exact couples
2017-05-21 00:39:53 -04:00
Ulrik Buchholtz
a7ec040f57
work on degrees
2017-04-29 14:05:39 +02:00
Ulrik Buchholtz
cb45181a13
remove unused definition from realprojective
2017-04-28 11:26:21 +02: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
b9ed007161
Remove some old files
2017-03-07 22:55:51 -05: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
Floris van Doorn
f013c631d0
Finish the naturality of the smash-pmap adjunction
2017-03-03 17:43:03 -05:00
Floris van Doorn
013ca8d5f2
make progress on naturality of smash-pmap adjunction
...
The only fact left to be proven is a property (which is an equality of phomotopies) of the functorial action of the smash product
2017-03-03 17:43:03 -05:00
Floris van Doorn
ad43cd56f0
Work on the cofiber sequence and basic properties of cohomology theories
2017-03-03 17:42:38 -05:00
Floris van Doorn
78512444e8
prove that the cohomology of an Eilenberg-MacLane spectrum satisfies the dimension axiom
2017-02-18 19:01:24 -05:00
Floris van Doorn
81fe7df61f
fix definition of spectrum cohomology, and prove that spectrum cohomology forms a cohomology theory
2017-02-18 16:56:50 -05:00
Floris van Doorn
c0b7740f13
order of arguments in group.mk has changed
2017-02-02 17:16:14 -05:00
Floris van Doorn
d6de922d1f
give last step of associativity of smash
...
there are still unproven lemma's
2017-02-02 17:16:01 -05:00
Floris van Doorn
216a25af4f
fix typo
2017-02-02 17:15:46 -05:00
Floris van Doorn
00e01fd2a6
feat(homotopy): prove adjunction between smash product and pointed maps
...
also develop library for equality reasoning on pointed homotopies.
Also do the renamings like homomorphism -> is_mul_hom
2017-01-18 23:19:06 +01:00
Floris van Doorn
b2bfc978bf
continue on associativity of smash, and add some properties about the wedge sum
2017-01-14 21:08:00 +01:00
Floris van Doorn
802eec812f
Prove some basic properties about the smash product, and start on its associativity
2017-01-14 21:07:36 +01:00
Floris van Doorn
b7f53b90d7
more on pushouts, interaction with sums, and induction principle for certain cofibers
...
latter part ported from Agda
2017-01-14 21:07:36 +01:00
Floris van Doorn
cb3fac2fb3
start on torus = S^1 x S^1
2017-01-14 21:07:36 +01:00
Floris van Doorn
db72ff0a66
more pushout lemmas, continue with smash of the circle
2017-01-14 21:07:36 +01:00
Floris van Doorn
372ca7297c
finish proof that smash is the cofiber of the map from the wedge to the product
2017-01-14 21:07:36 +01:00
Floris van Doorn
6594be4292
prove some lemmas about pushouts, and start on the formulation of the 3x3 lemma
2017-01-14 21:06:17 +01:00
