Zulip Chat Archive

Stream: PR reviews

Topic: homology redesign and derived functors

Scott Morrison (May 04 2021 at 11:57):

I just made a huge block of 20 PRs about the new design for homology, and as an outgrowth of this the definition and basic API for left-derived functors.

  • #7460 #7466 #7462 #7464 --- small easy PRs for the homology redesign
  • #7467 --- more about kernel and image subobjects (depends on #7460 and #7466)
  • #7473 --- the main refactor of chain complexes and homology (depends on #7467, #7462, and #7464)
  • #7479 #7481 #7482 --- minor PRs exercising the refactor, but not esential for what comes later (depend on #7473)
  • #7480 --- augmentation and truncation of chain complexes (depends on #7473)
  • #7485 --- refactor of the projective object API (depends on #7473)
  • #7477 --- chain complexes supported in a single degree (depends on #7473)
  • #7478 --- the category of chain complexes is additive, and various functoriality properties (depends on #7477 and #7463)
  • #7483 --- homotopies (depends on #7478)
  • #7484 --- the homotopy category (depends on #7483 and #7465)
  • #7486 --- projective resolutions (depends on #7485 and #7484)
  • #7487 --- derived functors (depends on #7486)
  • #7488 --- abelian categories with enough projectives have projective resolutions (depends on #7486 and #7480)

Scott Morrison (May 04 2021 at 12:00):

Sorry to dump everything at once: I'm sure CI is overwhelmed for a while now. :-) I wanted to get derived functors working nicely before committing to PRs of the early stuff.

Adam Topaz (May 04 2021 at 13:56):

This is really awesome!

Scott Morrison (May 06 2021 at 04:40):

A few steps got merged. Current PRs ready for review: #7467 #7514.

Johan Commelin (May 07 2021 at 10:43):

Next up seems to be the huge redesign: #7473
(I've merged master, which shrunk the diff from ~1600 added lines to ~1500 :laughing:)

Scott Morrison (May 07 2021 at 12:21):

This could actually be split up if we were happy to have a regression for a while in the middle. The problem here is that I have not just renamed image_to_kernel_map to image_to_kernel, but also largely rewritten it to use the subobject API.

Scott Morrison (May 07 2021 at 12:22):

This would ideally be it's own PR.

Johan Commelin (May 07 2021 at 12:22):

I personally think that a split is not necessary

Scott Morrison (May 07 2021 at 12:22):

However it completely breaks the existing work on homology.

Scott Morrison (May 07 2021 at 12:23):

That that work has been entirely rewritten, so if we did want to make the PRs more fine grained, we could ditch that as a first step, replace image_to_kernel_map, then put back in the new homology.

Scott Morrison (May 07 2021 at 12:23):

But I agree this isn't necessary, and in any case I couldn't even start until next week.

Scott Morrison (May 07 2021 at 12:24):

Now I'm going to go to sleep listening to the waves breaking on a cliff. :-)

Kevin Buzzard (May 07 2021 at 12:25):

Thank you so much for all this homology work. It would be wonderful if we have finally cracked it. there are so many cohomology theories which we are in a position to do once we have the machine working.

Scott Morrison (May 09 2021 at 22:42):

Two related things that really should be explored sooner rather than later: working with short exact sequences, and building a nat-indexed chain complex where you want to specify some fixed finite number of terms by hand, then do the rest inductively (e.g. in the main use case, 0 everywhere).

Johan Commelin (May 11 2021 at 07:30):

#7473 is on the queue

Scott Morrison (May 11 2021 at 10:10):

The two interesting PRs to review now are #7477 and #7485. Also ready for review now are #7479, #7481, and #7482, but these are less interesting, and just "leaves" on this big batch of PRs.

Scott Morrison (May 14 2021 at 00:50):

Next up on the critical path is #7478, showing that various categories and functors are additive. Hopefully this one is quite straightforward, and then we have #7483, introducing homotopies, after which we can start trying things out in LTE.

Adam Topaz (May 14 2021 at 01:13):

Added some comments for #7478

Scott Morrison (May 14 2021 at 01:30):

Thanks! I've updated.

Adam Topaz (May 14 2021 at 01:34):

@Scott Morrison I guess at some point we should add the analogue of single₀_map_homological_complex for the functor single. Would you like to leave that to a later PR?

Scott Morrison (May 14 2021 at 03:15):

Done.

Scott Morrison (May 14 2021 at 10:55):

I just ported #6308, on old WIP PR about the normalized Moore complex, over to the new design. It was fairly straightforward, happily.

Johan Commelin (May 14 2021 at 13:17):

That's good news! Thanks for trying that!

Johan Commelin (May 15 2021 at 04:25):

I feel like the top post is too far up, so here is a new copy of the status of these PRs

Johan Commelin (May 15 2021 at 04:25):

  • #7460 #7466 #7462 #7464 --- small easy PRs for the homology redesign
  • #7467 --- more about kernel and image subobjects (depends on #7460 and #7466)
  • #7473 --- the main refactor of chain complexes and homology (depends on #7467, #7462, and #7464)
  • #7479 #7481 #7482 --- minor PRs exercising the refactor, but not esential for what comes later (depend on #7473)
  • #7480 --- augmentation and truncation of chain complexes (depends on #7473)
  • #7485 --- refactor of the projective object API (depends on #7473)
  • #7477 --- chain complexes supported in a single degree (depends on #7473)
  • #7478 --- the category of chain complexes is additive, and various functoriality properties (depends on #7477 and #7463)
  • #7483 --- homotopies (depends on #7478)
  • #7484 --- the homotopy category (depends on #7483 and #7465)
  • #7486 --- projective resolutions (depends on #7485 and #7484)
  • #7487 --- derived functors (depends on #7486)
  • #7488 --- abelian categories with enough projectives have projective resolutions (depends on #7486 and #7480)
  • #7512 --- definition of tor in a monoidal category (depends on #7487)
  • #7514 --- the opposite of an abelian category is abelian
  • #7525 --- definition of ext in a linear abelian category (depends on #7487 #7488 and #7514)

Scott Morrison (May 15 2021 at 14:31):

#7480, #7485, and #7483 have been merged, and I've added a dependency in #7484 to David Warn's #7501, which bors is currently merging.

Adam Topaz (May 15 2021 at 14:41):

The derived category is on the horizon!?

Johan Commelin (May 15 2021 at 14:44):

I'm starting the LTE refactor.

Scott Morrison (May 15 2021 at 14:46):

The derived category itself is still a bit harder than anything in these PRs. We need some nontrivial work on localization first.

Adam Topaz (May 15 2021 at 14:47):

branch#cat_localization

Adam Topaz (May 15 2021 at 14:48):

But that's just some silly inductive construction. We probably want more control on the inverses we add

Adam Topaz (May 15 2021 at 14:53):

And besides, now that we have the free category on a quiver, we can even simplify this inductive construction significantly

David Wärn (May 15 2021 at 17:01):

I don't know the maths here, but I guess the localization can be defined as a docs#category_theory.quotient of a docs#category_theory.paths

Johan Commelin (May 21 2021 at 05:58):

The remaining tail, as far as I can see:

  • #7484 --- the homotopy category (depends on #7483 and #7465)
  • #7486 --- projective resolutions (depends on #7485 and #7484)
  • #7487 --- derived functors (depends on #7486)
  • #7488 --- abelian categories with enough projectives have projective resolutions (depends on #7486 and #7480)
  • #7512 --- definition of tor in a monoidal category (depends on #7487)
  • #7514 --- the opposite of an abelian category is abelian
  • #7525 --- definition of ext in a linear abelian category (depends on #7487 #7488 and #7514)

Johan Commelin (May 31 2021 at 09:29):

I've kicked #7486 on the queue

Johan Commelin (May 31 2021 at 15:11):

Derived functors are now unblocked!

Last updated: Dec 20 2023 at 11:08 UTC