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
|
a7b746c813
|
define parametrized cohomology
|
2017-05-24 08:27:06 -04:00 |
|
Floris van Doorn
|
91931ca338
|
generalize is_exact
|
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
|
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
|
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
|
b08457c77f
|
move things to the Lean library, and update after changes in the Lean library
|
2016-11-24 00:11:55 -05:00 |
|
Floris van Doorn
|
4f1db25e16
|
Work on the uniqueness of Eilenberg-Maclane spaces
|
2016-11-23 23:54:32 -05:00 |
|
Floris van Doorn
|
0a15d184b2
|
cohomology: define cohomology as abelian groups and define the functorial action
|
2016-10-13 15:49:17 -04:00 |
|
Floris van Doorn
|
d8c694e113
|
update after changes in the HoTT library. Mostly some naming and notation changes
|
2016-09-23 17:16:25 -04:00 |
|
Floris van Doorn
|
b45e20d0cc
|
feat(cohomology): start on cohomology file
|
2016-09-09 16:43:09 -04:00 |
|