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

Commit graph

  • 3b078f5f1d
         Update README.md: linkfix master Floris van Doorn 2023-05-15 18:56:12 +0200
  • 9075b67c49 update colim/README Floris van Doorn 2019-01-11 16:11:43 -0500
  • 59aed195ba cleanup in colimit Floris van Doorn 2019-01-10 23:45:37 -0500
  • a4d47837ab small change in notes/smash Floris van Doorn 2018-12-12 23:58:10 -0500
  • 02f5c54b77 cleanup, expand explanation Floris van Doorn 2018-11-13 19:36:35 -0500
  • 2913de520d finish proving that the gysin sequence consists of the correct groups Floris van Doorn 2018-11-13 19:22:07 -0500
  • ea402f56ea finish first part of constructing gysin sequence Floris van Doorn 2018-11-12 18:07:05 -0500
  • b251465e72 continue on gysin sequence Floris van Doorn 2018-10-24 21:19:26 -0400
  • af447f4f8e start on gysin sequence Floris van Doorn 2018-10-09 21:27:50 -0400
  • 94066a6ba8 some more algebra Floris van Doorn 2018-10-09 21:27:37 -0400
  • 5c9927ce2d fix universe level for has_choice Floris van Doorn 2018-10-09 21:27:27 -0400
  • eb8601dc93 prove some properties about is_built_from Floris van Doorn 2018-10-05 18:03:12 -0400
  • 266e37d9ed prove some properties about first quadrant spectral sequences where the degree of d is as usual Floris van Doorn 2018-10-05 18:01:43 -0400
  • 0c4baacfcc fix free_abelian_group and direct_sum Ulrik Buchholtz 2018-11-02 13:39:40 +0100
  • 2f16008700 no longer working on truncatedness of suspensions of pointed sets (: - still some clean-up to do Ulrik Buchholtz 2018-10-26 16:51:42 +0200
  • 4313f3f642 working on truncatedness of suspensions of sets Ulrik Buchholtz 2018-10-24 17:07:35 +0200
  • 8f998637b5 factor free group on set via free group on pointed set Ulrik Buchholtz 2018-10-23 13:30:26 +0200
  • 32512bf47d compute unreduced cohomology of spheres Floris van Doorn 2018-10-03 19:39:08 -0400
  • c19192fbe5 fix error with numerals in integers Floris van Doorn 2018-10-03 17:14:37 -0400
  • 138fef02fa update README/usage Floris van Doorn 2018-10-03 13:42:09 -0400
  • 3b25ec0266 update README Floris van Doorn 2018-10-02 15:36:27 -0400
  • 627deba24b smash.tex: small changes, add some preliminary references Floris van Doorn 2018-10-02 12:12:50 -0400
  • 075f12efe2 WIP smash.tex Floris van Doorn 2018-09-24 14:05:50 +0200
  • 179575794a Prove basic properties of spectral sequences Floris van Doorn 2018-10-01 17:44:49 -0400
  • 4481935a83 define spectral sequence from exact couple Floris van Doorn 2018-09-29 16:23:03 +0200
  • 96e11300ed fix indexing of abutment in spectral sequences Floris van Doorn 2018-09-29 12:07:54 +0200
  • 48cf8a5f31 typo in converging_spectral_sequence Floris van Doorn 2018-09-26 20:07:01 +0200
  • acae548d3a some cleanup, and add a todo list Floris van Doorn 2018-09-26 19:53:23 +0200
  • 8937371b33 put exit in projective space file Floris van Doorn 2018-09-26 13:17:57 +0200
  • f9ce395b1c reindex the AHSS and SSS Floris van Doorn 2018-09-26 13:12:33 +0200
  • 4d3053daff Change the definition of graded morphisms Floris van Doorn 2018-09-26 13:12:24 +0200
  • db8402e1af define deloopable types, define cup product Floris van Doorn 2018-09-24 17:31:13 +0200
  • e019097fed update after changes in Lean Floris van Doorn 2018-09-20 16:03:59 +0200
  • da033c0f4c work on dependent smash and cup product on EM-spaces Floris van Doorn 2018-09-20 02:08:45 +0200
  • 68345f75ce move more and update after changes Floris van Doorn 2018-09-11 17:06:46 +0200
  • f7e0ce0e20 add file on binary pointed maps Floris van Doorn 2018-09-10 18:03:29 +0200
  • ba5648fb87 start on construction of cup product of EM-spaces Floris van Doorn 2018-09-10 18:02:07 +0200
  • c3650048f0 fixes and additions Floris van Doorn 2018-09-10 18:01:44 +0200
  • e4db64ae9a fixes after changes in the library Floris van Doorn 2018-09-07 16:30:39 +0200
  • 0dd7ec3c29 add missing file Floris van Doorn 2018-09-07 17:53:36 +0200
  • f835dc896e fix typos spiceghello 2018-04-10 10:41:57 +0200
  • d2c7eb2368 generalize the spectral sequence of a sequence of spectrum maps Floris van Doorn 2018-06-06 16:40:56 -0400
  • fffc3cd03a fix after moving stuff to library Floris van Doorn 2018-09-05 22:56:40 +0200
  • e1d2392a13 move more stuff Floris van Doorn 2018-09-04 11:54:26 +0200
  • be0d5977f6 move to lib and older things Floris van Doorn 2018-08-19 13:52:20 +0200
  • ec5b9dba12 more on decidable free group Floris van Doorn 2018-06-06 16:40:41 -0400
  • dd14277e0b additions on pentagons with interchange spiceghello 2018-03-26 09:11:55 +0200
  • 12f23c0dbe the free group on a decidable set eliminates to any InfGroup Floris van Doorn 2018-03-25 16:51:23 -0400
  • 9b624edb9f fix indexing for homotopy group of presprectrum Floris van Doorn 2018-03-24 17:08:41 -0400
  • bcb78b4575 minor additions Floris van Doorn 2018-03-24 16:57:24 -0400
  • cf25666beb higher groups: add is_trunc_ppi_of_is_conn Floris van Doorn 2018-02-01 00:10:58 -0500
  • 2f957b7828 higher groups: finalize file Floris van Doorn 2018-01-31 21:39:01 -0500
  • e34fba2027 change title in README Floris van Doorn 2018-01-31 13:21:42 -0500
  • fbad62541b higher groups: rename Grp to GType Floris van Doorn 2018-01-31 13:01:17 -0500
  • 9914352e10 higher groups: prove equivalence of categories for 0-Grp Floris van Doorn 2018-01-31 12:32:20 -0500
  • 85b04639cb higher groups: prove naturality of all adjunctions Floris van Doorn 2018-01-30 20:28:15 -0500
  • 98092df59c various things about higher groups Floris van Doorn 2018-01-30 16:11:13 -0500
  • e0365d2c65 higher_groups: finish adjunction between loop and deloop Floris van Doorn 2018-01-29 15:30:10 -0500
  • 0949070096 Prove stabilization and work on equivalence of categories Floris van Doorn 2018-01-28 18:05:45 -0500
  • 9d91957303 connectivity of loop_susp_counit Ulrik Buchholtz 2018-01-27 19:42:09 +0100
  • 8acdbf3f67 the wedge extension lemma actually works! Ulrik Buchholtz 2018-01-27 19:01:42 +0100
  • f1fe71b0a8 comparison of fibers between prod_of_wedge and loop_susp_counit Ulrik Buchholtz 2018-01-27 10:56:01 +0100
  • 7a5bb0c2fe alternative version of pushout flattening Ulrik Buchholtz 2018-01-27 10:55:09 +0100
  • f51dac9045 rename pequiv.sigma_char_equiv' to pequiv.sigma_char_pmap Ulrik Buchholtz 2018-01-26 18:15:32 +0100
  • 3a09e743a2 fix error in EM Floris van Doorn 2018-01-23 12:47:29 -0500
  • 6de6e72a03 simplify proof of is_trunc_Grp Floris van Doorn 2018-01-23 12:44:01 -0500
  • d7b8530718 prove that [n;k]Grp is an (n+1)-type Ulrik Buchholtz 2018-01-21 12:28:43 +0100
  • d5a0080355 prove various properties about pointed truncated and/or connected types Floris van Doorn 2018-01-19 17:25:34 -0500
  • a22ac8af28 work on connectification of a type Floris van Doorn 2018-01-19 10:07:28 -0500
  • f6bbc75365 unindent higher_groups Floris van Doorn 2018-01-18 14:50:26 -0500
  • 44cf88a2a5 fix connectivity levels, they were off by one Floris van Doorn 2018-01-17 19:12:13 -0500
  • 9cf33dd3a7 continue working on higher groups Floris van Doorn 2018-01-17 18:43:50 -0500
  • aa191493e9 give alternative definition of free group on a set with decidable equality Floris van Doorn 2018-01-14 17:58:43 -0800
  • 743985e3d8 Work on pointed naturality of smash-C Floris van Doorn 2017-12-08 15:30:34 +0100
  • 5bfb6e8d15 Work on notes on smash product spiceghello 2017-12-07 12:36:55 +0100
  • ac7e75bb9e continue on unit-counit Floris van Doorn 2017-12-07 13:32:11 +0100
  • f92cce42e3 add discussion to notes smash Floris van Doorn 2017-12-06 18:15:33 +0100
  • c1cde3db1c notes, minor spiceghello 2017-12-06 18:15:31 +0100
  • 114a296531 notes on smash spiceghello 2017-12-06 09:19:31 +0100
  • 31483834f4 notes yoneda spiceghello 2017-12-04 14:58:17 +0100
  • e2ac187822 notes on naturality spiceghello 2017-12-01 11:59:24 +0100
  • 4d39e86f27 Mostly formalize the pentagon of the smash product, fix the order of the arguments in the adjunction Floris van Doorn 2017-11-28 08:26:13 +0100
  • 3813b17479 Write notes with a mostly-complete proof that the smash product forms a 1-coherent symmetric monoidal category spiceghello 2017-11-29 11:52:30 +0100
  • d4ab6e15ef small changes in colimit Floris van Doorn 2017-11-28 08:25:51 +0100
  • 91c21e9d92 add readme for colimit Floris van Doorn 2017-11-24 19:38:54 -0500
  • 899e3cf2e4 prove that iota is n-truncated/n-connected if the maps in the sequence are Floris van Doorn 2017-11-24 19:37:49 -0500
  • 1a35543661 minor changes in colimit Floris van Doorn 2017-11-22 20:15:46 -0500
  • cca1279f45 remove colim file from Spectral Floris van Doorn 2017-11-22 16:30:52 -0500
  • 03cacd2dc1 move colimit project here Floris van Doorn 2017-11-22 16:12:30 -0500
  • 12a9345df1 Restructure spectral sequences, compute cohomology of projective space Floris van Doorn 2017-09-21 20:14:24 -0400
  • ee4c9f989a we don't need to assume that the map is pointed Floris van Doorn 2017-09-20 22:13:57 -0400
  • b31658c2f3 construct serre spectral sequence for any map Floris van Doorn 2017-09-20 22:00:58 -0400
  • f8157068e4 derive the unparametrized serre spectral sequence Floris van Doorn 2017-09-15 20:39:51 -0400
  • ceee305a60 remove spaces at end of lines Floris van Doorn 2017-09-15 19:02:47 -0400
  • 741e585ca0 fix homotopy.EM so that it compiles Floris van Doorn 2017-09-15 19:01:37 -0400
  • f89edc5403 * cleaned up univalent_subcategory.hlean * removed duplicates from move_to_lib.hlean Jonas Frey 2017-09-14 15:36:35 -0400
  • 593efa1bf2 some cleanup univalent_subcategory.hlean Jonas Frey 2017-09-07 00:39:50 -0400
  • d8350ad125 add file containing proof about univalent subcategories and that AbGrp is univalent Jonas Frey 2017-09-06 16:14:25 -0400
  • 50837e789f Merge 72d5210915 into af30b19099 jonas-frey 2017-09-14 19:46:39 +0000
  • 72d5210915 * cleaned up univalent_subcategory.hlean * removed duplicates from move_to_lib.hlean Jonas Frey 2017-09-14 15:36:35 -0400