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

Commit graph

  • d3f42e5a3c starting to think about equivalences of prespectra Egbert Rijke 2017-06-28 17:53:09 +0100
  • 9934c9c73d trivial homotopy groups of truncated spectra Ulrik Buchholtz 2017-06-28 17:19:23 +0100
  • 2092e4a83b resolve merge conflict Egbert Rijke 2017-06-28 15:53:27 +0100
  • f4e74687f9 conjecture about prespectrification Egbert Rijke 2017-06-28 15:49:46 +0100
  • 1c07806726 work on strunc Ulrik Buchholtz 2017-06-28 15:21:11 +0100
  • b419e9c8f7 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-06-28 14:05:43 +0100
  • d814c472ab add strunc file for truncatedness/truncations of spectra Floris van Doorn 2017-06-28 13:14:48 +0100
  • 4974b2ea3d Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-06-28 13:13:13 +0100
  • 635b10821f temporarily disable proof, which caused error after redefinition of phomotopy Floris van Doorn 2017-06-28 11:08:41 +0100
  • 36cd36a64c making a start on the exactness of the derived couple Egbert Rijke 2017-06-19 13:40:52 -0400
  • cfdfa0f22a Work on the fact that pointed dependent products preserve fibration sequences Floris van Doorn 2017-06-17 17:21:28 -0400
  • 313754ee2b completed definition of k prime Egbert Rijke 2017-06-16 17:06:04 -0400
  • a1e01456f1 Merge branch 'master' of https://github.com/cmu-phil/Spectral Egbert Rijke 2017-06-16 15:41:15 -0400
  • 17a5218b62 definition of j prime completed Egbert Rijke 2017-06-16 15:41:01 -0400
  • 89118f2a8e Merge remote-tracking branch 'origin/new_lean' into new_lean Steve Awodey 2017-06-16 14:50:55 -0400
  • a2c4e0858d clean up computation of fiber of postnikov tower Floris van Doorn 2017-06-15 17:49:48 -0400
  • 0885a7ef4a renamed pequiv.MK2 to pequiv.MK Floris van Doorn 2017-06-14 22:55:10 -0400
  • b6fa4e8716 compute fibers of postnikov tower Floris van Doorn 2017-06-14 20:04:35 -0400
  • da95ea0acb remove uses of homomorphism_comp_compute Floris van Doorn 2017-06-14 18:46:54 -0400
  • 5d57e60a43 Minor optimization. favonia 2017-06-09 15:55:19 -0600
  • a78c92636e Add Hptorus. favonia 2017-06-09 15:48:00 -0600
  • b8de7ffd80 work on functorial action of prespectrum homotopy groups Floris van Doorn 2017-06-09 17:42:05 -0400
  • d057ddec51 Add Hpwedge. favonia 2017-06-09 15:00:56 -0600
  • 9cfc13d4cf naturality for wedge elimination Robert Rose 2017-06-09 16:51:13 -0400
  • f93fc153d4 fix explicit arguments of dirsum_functor_homotopy Floris van Doorn 2017-06-09 14:28:52 -0400
  • c8043a6f9f Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-09 12:24:58 -0600
  • 39883fd3ee A bit of code for incoherent homotopies between maps of spectra Yuri Sulyma 2017-06-09 12:24:33 -0600
  • 0acc5c786d Add fwedge_down_left. favonia 2017-06-09 11:55:34 -0600
  • 2e55a4a4ef fwedge_prespectrum spiceghello 2017-06-09 11:51:04 -0600
  • 88dc53d113 Add the missing 'p'. favonia 2017-06-09 11:22:15 -0600
  • 3c51bbea1f minor spiceghello 2017-06-09 10:36:10 -0600
  • 61e3a9ce0e redefine homology to use smash with prespectra Floris van Doorn 2017-06-09 12:25:09 -0400
  • e90c657dcb Add dirsum_down_lift. favonia 2017-06-09 10:08:21 -0600
  • c9ce91524f Fix typo and type of Hfwedge. favonia 2017-06-09 06:38:07 -0600
  • f098063d96 More lemmas about fwedge. favonia 2017-06-09 06:35:21 -0600
  • 5826288a48 composition/inverse for homotopies of pointed spaces and spectra Yuri Sulyma 2017-06-08 20:07:46 -0600
  • cf3dec8fb9 Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-08 20:01:47 -0600
  • aa54adf770 Use psquare/phsquare in spectrum Yuri Sulyma 2017-06-08 20:01:41 -0600
  • b2ab29c3c3 on colim.elim o pinclusion, and corollary on spectra spiceghello 2017-06-08 18:28:15 -0600
  • e4168439c0 work on homotopy group of prespectrum Floris van Doorn 2017-06-08 20:09:48 -0400
  • 56d97200d6 Fix the naming. favonia 2017-06-08 18:06:59 -0600
  • c0ea92a0b5 Add dirsum_functor_isomorphism. favonia 2017-06-08 17:51:25 -0600
  • 8362498b56 Remove AddGroup symbol. favonia 2017-06-08 17:48:26 -0600
  • bc69a96faa Rename homomorphism_comp_compute. favonia 2017-06-08 16:49:47 -0600
  • 3bc528a17c Unfinished stuff. favonia 2017-06-08 14:11:42 -0600
  • 4165f9a613 Add pwedge_pequiv and plift_pwedge. favonia 2017-06-08 14:11:02 -0600
  • 85c0ae53a6 Merge branch 'master' of https://github.com/fpvandoorn/Spectral Robert Rose 2017-06-08 18:22:41 -0400
  • 8b97339ffa seq_colim universal property Robert Rose 2017-06-08 18:17:23 -0400
  • a06ecd4523 part of spectrify_elim spiceghello 2017-06-08 15:07:50 -0600
  • db6fccc971 pmap_eta spiceghello 2017-06-08 14:50:25 -0600
  • 52b6320cd0 Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-08 14:05:14 -0600
  • 3fd6e8e852 Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-08 14:04:58 -0600
  • a3146d0d2a Fix bug Yuri Sulyma 2017-06-08 14:03:29 -0600
  • 7f637206a0 Add a few spectrification things Yuri Sulyma 2017-06-08 14:03:10 -0600
  • daf3472468 Start proving that the homology theory associated to a spectrum satisfies the ES axioms Yuri Sulyma 2017-06-08 14:02:28 -0600
  • 1b21765391 work on spectrify elim Floris van Doorn 2017-06-08 15:41:57 -0400
  • 15cc880b15 spectrify_map (last triangle missing) spiceghello 2017-06-08 12:13:01 -0600
  • abe62d1f61 spectrify_pequiv spiceghello 2017-06-08 10:26:21 -0600
  • 3ab890c464 fix rename ordinary_theory -> ordinary_cohomology_theory Floris van Doorn 2017-06-08 12:12:46 -0400
  • 5cda45ae1d Add the missing 'p'. favonia 2017-06-08 10:14:07 -0600
  • a8592e0184 Add homology_ordinary_theory and copyright statement. favonia 2017-06-08 09:54:47 -0600
  • 5b384882f8 rename ordinary_theory to ordinary_cohomology_theory Floris van Doorn 2017-06-08 11:51:49 -0400
  • 664d971d4b add some constructor attributes to product_group Floris van Doorn 2017-06-08 11:41:37 -0400
  • 4ca9907929 fix spectrum file Floris van Doorn 2017-06-08 11:33:08 -0400
  • 8e3c2d020f Add binary_dirsum. favonia 2017-06-08 09:28:52 -0600
  • 1fee1395ed Add Group_sum_elim. favonia 2017-06-07 12:30:08 -0600
  • 9f1df6becb lemma in colim for spectrification spiceghello 2017-06-08 09:27:57 -0600
  • 877c740ea9 progress on spectrum and colim Floris van Doorn 2017-06-08 11:19:29 -0400
  • 2e9a225a82 minor spiceghello 2017-06-08 09:16:57 -0600
  • 480bcd5dee another lemma for spectrification spiceghello 2017-06-07 12:24:25 -0600
  • 610aa351b8 Add interchange. favonia 2017-06-07 12:03:00 -0600
  • 7ed3e47e09 Removing troublesome composition of group homomorphism in quotient_group Robert Rose 2017-06-07 12:02:09 -0600
  • 21a0dcfcfe seq_colim_elim added Robert Rose 2017-06-07 10:30:32 -0600
  • 9256bf8861 Change to dirsum_elim_compute Robert Rose 2017-06-07 10:28:00 -0600
  • 5fffcd6f70 Fix copyright statement. favonia 2017-06-07 09:42:58 -0600
  • f84cebe13c Add product_inl and product_inr. favonia 2017-06-07 09:41:41 -0600
  • 607e5343b1 Remove useless esimp to speed up Lean. favonia 2017-06-07 09:39:33 -0600
  • df3ce3872f Fix the statement of susp_product. favonia 2017-06-07 09:38:33 -0600
  • c19c885de3 fix [unfold] index Floris van Doorn 2017-06-07 11:34:09 -0400
  • 9274ba04c9 Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-07 09:40:08 -0600
  • ec852ca73f Merge branch 'master' of github.com:fpvandoorn/Spectral Yuri Sulyma 2017-06-07 09:39:46 -0600
  • 0a135fbe91 Remove useless esimp to speed up Lean. favonia 2017-06-07 09:39:33 -0600
  • abe46fd211 Functoriality of smashing a pointed space with a prespectrum Yuri Sulyma 2017-06-07 09:39:26 -0600
  • 95173995f4 Merge branch 'master' of github.com:fpvandoorn/Spectral favonia 2017-06-07 09:38:45 -0600
  • 8639eaff7a Fix the statement of susp_product. favonia 2017-06-07 09:38:33 -0600
  • be802be170 fix [unfold] index Floris van Doorn 2017-06-07 11:34:09 -0400
  • 984d564cc6 unbundle set in direct_sum Floris van Doorn 2017-06-07 11:30:09 -0400
  • 5fdc8ad2c8 Seal several definitions as theorems. favonia 2017-06-06 23:10:25 -0600
  • 18ee7ce410 redefine direct_sum to use multiplicative groups Floris van Doorn 2017-06-07 01:01:19 -0400
  • 3881982774 small changes to spectrum Floris van Doorn 2017-06-07 00:54:52 -0400
  • 74955d5a75 Stub of seq_colim Robert Rose 2017-06-06 21:53:45 -0600
  • fecc9b4a70 The statement of susp_product. favonia 2017-06-06 18:09:19 -0600
  • 5afbc4afdd a lemma for spectrification spiceghello 2017-06-06 17:52:30 -0600
  • bf8f77a9e5 Add Hsphere. favonia 2017-06-06 17:30:42 -0600
  • a292dba89f Merge two group namespaces. favonia 2017-06-06 17:18:10 -0600
  • b6394b9750 A more useful lemma! favonia 2017-06-06 17:12:50 -0600
  • 32a6cc639d Add several helper functions. favonia 2017-06-06 16:57:55 -0600
  • 52b8fee078 Clean up homotopy.hlean a little bit. favonia 2017-06-06 16:57:34 -0600
  • 7940bf0cd6 Add pmap.eta. favonia 2017-06-06 16:57:17 -0600
  • 5e4c536d27 progress on spectrify Floris van Doorn 2017-06-06 17:07:07 -0400