# Complexes of modules #

We provide some additional API to work with homological complexes in ModuleCat R.

theorem ModuleCat.homology'_ext {R : Type v} [Ring R] {L : } {M : } {N : } {K : } {f : L M} {g : M N} (w : ) {h : homology' f g w✝ K} {k : homology' f g w✝ K} (w : ∀ (x : ()), h (() (ModuleCat.toKernelSubobject x)) = k (() (ModuleCat.toKernelSubobject x))) :
h = k

To prove that two maps out of a homology group are equal, it suffices to check they are equal on the images of cycles.

@[reducible, inline]
abbrev ModuleCat.toCycles' {R : Type v} [Ring R] {ι : Type u_1} {c : } {C : } {i : ι} (x : (LinearMap.ker (C.dFrom i))) :
(CategoryTheory.Subobject.underlying.obj (C.cycles' i))

Bundle an element C.X i such that C.dFrom i x = 0 as a term of C.cycles i.

Equations
• = ModuleCat.toKernelSubobject x
Instances For
theorem ModuleCat.cycles'_ext {R : Type v} [Ring R] {ι : Type u_1} {c : } {C : } {i : ι} {x : (CategoryTheory.Subobject.underlying.obj (C.cycles' i))} {y : (CategoryTheory.Subobject.underlying.obj (C.cycles' i))} (w : (C.cycles' i).arrow x = (C.cycles' i).arrow y) :
x = y
@[simp]
theorem ModuleCat.cycles'Map_toCycles' {R : Type v} [Ring R] {ι : Type u_1} {c : } {C : } {D : } (f : C D) {i : ι} (x : (LinearMap.ker (C.dFrom i))) :
() = ModuleCat.toCycles' (f.f i) x,
@[reducible, inline]
abbrev ModuleCat.toHomology' {R : Type v} [Ring R] {ι : Type u_1} {c : } {C : } {i : ι} (x : (LinearMap.ker (C.dFrom i))) :
(C.homology' i)

Build a term of C.homology i from an element C.X i such that C.d_from i x = 0.

Equations
Instances For
theorem ModuleCat.homology'_ext' {R : Type v} [Ring R] {ι : Type u_1} {c : } {C : } {M : } (i : ι) {h : C.homology' i M} {k : C.homology' i M} (w : ∀ (x : (LinearMap.ker (C.dFrom i))), = ) :
h = k