explicit homology in Ab

Stream: condensed mathematics

[Johan Commelin]

There are 3 reasonably self-contained sorrys in for_mathlib/homology_iso_Ab.lean. They require a bit of fiddling around with categorical (co)kernels and explicit (co)kernels in Ab.