derived functors

Stream: maths

[Scott Morrison]

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]

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]

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

[Oliver Nash]

Oh wow, this is big. Nice one!

[Johan Commelin]

@Scott Morrison This is incredible! Really cool!