ModuleCat.homology'_ext

theorem ModuleCat.homology'_ext : ∀ {R : Type v} [inst : Ring R] {L M N K : ModuleCat R} {f : L ⟶ M} {g : M ⟶ N} (w : CategoryTheory.CategoryStruct.comp f g = 0) {h k : homology' f g w ⟶ K}, (∀ (x : ↥(LinearMap.ker g)), h ((CategoryTheory.Limits.cokernel.π (imageToKernel f g w)) (ModuleCat.toKernelSubobject x)) = k ((CategoryTheory.Limits.cokernel.π (imageToKernel f g w)) (ModuleCat.toKernelSubobject x))) → h = k

This theorem states that in order to prove that two maps from a homology group are equal, it suffices to check they are equal on the images of cycles. More precisely, given a ring `R` and four modules `L`, `M`, `N`, and `K` over `R`, as well as morphisms `f : L ⟶ M` and `g : M ⟶ N` such that their composition `f ≫ g` is zero, and two maps `h` and `k` from the homology of `f` and `g` to `K`, if for every element `x` in the kernel of `g`, the image of `x` under the map from the cokernel of `f` and `g` to the kernel subobject of `x` via `h` is equal to the image via `k`, then the two maps `h` and `k` are equal.

More concisely: Given homomorphisms `f: L ⟶ M`, `g: M ⟶ N`, and `h, k: H_*(f, g): H*(K) ⟶ H*(L)`, if `f ≫ g = 0` and for all `x ∈ ker(g)`, `h(cokernel(f, g)(x)) = k(x)`, then `h = k`.