Zulip Chat Archive

Stream: maths

Topic: derived functors


view this post on Zulip Scott Morrison (Apr 29 2021 at 13:16):

I still have some moderate sorries to fill in, but I just got

def functor.left_derived (n : ) (F : C  D) [F.additive] : C  D :=
projective_resolutions C  F.map_homotopy_category _ _  homotopy_category.homology_functor D _ n

to typecheck. :-)

view this post on Zulip Scott Morrison (Apr 29 2021 at 13:17):

I think I am going to keep going forward, and make sure that I can calculate this using a chosen projective resolution, before going back to the sorries.

view this post on Zulip Scott Morrison (Apr 29 2021 at 13:18):

Tor and Ext and group (co)homology, here we come. :-)

view this post on Zulip Oliver Nash (Apr 29 2021 at 13:20):

Oh wow, this is big. Nice one!

view this post on Zulip Johan Commelin (Apr 29 2021 at 13:43):

@Scott Morrison This is incredible! Really cool!


Last updated: Jun 17 2021 at 17:28 UTC