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

Commit graph

  • 78492bbe09 feat(EM): Work on uniqueness of K(G,n)'s Floris van Doorn 2016-06-28 19:52:14 +0100
  • dc2a26745e move results to HoTT library, and start on uniqueness of K(G, n) for n>1 Floris van Doorn 2016-06-24 09:49:45 +0100
  • 21c6e8f7e5 small changes after changes in HoTT library Floris van Doorn 2016-06-23 21:53:50 +0100
  • d6d08ccd83 update README Floris van Doorn 2016-06-26 09:25:50 +0100
  • 4524af4ddc image of homomorphism is subgroup Egbert Rijke 2016-05-12 16:57:33 -0400
  • 9f5d7bda9f more stuff Floris van Doorn 2016-04-26 17:33:17 -0400
  • 62c134df4e whitehead corollaries Floris van Doorn 2016-04-26 16:07:15 -0400
  • ba7b25d00f move files to the HoTT library and update after changes in the HoTT library Floris van Doorn 2016-04-25 19:51:17 -0400
  • 0af9c0ecc7 prove is_equiv_π_of_is_connected for functions where the domain and codomain live in different universes Floris van Doorn 2016-04-14 17:07:49 -0400
  • 7d7ddaff9f give the LES of a fibration sequence Floris van Doorn 2016-04-13 12:20:22 -0400
  • 2de92db5b6 some cleanup Floris van Doorn 2016-04-12 17:59:15 -0400
  • a716ef2108 applications: prove almost completely that S^3 and S^2 have the same high enough homotopy groups Floris van Doorn 2016-04-11 23:17:10 -0400
  • 9a476fecfe sec86: finish proof of stability of spheres as groups Floris van Doorn 2016-04-11 15:55:28 -0400
  • 0f9433c921 Rename some files, use the new LES file for the application file. Floris van Doorn 2016-04-07 17:28:33 -0400
  • 37fbe56b8c Finish construction of the LES of homotopy groups without signs Floris van Doorn 2016-04-07 17:28:19 -0400
  • cb40d9b8fc add some copyright notices and LICENSE file Floris van Doorn 2016-03-24 13:25:42 -0400
  • c1038a3f96 give the definition of the I-ary direct sum Floris van Doorn 2016-03-31 13:22:45 -0400
  • a6bf82618f feat(homotopy/spectrum): sections of parametrized spectra Mike Shulman 2016-03-25 09:33:36 -0700
  • af5a3091bb Merge branch 'master' of github.com:cmu-phil/Spectral Mike Shulman 2016-03-24 16:30:22 -0700
  • f8f7f69bcd Finish proof of pfiber_equiv_of_square Mike Shulman 2016-03-24 16:30:10 -0700
  • 288e0d71b2 make everything compile on lean post 6f74f6522... Ulrik Buchholtz 2016-03-24 16:14:44 -0400
  • 960e7075bd initiating graded.hlean Egbert Rijke 2016-03-24 14:24:47 -0400
  • 0b1fbbe3e1 initiating algebra folder Egbert Rijke 2016-03-24 14:19:06 -0400
  • 6807883830 port module from the standard library Floris van Doorn 2016-03-24 13:41:03 -0400
  • 5a23744094 update README to reflect recent discussion Ulrik Buchholtz 2016-03-21 14:44:57 -0400
  • 652ca1da84 working on the join theorem Egbert Rijke 2016-03-10 22:51:32 -0500
  • 9ca4a3fbb1 start spherical fibrations (NB post #1021 lean) Ulrik Buchholtz 2016-03-10 19:50:49 -0500
  • 00978587e5 update README Floris van Doorn 2016-03-06 13:23:30 -0500
  • 97d7d0c108 updates after changes in the HoTT library Floris van Doorn 2016-03-06 11:26:15 -0500
  • 0483966328 prove the Freudenthal Suspension Theorem Floris van Doorn 2016-03-03 17:24:34 -0500
  • a76e4fce08 prove that the join of two spheres is a sphere Floris van Doorn 2016-03-03 12:48:31 -0500
  • 22e75da53e chain complexes of spectra Mike Shulman 2016-03-22 09:53:16 -0700
  • 559777e45c index spectra by a general succ_str, +Z, or +N, as appropriate Mike Shulman 2016-03-22 08:10:10 -0700
  • 5379c2e253 feat(homotopy/spectrum): fibers of spectra Mike Shulman 2016-03-23 11:30:39 -0700
  • 104378f2c3 feat(homotopy/spectrum): use namespaces and better typeclasses Mike Shulman 2016-03-21 15:53:25 -0700
  • 2bb5176b97 feat(homotopy/spectrum): basic definitions and cotensors by types Mike Shulman 2016-03-20 20:16:36 -0700
  • 6d11d025dd remove namespace equiv.ops Floris van Doorn 2016-03-03 11:56:56 -0500
  • b7c4f3b6a7 use have instead of assert Floris van Doorn 2016-03-03 11:05:44 -0500
  • 1213001a6a feat(LES_applications): give most of the proof of 8.4.8 Floris van Doorn 2016-03-02 22:14:32 -0500
  • a578b1c42e Add computing version of the LES of homotopy groups. Floris van Doorn 2016-02-17 18:27:26 -0500
  • b7f2b9d689 update after renamings in the HoTT library Floris van Doorn 2016-02-17 15:36:31 -0500
  • 5c9355c4c1 feat(chain_complex): give the construction of the LES of homotopy groups Floris van Doorn 2016-02-17 15:39:37 -0500
  • efd5d25039 Merge branch 'master' of https://github.com/cmu-phil/Spectral Clive Newstead 2016-02-18 16:18:02 -0500
  • ae01bcba86 Created sec83.hlean Clive Newstead 2016-02-18 16:16:55 -0500
  • 5342e41863 Delete clive.hlean cnewstead 2016-02-18 14:04:05 -0500
  • 52f59f8592 rename long_exact_sequence to chain_complex Floris van Doorn 2016-02-09 18:27:38 -0500
  • d1619c1b53 feat(homotopy/long_exact_sequence): change to chain complexes as basic structure Floris van Doorn 2016-02-09 12:38:23 -0500
  • 8f9ef03ad2 feat(homotopy/LES): continue working on the LES of homotopy groups Floris van Doorn 2016-02-05 00:51:00 -0500
  • c926955c8b begin LESs Floris van Doorn 2016-02-04 19:02:15 -0500
  • 2f150dce1f Playing with groups Clive Newstead 2016-02-04 15:31:41 -0500
  • 103e4f72fe Learning how to Git... Clive Newstead 2016-02-04 14:02:39 -0500
  • 3a09986692 Created clive.hlean Clive Newstead 2016-02-04 14:00:48 -0500
  • 895050d155 fix(*): fix broken files Floris van Doorn 2016-02-04 13:38:33 -0500
  • 6889eba5ea added homotopy subdirectory and sample file Steve Awodey 2016-01-21 14:33:54 -0500
  • 2c97f5cef7 Merge remote-tracking branch 'origin/master' Steve Awodey 2016-01-21 14:27:14 -0500
  • 392ee8555a added HoTT Book Chapter 8 to do Steve Awodey 2016-01-21 14:25:17 -0500
  • 5f11c03d60 add rough sketch of dependency graph Ulrik Buchholtz 2016-01-21 14:18:00 -0500
  • 01e0d1897b some cleanup Floris van Doorn 2015-12-10 21:17:29 -0500
  • 3c9ca4b51c working on tensor group Floris van Doorn 2015-12-10 15:46:09 -0500
  • 492b433cc6 show that groups form a precategory (category todo) Floris van Doorn 2015-12-10 15:45:49 -0500
  • 304bcc472a homework accomplished Egbert Rijke 2015-12-10 18:37:30 -0500
  • fa25173a38 kernels Egbert Rijke 2015-12-10 16:36:10 -0500
  • f1e76aa8db Revert "There have been some changes in the algebra-part of Lean." Steve Awodey 2015-12-10 15:41:38 -0500
  • f4a8a679c6 tiny Steve Awodey 2015-12-10 15:41:24 -0500
  • c1d1a5e509 There have been some changes in the algebra-part of Lean. Floris van Doorn 2015-12-09 17:12:37 -0500
  • 633d1f6d46 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2015-12-08 16:17:55 -0500
  • 99c730b0a5 added Floris his notes Egbert Rijke 2015-12-08 16:17:38 -0500
  • af9f77b71c add Mac Lane's Homology to README.md Ulrik Buchholtz 2015-12-07 09:20:54 +0100
  • 0d4166bfbc Update README.md Egbert Rijke 2015-12-06 18:00:19 -0500
  • 80694430f9 Update README.md Egbert Rijke 2015-12-06 17:38:55 -0500
  • bc5a240a3a Update README.md Egbert Rijke 2015-12-06 13:23:49 -0500
  • 5d14d74145 Update README.md Egbert Rijke 2015-12-04 17:00:38 -0500
  • 5bc66d6d23 Update README.md Egbert Rijke 2015-12-04 16:57:32 -0500
  • 952f2742e2 Update README.md Egbert Rijke 2015-12-04 16:54:48 -0500
  • bf74676b0f Update README.md Egbert Rijke 2015-12-04 16:53:35 -0500
  • c9758ba4a2 removing K-theory part Egbert Rijke 2015-12-04 16:05:00 -0500
  • 5da0c57835 added notes Egbert Rijke 2015-12-04 16:03:04 -0500
  • 35db866a61 Update README.md with roadmap based on Mike's blog post Mike Shulman 2015-12-04 09:25:18 -0800
  • 9e7b0bfae3 Update README.md Egbert Rijke 2015-12-04 12:03:18 -0500
  • 0f762059fe Update README.md Egbert Rijke 2015-12-04 11:57:56 -0500
  • e0cc495abf Update README.md Egbert Rijke 2015-12-03 19:59:03 -0500
  • 8d9dd87f3a Update README.md Egbert Rijke 2015-12-03 19:55:16 -0500
  • 036d251d25 feat(constructions): add universal properties of free (abelian) groups Floris van Doorn 2015-11-21 14:32:45 -0500
  • 96f74d8ea6 feat(group_theory): move files to subfolder, define free (abelian) group Floris van Doorn 2015-11-21 02:06:05 -0500
  • 519f5952b0 add .gitignore and .project files Floris van Doorn 2015-11-20 12:58:16 -0500
  • 6da27d3121 feat(group_theory): start on group theory, define quotient group Floris van Doorn 2015-11-20 12:25:29 -0500
  • 9997bad07e more information README.md Ulrik Buchholtz 2015-11-18 17:09:18 -0500
  • f34a36ce17 Create README.md jdramsey 2015-11-18 17:00:07 -0500