Topic: derived functors
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. :-)
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.
Scott Morrison (Apr 29 2021 at 13:18):
Tor and Ext and group (co)homology, here we come. :-)
Oliver Nash (Apr 29 2021 at 13:20):
Oh wow, this is big. Nice one!
Johan Commelin (Apr 29 2021 at 13:43):
@Scott Morrison This is incredible! Really cool!
Last updated: Jun 17 2021 at 17:28 UTC