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

Commit graph

  • 61c9f175d3 Add HH_base_indep. favonia 2017-06-06 14:29:41 -0600
  • e2a12f7db7 Make A in isomorphism_ap implicit. favonia 2017-06-06 12:34:13 -0600
  • d014e50cd7 Add isomorphism_ap. favonia 2017-06-06 12:33:22 -0600
  • 7125413a9a Renamed homology file + fixed a superfluous hypothesis in spectrify_map Yuri Sulyma 2017-06-06 12:08:37 -0600
  • 76a0f5a683 Add plift_psusp. favonia 2017-06-06 11:54:42 -0600
  • aef91cd344 fix error when compiling Floris van Doorn 2017-06-06 13:26:18 -0400
  • dcf0327e98 Skeleton of homology groups of spheres. favonia 2017-06-06 11:17:11 -0600
  • 3f62c7b500 Define a homology theory in hlean Yuri Sulyma 2017-06-06 10:22:11 -0600
  • dc2c697885 fix error Floris van Doorn 2017-06-06 12:00:08 -0400
  • 56f7ea093e smash_prespectrum spiceghello 2017-06-06 09:38:08 -0600
  • 6ded2b94d7 give type to (pre)spectrum.mk Floris van Doorn 2017-06-06 00:43:11 -0400
  • 6e6fad5cb2 fix error Floris van Doorn 2017-06-05 17:09:48 -0400
  • 38bff9ddb4 very small additions new_lean Steve Awodey 2017-06-01 18:01:52 -0400
  • ed7de51d02 move basic lemmas from the spectral repository to the main repository Floris van Doorn 2017-06-02 12:15:31 -0400
  • c7fb842124 checkpoint EM Floris van Doorn 2017-05-29 10:36:34 -0400
  • 9a3eed11bb move some stuff to more appropriate places (before big move to HoTT library) Floris van Doorn 2017-05-26 17:32:42 -0400
  • 9ad673682d add stuff about Postnikov towers, EM-spaces and components Floris van Doorn 2017-05-26 05:17:02 -0400
  • 6fbbc051e2 postnikov tower WIP Floris van Doorn 2017-05-25 22:51:11 -0400
  • fcbdb472c8 todo file Floris van Doorn 2017-05-25 13:46:35 -0400
  • d9c24316d8 add serre Floris van Doorn 2017-05-25 13:46:23 -0400
  • a7b746c813 define parametrized cohomology Floris van Doorn 2017-05-24 08:25:58 -0400
  • bdf0d1bb0e small cleanup on modules Floris van Doorn 2017-05-23 00:32:03 -0400
  • 798a57e546 construct the derived couple for graded modules Floris van Doorn 2017-05-22 21:27:34 -0400
  • 73a34e9edf finish construction of exact couple from a sequence of spectrum maps Floris van Doorn 2017-05-21 00:39:30 -0400
  • b953850362 define Z-modules from abelian groups Floris van Doorn 2017-05-19 14:55:13 -0400
  • 61ad085373 construct bounded exact couple from sequence of spectrum maps (there are still some holes in the proof) Floris van Doorn 2017-05-18 20:40:20 -0400
  • 2c2fefd644 continue on exact couples, simplify definition of bounded exact couple Floris van Doorn 2017-05-18 18:35:57 -0400
  • cea1250ca6 Work on the construction of exact couples Floris van Doorn 2017-05-11 17:17:50 -0400
  • 7ee38d255c left square Steve Awodey 2017-05-18 17:54:13 -0400
  • c28c078f1c Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-05-18 17:37:40 -0400
  • c42c49415e image_homomorphism_square Egbert Rijke 2017-05-18 17:37:28 -0400
  • 59cf3c6737 couple Steve Awodey 2017-05-18 17:24:36 -0400
  • f35158874a Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-05-18 17:24:14 -0400
  • 153e48d6e5 ab_image_homomorphism Egbert Rijke 2017-05-18 17:24:02 -0400
  • 502cae8088 exact couple small change Steve Awodey 2017-05-18 16:45:28 -0400
  • 8382043184 ab_subgroup_iso Egbert Rijke 2017-05-18 16:44:42 -0400
  • eaf7290def some stuff about exact couples Egbert Rijke 2017-05-11 17:25:02 -0400
  • 922baa9975 wip Steve Awodey 2017-05-11 17:14:28 -0400
  • 0b1d4428b3 exact_couple Steve Awodey 2017-05-11 15:09:24 -0400
  • de08cf57d1 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-05-11 15:06:44 -0400
  • 010e0e430b triangle commutes Egbert Rijke 2017-05-11 15:06:18 -0400
  • 1524233fec ses Steve Awodey 2017-05-11 15:00:48 -0400
  • 760af1af79 equality and isomorphisms of quotient groups Egbert Rijke 2017-05-11 15:00:30 -0400
  • c67fd11633 getting close in exact couple Steve Awodey 2017-05-04 17:46:43 -0400
  • ed00db374b Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-05-04 17:45:28 -0400
  • 3ac3146c24 extensionally equal subgroups give equal quotient groups Egbert Rijke 2017-05-04 17:45:04 -0400
  • a5a174ef0c prove convergence theorem, assuming we can derive an exact couple Floris van Doorn 2017-05-03 23:40:27 -0400
  • daedc1dc48 continue convergence theorem Floris van Doorn 2017-04-27 19:04:30 -0400
  • 43f9edf82b start on convergence theorem Floris van Doorn 2017-04-25 18:26:59 -0400
  • 1b4c40413e work on graded modules Floris van Doorn 2017-04-24 13:33:48 -0400
  • a7ec040f57 work on degrees Ulrik Buchholtz 2017-04-28 11:26:17 +0200
  • cb45181a13 remove unused definition from realprojective Ulrik Buchholtz 2017-04-28 11:25:52 +0200
  • 454401fdea Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-04-27 18:08:25 -0400
  • 44d32281fb trying to show that quotient groups of logically equivalent subgroups are isomorphic Egbert Rijke 2017-04-27 18:07:58 -0400
  • cefdc8f4e7 exact couple still Steve Awodey 2017-04-27 18:07:30 -0400
  • 6e13cb9dad small changes Steve Awodey 2017-04-27 17:09:20 -0400
  • 987f9f41ed finish definition of j' Floris van Doorn 2017-04-21 18:00:27 -0400
  • e87cbbce9e small changes in notes on smash Floris van Doorn 2017-04-21 17:36:41 -0400
  • bb209af2e8 continue with derived couple of graded R-modules, almost finish defining the maps Floris van Doorn 2017-04-20 22:58:19 -0400
  • c313d33b03 working on it Steve Awodey 2017-04-20 16:18:18 -0400
  • fd5d774e55 is_embedding_ab_subgroup_of_subgroup_incl Egbert Rijke 2017-04-20 15:45:00 -0400
  • 07d775563b ab_subgroup_of_subgroup_incl Egbert Rijke 2017-04-20 14:59:55 -0400
  • ec376b407e move stuff about subgroups to subgroup Floris van Doorn 2017-04-20 14:42:29 -0400
  • 89d9bd10b6 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-04-20 14:30:34 -0400
  • 05c5952526 changes Egbert Rijke 2017-04-20 14:30:29 -0400
  • aefc8eccc1 define submodules, quotient modules and homology of module morphisms Floris van Doorn 2017-04-13 20:39:04 -0400
  • 93126a9c2b checkpoint, submodules Floris van Doorn 2017-04-13 14:54:48 -0400
  • d828120216 checkpoint, additive homs Floris van Doorn 2017-04-07 15:56:37 -0400
  • c06793b018 add lessons file Floris van Doorn 2017-04-10 20:34:04 -0400
  • 5bb2c7859d checkpoint for direct sum of graded modules Floris van Doorn 2017-03-31 18:21:02 -0400
  • 200885ad21 started on derived couple Steve Awodey 2017-04-07 15:05:10 -0400
  • f76e665dd3 resolve merge conflict Egbert Rijke 2017-04-07 13:25:54 -0400
  • 024f8f740e stuff Egbert Rijke 2017-04-07 13:14:51 -0400
  • e4f4536080 add logic and some facts about sets Jeremy Avigad 2017-03-31 16:36:35 -0400
  • ae5399b820 add set Jeremy Avigad 2017-03-31 14:31:56 -0400
  • dc2b905a7c rename module to left_module Floris van Doorn 2017-03-30 18:33:33 -0400
  • 20a044b2e4 finish categorical structure of graded modules Floris van Doorn 2017-03-30 18:27:09 -0400
  • f96c92b72d start on graded R-modules Floris van Doorn 2017-03-30 15:02:24 -0400
  • 27bd4bc72a add file where we keep track of bugs and other undesirable behavior of Lean Floris van Doorn 2017-03-30 16:59:06 -0400
  • 91931ca338 generalize is_exact Floris van Doorn 2017-03-30 15:02:14 -0400
  • 3cd846a757 checkpoint, smash susp Floris van Doorn 2017-03-28 12:07:18 -0400
  • c0d4bc2cc1 more notes Floris van Doorn 2017-03-24 09:27:16 -0400
  • 5d6598c0ae notes smash Floris van Doorn 2017-03-22 20:35:50 -0600
  • 773e9f9a2e susp and other things Floris van Doorn 2017-03-22 20:02:53 -0400
  • b61fb7e685 work on notes Floris van Doorn 2017-03-09 17:34:30 -0500
  • b781de8473 simplify smash proof Floris van Doorn 2017-03-09 16:13:24 -0500
  • 0b55cc6b7c continue notes Floris van Doorn 2017-03-09 13:38:06 -0500
  • 8b2cd9cd64 update .gitignore with LaTeX helper files Floris van Doorn 2017-03-09 12:46:17 -0500
  • 9cf51e98cd start on notes Floris van Doorn 2017-03-08 21:30:38 -0500
  • c0a301e141 fix left module namespace Jeremy Avigad 2017-03-30 15:43:54 -0400
  • 4fd9c00755 the short five lemma Jeremy Avigad 2017-03-10 11:51:37 -0500
  • 41bc4b6673 chain complexes of modules Jeremy Avigad 2017-03-10 11:51:24 -0500
  • 153c8499af add module homomorphisms and miscellany Jeremy Avigad 2017-03-10 11:50:44 -0500
  • 4c713e921d stuff Egbert Rijke 2017-03-09 16:16:43 -0500
  • b9ed007161 Remove some old files Floris van Doorn 2017-03-07 22:31:44 -0500
  • 47532e4315 Prove the naturality of the smash-pmap adjunction, and hence of the associativity of the smash product Floris van Doorn 2017-03-06 01:01:36 -0500
  • f013c631d0 Finish the naturality of the smash-pmap adjunction Floris van Doorn 2017-03-01 22:58:50 -0500
  • 013ca8d5f2 make progress on naturality of smash-pmap adjunction Floris van Doorn 2017-03-01 20:38:13 -0500
  • ad43cd56f0 Work on the cofiber sequence and basic properties of cohomology theories Floris van Doorn 2017-02-20 16:23:57 -0500
  • 661bd961e9 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-03-02 17:11:26 -0500