jcommelin opened this issue 3 years ago · 0 comments
A pseudo-resolution (my terminology) of M is a complex C such that ∀ i, RⁱF(C) = 0 implies ∀ i, RⁱF(M) = 0.
M
C
∀ i, RⁱF(C) = 0
∀ 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