michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • 7e8f183133 quotient_extend_unique_SES Egbert Rijke 2017-03-02 17:11:06 -0500
  • e7c174719b fix typo Jeremy Avigad 2017-03-02 17:08:00 -0500
  • 89d65b1dca add is_short_exact.hlean Jeremy Avigad 2017-03-02 17:06:13 -0500
  • 78512444e8 prove that the cohomology of an Eilenberg-MacLane spectrum satisfies the dimension axiom Floris van Doorn 2017-02-18 19:01:24 -0500
  • 81fe7df61f fix definition of spectrum cohomology, and prove that spectrum cohomology forms a cohomology theory Floris van Doorn 2017-02-18 16:56:38 -0500
  • 3a63635fd2 WIP: coinductive colimit definition Floris van Doorn 2017-02-10 18:03:04 -0500
  • 3bd66e60a4 separate ses from exact_couple Egbert Rijke 2017-02-16 23:00:55 -0500
  • 159ea323ab SES_hom extension lemma Egbert Rijke 2017-02-16 22:26:06 -0500
  • 2aaea21e2a tiny change Steve Awodey 2017-02-16 21:10:44 -0500
  • 92a4b95302 abgrpkernelquotientstuff Steve Awodey 2017-02-10 12:07:48 -0500
  • e3f1d64330 useless commit Egbert Rijke 2017-02-08 12:26:23 -0500
  • c0b7740f13 order of arguments in group.mk has changed Floris van Doorn 2017-02-02 17:14:48 -0500
  • d6de922d1f give last step of associativity of smash Floris van Doorn 2017-01-25 12:14:47 -0500
  • 216a25af4f fix typo Floris van Doorn 2017-01-25 12:14:20 -0500
  • cde8333151 short exact sequences Egbert Rijke 2017-01-26 17:44:37 -0500
  • 2d995b0347 short exact sequences Egbert Rijke 2017-01-26 17:44:22 -0500
  • e59f0adedf Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-01-26 16:59:18 -0500
  • 010d211b96 help Steve Awodey 2017-01-26 16:59:02 -0500
  • 701c77ba6f Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-01-26 16:56:01 -0500
  • af70424d60 work on SES Egbert Rijke 2017-01-26 16:55:59 -0500
  • b4bdf3a77e image group Steve Awodey 2017-01-26 16:55:07 -0500
  • 271459d533 image of a surjection is the codomain Steve Awodey 2017-01-26 16:44:49 -0500
  • c09f568992 trivial Steve Awodey 2017-01-26 14:58:19 -0500
  • 00e01fd2a6 feat(homotopy): prove adjunction between smash product and pointed maps Floris van Doorn 2017-01-18 23:19:00 +0100
  • b2bfc978bf continue on associativity of smash, and add some properties about the wedge sum Floris van Doorn 2017-01-13 16:47:22 +0100
  • 802eec812f Prove some basic properties about the smash product, and start on its associativity Floris van Doorn 2017-01-11 15:19:36 +0100
  • b7f53b90d7 more on pushouts, interaction with sums, and induction principle for certain cofibers Floris van Doorn 2017-01-08 22:46:54 +0100
  • cb3fac2fb3 start on torus = S^1 x S^1 Floris van Doorn 2017-01-07 14:05:14 +0100
  • db72ff0a66 more pushout lemmas, continue with smash of the circle Floris van Doorn 2017-01-06 21:46:09 +0100
  • 372ca7297c finish proof that smash is the cofiber of the map from the wedge to the product Floris van Doorn 2017-01-05 20:02:41 +0100
  • 6594be4292 prove some lemmas about pushouts, and start on the formulation of the 3x3 lemma Floris van Doorn 2017-01-05 18:18:44 +0100
  • 7f6752e14f Show that the Eilenberg-MacLane-space-functor induces an equivalence of categories Floris van Doorn 2016-12-26 16:24:01 +0100
  • 43f5112c86 move realprojective over from K-Theory repo Ulrik Buchholtz 2017-01-10 10:50:24 +0100
  • c814534104 First Isomorphism Theorem for AbGroups Steve Awodey 2016-12-08 16:20:14 -0500
  • 8d586d587b finished some lemma Egbert Rijke 2016-12-08 14:16:40 -0500
  • 4ea75446ba noethers homomorphism theorem Egbert Rijke 2016-12-02 14:05:20 -0500
  • bffab663bb messy quotient groups Steve Awodey 2016-12-01 16:34:01 -0500
  • d3cba4b95d simplifty the trivial subgroup Egbert Rijke 2016-12-01 15:43:05 -0500
  • de641aac71 fix Egbert Rijke 2016-12-01 14:41:36 -0500
  • c0a6e581e6 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2016-12-01 14:39:23 -0500
  • 652ef70739 some work, I guess Egbert Rijke 2016-12-01 14:39:10 -0500
  • b08457c77f move things to the Lean library, and update after changes in the Lean library Floris van Doorn 2016-11-23 23:54:57 -0500
  • 4f1db25e16 Work on the uniqueness of Eilenberg-Maclane spaces Floris van Doorn 2016-11-17 16:21:40 -0500
  • 8e366e08c3 Finish the universal property of the direct sum Floris van Doorn 2016-11-18 15:20:22 -0500
  • c96f3d18f2 Work on the smash product Floris van Doorn 2016-11-14 18:04:41 -0500
  • 6be1b46d5e WIP first group isomorphism them Steve Awodey 2016-11-17 16:25:14 -0500
  • 9df0b25ae5 some additions to the smash product and direct sums Floris van Doorn 2016-11-14 14:44:29 -0500
  • e87c235e24 WIP on exact couple and basic group theory Steve Awodey 2016-11-10 16:49:09 -0500
  • e4c5d34d10 wip Steve Awodey 2016-11-10 16:23:07 -0500
  • f0d595205c Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2016-11-10 16:25:11 -0500
  • ec6c4d8339 image_incl_eq_one Egbert Rijke 2016-11-10 16:25:00 -0500
  • 1fcb41a4e7 wip Steve Awodey 2016-11-10 15:40:30 -0500
  • 7d6557bdc1 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2016-11-10 15:40:24 -0500
  • c7ccd0d43b comm_gq_map Egbert Rijke 2016-11-10 15:40:12 -0500
  • 25ae0e9dce truncation level of pointed maps given connectivity of domain and truncation level of codomain Ulrik Buchholtz 2016-11-06 11:01:14 +0100
  • 7ab6eafc3c image of an abelian group is abelian Egbert Rijke 2016-11-03 23:30:44 -0400
  • 699531a74c Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2016-11-03 16:42:22 -0400
  • 81e6c07f23 progress on derived exact couples Egbert Rijke 2016-11-03 16:42:12 -0400
  • 704717e9ae minor changes Floris van Doorn 2016-11-03 15:34:06 -0400
  • 627b2acfe3 finished UMP of the quotient Steve Awodey 2016-11-03 15:12:46 -0400
  • b57eadc56a image of a boundary is subgroup of the kernel Egbert Rijke 2016-10-27 15:52:47 -0400
  • 1b09aee650 initiating exact couples Egbert Rijke 2016-10-20 16:23:55 -0400
  • 29bf3bdd8e clean-up in imports/opens of the files in the algebra folder Floris van Doorn 2016-10-13 16:01:17 -0400
  • 79dea677e8 colimit, start on encode-decode proof Floris van Doorn 2016-10-12 20:07:18 -0400
  • ead2fbbd58 do the loop-susp adjunction in pointed types Floris van Doorn 2016-10-12 17:14:34 -0400
  • a31c15e384 continue on spectrification Floris van Doorn 2016-10-10 11:10:24 -0400
  • 946506af5c define smash without any 2-paths and work on smashing with the circle Floris van Doorn 2016-10-07 16:00:09 -0400
  • b3765932d9 work on spectrification Floris van Doorn 2016-10-06 19:53:44 -0400
  • 0a15d184b2 cohomology: define cohomology as abelian groups and define the functorial action Floris van Doorn 2016-09-28 10:33:21 -0400
  • 038bbb8be3 split group_constructions into several files Egbert Rijke 2016-10-13 15:04:57 -0400
  • 258671578d EM: add functorial action and equivalence of 1-Type*[0] and Group Floris van Doorn 2016-09-23 17:05:01 -0400
  • d8c694e113 update after changes in the HoTT library. Mostly some naming and notation changes Floris van Doorn 2016-09-22 16:03:08 -0400
  • a34606c64f small changes, remove old file Floris van Doorn 2016-09-17 19:11:04 -0400
  • 5fbcbfe6e8 prove that the degree of composites is the product of the degrees Floris van Doorn 2016-09-17 00:02:22 -0400
  • fb55292c34 add move_to_lib: a file where we can put theorems which should be moved to files in the HoTT library Floris van Doorn 2016-09-16 20:23:05 -0400
  • d4508eee2f start on mapping spectra Floris van Doorn 2016-09-15 21:20:16 -0400
  • 580298d2c7 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2016-09-16 02:04:08 -0400
  • 392590bec8 working with Ulrik on basic group theory Egbert Rijke 2016-09-16 02:03:58 -0400
  • 6fca83a2ed finish the construction of the LES for spectrum maps Floris van Doorn 2016-09-15 19:19:03 -0400
  • e7c3144dbd fill in sorry in spherical_fibrations Floris van Doorn 2016-09-15 18:05:58 -0400
  • 683a515178 progress on LES of spectrum maps Floris van Doorn 2016-09-15 16:24:01 -0400
  • f826a7a711 complete is_full_subgroup Ulrik Buchholtz 2016-09-15 15:06:54 -0400
  • 22d8fad087 complete is_trivial_subgroup Ulrik Buchholtz 2016-09-15 15:04:10 -0400
  • 6cec5dcdaa fix definition of homotopy group of spectrum, continue of LES of spectra Floris van Doorn 2016-09-14 18:46:53 -0400
  • 2bf316e347 add the universal property of quotient as exercises Floris van Doorn 2016-09-14 17:31:37 -0400
  • 17d76bdb31 rename group_basics to subgroup Floris van Doorn 2016-09-14 17:12:28 -0400
  • d2f95f344f some small changes, move aut to group_constructions Floris van Doorn 2016-09-14 17:11:44 -0400
  • 65e6e062be let group_constructions import group_basics Floris van Doorn 2016-09-14 17:07:09 -0400
  • 9d00ea2f6f feat(spectrum): start on the LES of homotopy groups for spectra Floris van Doorn 2016-09-09 16:45:44 -0400
  • c9af080cc2 feat(splice): prove a lemma on how to splice chain complexes together Floris van Doorn 2016-09-09 16:43:39 -0400
  • b45e20d0cc feat(cohomology): start on cohomology file Floris van Doorn 2016-09-09 16:43:09 -0400
  • aeec8cae85 full_subgroup Ulrik Buchholtz 2016-09-08 15:02:28 -0400
  • af0b342de8 group_basics fixes Ulrik Buchholtz 2016-09-08 14:58:51 -0400
  • 01f90ef944 small comment Egbert Rijke 2016-09-08 14:28:52 -0400
  • b1dfa3ad7b defined the full subgoup in group_basic.hlean Egbert Rijke 2016-09-08 14:27:51 -0400
  • b470ea7dcd definition of trivial group in group_basic.hlean Egbert Rijke 2016-09-08 14:00:23 -0400
  • 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 Egbert Rijke 2016-09-08 11:32:36 -0400
  • ff99c2113a kernels were already defined later. I moved them Egbert Rijke 2016-09-07 23:05:49 -0400
  • 9f4436d505 some comments on the file on group_constructions Egbert Rijke 2016-09-07 22:43:50 -0400
  • 2b96a317b4 added SStodo9_2016 Steve Awodey 2016-09-01 15:40:11 -0400