Floris van Doorn
ea402f56ea
finish first part of constructing gysin sequence
...
We have a long exact sequence, we still need to show that it consists of the correct groups
2018-11-12 18:07:05 -05:00
Floris van Doorn
b251465e72
continue on gysin sequence
2018-11-12 13:02:20 -05:00
Floris van Doorn
4d3053daff
Change the definition of graded morphisms
...
Now we require them to be automorphisms which are equal to \g, g + d(0)
2018-09-26 13:12:24 +02:00
Floris van Doorn
e4db64ae9a
fixes after changes in the library
2018-09-10 18:04:28 +02: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
Jeremy Avigad
6e2d8807f4
get everything to compile
2017-08-21 17:05:59 -04:00
Floris van Doorn
da95ea0acb
remove uses of homomorphism_comp_compute
...
making group_fun an abbreviation makes this obsolete
2017-06-14 22:56:03 -04:00
Floris van Doorn
f93fc153d4
fix explicit arguments of dirsum_functor_homotopy
2017-06-09 14:29:08 -04:00
Floris van Doorn
18ee7ce410
redefine direct_sum to use multiplicative groups
2017-06-07 01:01:19 -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
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
Floris van Doorn
a5a174ef0c
prove convergence theorem, assuming we can derive an exact couple
2017-05-03 23:41:25 -04:00
Floris van Doorn
daedc1dc48
continue convergence theorem
2017-05-03 23:41:24 -04:00
Floris van Doorn
43f9edf82b
start on convergence theorem
2017-05-03 23:41:19 -04:00
Floris van Doorn
1b4c40413e
work on graded modules
2017-05-03 23:40:54 -04:00
Floris van Doorn
987f9f41ed
finish definition of j'
2017-04-21 18:00:27 -04:00
Floris van Doorn
bb209af2e8
continue with derived couple of graded R-modules, almost finish defining the maps
2017-04-20 22:58:33 -04:00
Floris van Doorn
ec376b407e
move stuff about subgroups to subgroup
2017-04-20 14:42:54 -04:00
Floris van Doorn
aefc8eccc1
define submodules, quotient modules and homology of module morphisms
2017-04-13 20:39:04 -04:00
Floris van Doorn
93126a9c2b
checkpoint, submodules
2017-04-13 14:54:48 -04:00
Floris van Doorn
5bb2c7859d
checkpoint for direct sum of graded modules
2017-04-10 20:34:49 -04:00
Floris van Doorn
dc2b905a7c
rename module to left_module
2017-03-30 18:33:33 -04:00
Floris van Doorn
20a044b2e4
finish categorical structure of graded modules
2017-03-30 18:27:09 -04:00
Floris van Doorn
f96c92b72d
start on graded R-modules
2017-03-30 17:05:32 -04:00
Egbert Rijke
960e7075bd
initiating graded.hlean
2016-03-24 14:24:47 -04:00
