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

Commit graph

  • 9c1ffaa201 Merge branch 'master' of https://github.com/jonas-frey/Spectral Jonas Frey 2017-09-14 14:41:57 -0400
  • 8db8c18516 Merge branch 'master' of https://github.com/cmu-phil/Spectral Jonas Frey 2017-09-14 14:31:44 -0400
  • af30b19099 restore quotient_group.hlean Jeremy Avigad 2017-09-07 15:22:04 -0400
  • 7e2af3e19b some cleanup univalent_subcategory.hlean Jonas Frey 2017-09-07 00:39:50 -0400
  • f3ba645573 add file containing proof about univalent subcategories and that AbGrp is univalent Jonas Frey 2017-09-06 16:14:25 -0400
  • dc327487f6 start on higher groups file Floris van Doorn 2017-09-05 22:28:55 -0400
  • b9c2145fab add naturality of sigma's commuting with pushouts Floris van Doorn 2017-08-22 22:34:13 +0100
  • 6e2d8807f4 get everything to compile Jeremy Avigad 2017-08-21 17:05:59 -0400
  • 345c45e07c revise quotient_group Jeremy Avigad 2017-06-30 21:22:53 +0100
  • 1cb3e5c658 change terminology set -> property Jeremy Avigad 2017-06-26 17:39:40 +0100
  • c74779959a base subgroups on sets and unbundle Jeremy Avigad 2017-04-07 15:12:31 -0400
  • a001491183 various properties of pushout: commutation with sums and sigma's Floris van Doorn 2017-08-02 23:06:07 +0100
  • ee11b1cfb9 work of fiber of maps between EM-spaces Floris van Doorn 2017-07-23 14:38:59 +0100
  • d0995af5b5 fix realprojective after sphere reindexing Ulrik Buchholtz 2017-07-23 11:52:02 +0200
  • 9a693f1ee3 define pmap in terms of ppi. Also move many facts about ppi to the standard library Floris van Doorn 2017-07-21 15:55:27 +0100
  • a6d621c6f3 rename ppi_gen to ppi Floris van Doorn 2017-07-20 22:04:21 +0100
  • 23780b0425 move naturality of loop-susp-adjunction to standard library Floris van Doorn 2017-07-20 18:55:51 +0100
  • 3367c20f9d make pointed suspension and spheres the default Floris van Doorn 2017-07-20 18:01:22 +0100
  • a5c80f79c6 work a bit on Eilenberg-MacLane spaces Floris van Doorn 2017-07-17 21:56:14 +0100
  • 4d7963d226 update README. Add small projects, which anyone could work on Floris van Doorn 2017-07-17 16:09:09 +0100
  • 5e27ef6c3e remove incoherent homotopies, we should use families of pointed homotopies instead. Floris van Doorn 2017-07-17 16:00:16 +0100
  • ead933e0a9 move spectrum files to separate directory Floris van Doorn 2017-07-17 15:54:05 +0100
  • 6bbe5ef450 reorganize some files in the library. In particular, split up spectrum Floris van Doorn 2017-07-17 15:39:49 +0100
  • 2745c17498 add some info to known_bugs Floris van Doorn 2017-07-17 14:15:11 +0100
  • 1eec8e65dc merge the two lessons files Floris van Doorn 2017-07-17 14:11:21 +0100
  • 3f68115d25 move some files around, create folder cohomology Floris van Doorn 2017-07-17 13:58:36 +0100
  • e76f1db8ae update README Floris van Doorn 2017-07-16 01:16:06 +0100
  • c98c9bb1e6 proof naturality of pointed funext. This finishes the proof of the Serre Spectral Sequence. Floris van Doorn 2017-07-16 01:11:51 +0100
  • 10be0d610a work on pppi_sigma_char_natural Ulrik Buchholtz 2017-07-14 00:15:32 +0100
  • a4c4da36df shorten proof of spi_compose_left Floris van Doorn 2017-07-13 17:26:39 +0100
  • df54ac858e finish functoriality of ppi_compose_left Floris van Doorn 2017-07-13 16:19:44 +0100
  • 37d9761596 work on functoriality of ppi_compose_left Floris van Doorn 2017-07-12 10:18:07 +0100
  • 969906d480 complete psigma_gen_functor_psquare Floris van Doorn 2017-07-11 15:19:08 +0100
  • 83f7761d31 work on naturality squares Floris van Doorn 2017-07-11 14:21:05 +0100
  • 5381aaa7bd progress on the naturality of loop_pppi_pequiv Floris van Doorn 2017-07-08 22:45:18 +0100
  • 5ac3ce7058 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-08 18:20:55 +0100
  • e769f5362e lemmas in the pointed pi file Egbert Rijke 2017-07-08 18:20:43 +0100
  • 5959ccf2af comment out some print statements, fix broken definition Floris van Doorn 2017-07-08 15:49:30 +0100
  • 0f24cda263 prove the other sorry's in cohomology Floris van Doorn 2017-07-08 15:40:43 +0100
  • e6b1c49f4a moving some definitions to pointed_pi Egbert Rijke 2017-07-08 15:25:17 +0100
  • e92fb0a435 prove two of the sorry's in cohomology Floris van Doorn 2017-07-08 15:11:11 +0100
  • b027186436 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-08 14:49:40 +0100
  • 1c51df13f2 further reductions to pointed_pi Egbert Rijke 2017-07-08 14:49:32 +0100
  • eaaaa79fc7 update some headers Ulrik Buchholtz 2017-07-08 13:39:23 +0100
  • 7a5b8a206d do the integer arithmetic sorrys Ulrik Buchholtz 2017-07-08 13:26:34 +0100
  • 1abb09b062 one sorry less: parametrized_cohomology_isomorphism_shomotopy_group_spi Ulrik Buchholtz 2017-07-08 12:22:31 +0100
  • bc43e079e0 getting closer ... Ulrik Buchholtz 2017-07-08 10:39:48 +0100
  • ad8b52cd59 simplify ppi_loop_equiv Ulrik Buchholtz 2017-07-08 09:48:11 +0100
  • 9ee02cfad5 typo in README Ulrik Buchholtz 2017-07-07 23:04:39 +0100
  • bb3995c573 isomorphism of truncations of h-groups Ulrik Buchholtz 2017-07-07 23:04:27 +0100
  • b8bb1ca67d solving one subgoal, get another Egbert Rijke 2017-07-08 11:53:31 +0100
  • cce49435f6 removing errors and warnings Egbert Rijke 2017-07-08 11:43:41 +0100
  • 6378a34fa6 minor stuff Egbert Rijke 2017-07-08 11:41:57 +0100
  • d00ad36f73 minor changes Egbert Rijke 2017-07-08 02:01:28 +0100
  • 99449db85c working of the last few subgoals Egbert Rijke 2017-07-08 01:40:27 +0100
  • 9c271470ca add sorry's to make library compile Floris van Doorn 2017-07-07 22:38:06 +0100
  • 90f4acb3f6 fix definition of atiyah-hirzebruch spectral sequence, define serre spectral sequence Floris van Doorn 2017-07-07 22:32:57 +0100
  • f6978927b2 working toward associativity of the wedge Steve Awodey 2017-07-07 20:35:56 +0100
  • 39526a821c Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-07 20:12:08 +0100
  • 1e80e9f1d9 eq_of_shomotopy Egbert Rijke 2017-07-07 20:11:55 +0100
  • 877bcd889e eq_of_shomotopy Egbert Rijke 2017-07-07 20:11:47 +0100
  • e24865d48b compute fiber of postnikov_smap Floris van Doorn 2017-07-05 20:40:15 +0100
  • 9d39f7771f redefine is_trunc_ppi and is_trunc_spi with unbundled families Floris van Doorn 2017-07-05 15:42:27 +0100
  • 58b007c873 reorganizing the prespectrification section Egbert Rijke 2017-07-05 17:26:31 +0100
  • 997d75cbf3 no errors hopefully Egbert Rijke 2017-07-05 15:51:52 +0100
  • 28b4559a0f induction on ~~* Egbert Rijke 2017-07-05 14:56:03 +0100
  • 4559ee6218 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-04 21:11:32 +0100
  • 1b9990a424 still working towards isretr Egbert Rijke 2017-07-04 21:11:20 +0100
  • d33502cf5f add reference in README Floris van Doorn 2017-07-04 17:14:28 +0100
  • fa9af80739 more updates in README Floris van Doorn 2017-07-04 16:20:09 +0100
  • 73abecaa89 rename some files, update README Floris van Doorn 2017-07-04 16:11:21 +0100
  • 36cce7acda work on translation from reduced cohomology to unreduced cohomology Floris van Doorn 2017-07-04 12:57:46 +0100
  • a34a639e80 dependent spectrum over X_+ Floris van Doorn 2017-07-03 13:37:02 +0100
  • 63ec1b8d37 progress on atiyah-hirzebruch and serre spectral sequences Floris van Doorn 2017-07-02 01:14:18 +0100
  • 7b3d1649fa finish sufficient condition when infinity page of spectral sequence is contractible Floris van Doorn 2017-07-02 01:12:55 +0100
  • f54011335d define atiyah-hirzebruch exact couple Floris van Doorn 2017-07-01 20:02:31 +0100
  • d23466396d fix some errors Floris van Doorn 2017-07-01 20:00:40 +0100
  • 9d562c1e5d working on the left inverse of a spectral equivalence Egbert Rijke 2017-07-01 17:13:29 +0100
  • eed538eb8f simplify shomotopy Egbert Rijke 2017-07-01 16:23:50 +0100
  • ed2ff9f113 simplify szero Egbert Rijke 2017-07-01 15:42:49 +0100
  • dd18b3a72a squares with two constant maps Egbert Rijke 2017-07-01 15:39:25 +0100
  • 4033195ce3 simplified scompose Egbert Rijke 2017-07-01 15:15:29 +0100
  • c71e275dcd Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-01 14:47:17 +0100
  • 958d7f72df add ptd cubes Egbert Rijke 2017-07-01 14:47:06 +0100
  • 8561c20aa6 redefine sid Egbert Rijke 2017-07-01 14:46:38 +0100
  • 9b895beeee add simpler versions of is_trunc_ppi and is_strunc_spi Ulrik Buchholtz 2017-07-01 14:26:38 +0100
  • aa1d1bd333 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-07-01 13:06:53 +0100
  • dffe842061 working on spectral equivalences Egbert Rijke 2017-07-01 13:06:47 +0100
  • 3cf424ef27 add is_strunc_spi Ulrik Buchholtz 2017-07-01 13:02:23 +0100
  • 4ba4929cd7 simplify definition of loop_ptrunc_maxm2_pequiv Floris van Doorn 2017-06-30 15:29:52 +0100
  • dce2832ead redefine maxm2 in strunc Floris van Doorn 2017-06-30 15:14:55 +0100
  • 057980ca1f start on postnikov tower of spectra Floris van Doorn 2017-06-29 15:48:43 +0100
  • f8f0157df5 define ==> notation for convergence of spectral sequences Floris van Doorn 2017-06-30 13:54:23 +0100
  • 0d48402927 add explanation of universal property of cofiber Floris van Doorn 2017-06-29 15:03:23 +0100
  • 00d02ecacf add authors of mrc projects to files with major contributions Floris van Doorn 2017-06-29 14:57:11 +0100
  • bf3a132e99 fixed Steve Awodey 2017-06-30 13:21:49 +0100
  • a209f4e085 trivial Steve Awodey 2017-06-30 13:20:08 +0100
  • 52dda63e4d refactor strunc Ulrik Buchholtz 2017-06-29 20:06:47 +0100
  • 79d13fd0d2 start map from spectrum to its truncation Ulrik Buchholtz 2017-06-28 23:02:09 +0100
  • 55b831d713 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-06-28 17:53:22 +0100