|
|
52b8fee078
|
Clean up homotopy.hlean a little bit.
|
2017-06-06 16:58:34 -06:00 |
|
|
|
7940bf0cd6
|
Add pmap.eta.
|
2017-06-06 16:58:34 -06:00 |
|
Floris van Doorn
|
5e4c536d27
|
progress on spectrify
|
2017-06-06 17:07:22 -04:00 |
|
|
|
61c9f175d3
|
Add HH_base_indep.
|
2017-06-06 14:29:41 -06:00 |
|
|
|
e2a12f7db7
|
Make A in isomorphism_ap implicit.
|
2017-06-06 12:34:13 -06:00 |
|
|
|
d014e50cd7
|
Add isomorphism_ap.
|
2017-06-06 12:33:22 -06: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 |
|
|
|
dcf0327e98
|
Skeleton of homology groups of spheres.
|
2017-06-06 11:17:11 -06: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 |
|
Steve Awodey
|
38bff9ddb4
|
very small additions
|
2017-06-02 12:16:07 -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
|
fcbdb472c8
|
todo file
|
2017-05-25 13:46:48 -04:00 |
|
Floris van Doorn
|
d9c24316d8
|
add serre
|
2017-05-25 13:46:48 -04:00 |
|
Floris van Doorn
|
a7b746c813
|
define parametrized cohomology
|
2017-05-24 08:27:06 -04:00 |
|
Floris van Doorn
|
bdf0d1bb0e
|
small cleanup on modules
|
2017-05-24 08:26:50 -04:00 |
|
Floris van Doorn
|
798a57e546
|
construct the derived couple for graded modules
|
2017-05-22 21:27:34 -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
|
b953850362
|
define Z-modules from abelian groups
|
2017-05-21 00:39:53 -04:00 |
|
Floris van Doorn
|
61ad085373
|
construct bounded exact couple from sequence of spectrum maps (there are still some holes in the proof)
|
2017-05-21 00:39:53 -04:00 |
|
Floris van Doorn
|
2c2fefd644
|
continue on exact couples, simplify definition of bounded exact couple
|
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 |
|
Steve Awodey
|
7ee38d255c
|
left square
|
2017-05-18 17:54:13 -04:00 |
|
Egbert Rijke
|
c28c078f1c
|
Merge branch 'master' of https://github.com/cmu-phil/Spectral
|
2017-05-18 17:37:40 -04:00 |
|
Egbert Rijke
|
c42c49415e
|
image_homomorphism_square
|
2017-05-18 17:37:28 -04:00 |
|
Steve Awodey
|
59cf3c6737
|
couple
|
2017-05-18 17:24:39 -04:00 |
|
Egbert Rijke
|
f35158874a
|
Merge branch 'master' of https://github.com/cmu-phil/Spectral
|
2017-05-18 17:24:14 -04:00 |
|
Egbert Rijke
|
153e48d6e5
|
ab_image_homomorphism
|
2017-05-18 17:24:02 -04:00 |
|
Steve Awodey
|
502cae8088
|
exact couple small change
|
2017-05-18 16:45:28 -04:00 |
|
Egbert Rijke
|
8382043184
|
ab_subgroup_iso
|
2017-05-18 16:44:42 -04:00 |
|
Egbert Rijke
|
eaf7290def
|
some stuff about exact couples
|
2017-05-11 17:25:02 -04:00 |
|
Steve Awodey
|
922baa9975
|
wip
|
2017-05-11 17:14:28 -04:00 |
|
Steve Awodey
|
0b1d4428b3
|
exact_couple
|
2017-05-11 15:09:24 -04:00 |
|
Egbert Rijke
|
de08cf57d1
|
Merge branch 'master' of https://github.com/cmu-phil/Spectral
|
2017-05-11 15:06:44 -04:00 |
|
Egbert Rijke
|
010e0e430b
|
triangle commutes
|
2017-05-11 15:06:18 -04:00 |
|
Steve Awodey
|
1524233fec
|
ses
|
2017-05-11 15:01:10 -04:00 |
|
Egbert Rijke
|
760af1af79
|
equality and isomorphisms of quotient groups
|
2017-05-11 15:00:30 -04:00 |
|
Steve Awodey
|
c67fd11633
|
getting close in exact couple
|
2017-05-04 17:46:43 -04:00 |
|
Egbert Rijke
|
ed00db374b
|
Merge branch 'master' of https://github.com/cmu-phil/Spectral
|
2017-05-04 17:45:28 -04:00 |
|
Egbert Rijke
|
3ac3146c24
|
extensionally equal subgroups give equal quotient groups
|
2017-05-04 17:45:04 -04:00 |
|
Floris van Doorn
|
a5a174ef0c
|
prove convergence theorem, assuming we can derive an exact couple
|
2017-05-03 23:41:25 -04:00 |
|
