Commit graph

180 commits

Author SHA1 Message Date
Egbert Rijke
81e6c07f23 progress on derived exact couples 2016-11-03 16:42:12 -04:00
Floris van Doorn
704717e9ae minor changes 2016-11-03 15:34:06 -04:00
Steve Awodey
627b2acfe3 finished UMP of the quotient 2016-11-03 15:12:53 -04:00
Egbert Rijke
b57eadc56a image of a boundary is subgroup of the kernel 2016-10-27 15:52:47 -04:00
Egbert Rijke
1b09aee650 initiating exact couples 2016-10-20 16:23:55 -04:00
Floris van Doorn
29bf3bdd8e clean-up in imports/opens of the files in the algebra folder 2016-10-13 16:02:04 -04:00
Floris van Doorn
0a15d184b2 cohomology: define cohomology as abelian groups and define the functorial action 2016-10-13 15:49:17 -04:00
Egbert Rijke
038bbb8be3 split group_constructions into several files 2016-10-13 15:04:57 -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
Egbert Rijke
580298d2c7 Merge branch 'master' of https://github.com/cmu-phil/Spectral 2016-09-16 02:04:08 -04:00
Egbert Rijke
392590bec8 working with Ulrik on basic group theory 2016-09-16 02:03:58 -04:00
Floris van Doorn
683a515178 progress on LES of spectrum maps 2016-09-15 17:57:33 -04:00
Ulrik Buchholtz
f826a7a711 complete is_full_subgroup 2016-09-15 15:06:54 -04:00
Ulrik Buchholtz
22d8fad087 complete is_trivial_subgroup 2016-09-15 15:04:20 -04:00
Floris van Doorn
2bf316e347 add the universal property of quotient as exercises 2016-09-14 17:31:52 -04:00
Floris van Doorn
17d76bdb31 rename group_basics to subgroup 2016-09-14 17:31:52 -04:00
Floris van Doorn
d2f95f344f some small changes, move aut to group_constructions 2016-09-14 17:11:44 -04:00
Floris van Doorn
65e6e062be let group_constructions import group_basics 2016-09-14 17:07:09 -04:00
Ulrik Buchholtz
aeec8cae85 full_subgroup 2016-09-08 15:02:28 -04:00
Ulrik Buchholtz
af0b342de8 group_basics fixes 2016-09-08 14:58:51 -04:00
Egbert Rijke
01f90ef944 small comment 2016-09-08 14:28:52 -04:00
Egbert Rijke
b1dfa3ad7b defined the full subgoup in group_basic.hlean 2016-09-08 14:27:51 -04:00
Egbert Rijke
b470ea7dcd definition of trivial group in group_basic.hlean 2016-09-08 14:00:23 -04:00
Egbert Rijke
d9648cd2b7 trying to split the file of group constructions into a part that's not about any constructions, and a part that is. The file became huge 2016-09-08 11:32:36 -04:00
Egbert Rijke
ff99c2113a kernels were already defined later. I moved them 2016-09-07 23:05:49 -04:00
Egbert Rijke
9f4436d505 some comments on the file on group_constructions 2016-09-07 22:43:50 -04:00
Egbert Rijke
4524af4ddc image of homomorphism is subgroup 2016-05-12 16:57:33 -04:00
Floris van Doorn
ba7b25d00f move files to the HoTT library and update after changes in the HoTT library 2016-04-25 19:51:17 -04:00
Egbert Rijke
960e7075bd initiating graded.hlean 2016-03-24 14:24:47 -04:00
Egbert Rijke
0b1fbbe3e1 initiating algebra folder 2016-03-24 14:19:06 -04:00