A pseudo-resolution (my terminology) of `M` is a complex `C` such that `∀ i, RⁱF(C) = 0` implies `∀ i, RⁱF(M) = 0`. MacLane's Q' construction has been formalised. Now we need to show that it satisfies the claim above. Depends on #74 and #76
A pseudo-resolution (my terminology) of
Mis a complexCsuch that∀ i, RⁱF(C) = 0implies∀ i, RⁱF(M) = 0.MacLane's Q' construction has been formalised. Now we need to show that it satisfies the claim above.
Depends on #74 and #76