Factoring through subcomplexes of complexes of modules

A subcomplex S of a homological complex L of modules is recorded degreewise by the range of the components of S.arrow. A morphism of complexes into L factors through S as soon as it does degreewise, that is, as soon as each of its components lands in the range of the corresponding component of S.arrow (CategoryTheory.Subobject.factors_of_forall_mem_range).

The degreewise ranges are monotone in the subcomplex (CategoryTheory.Subobject.range_arrow_f_hom_le) and stable under the differentials of L (CategoryTheory.Subobject.d_mem_range_arrow_f_hom). When S ≤ T and the quotient complex T/S is exact in degree j, a cycle of L lying in T is a boundary of an element of T up to an element of S (CategoryTheory.Subobject.exists_sub_d_mem_range_arrow_f_hom_of_isZero_homology_cokernel).

Main results

• CategoryTheory.Subobject.factors_iff_forall_mem_range: a morphism factors through a subcomplex exactly when it does degreewise.

theorem CategoryTheory.Subobject.factors_of_forall_mem_range {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} (S : Subobject L) (g : K ⟶ L) (h : ∀ (n : ι) (x : ↑(K.X n)), (ModuleCat.Hom.hom (g.f n)) x ∈ (ModuleCat.Hom.hom (S.arrow.f n)).range) : S.Factors g

A morphism of complexes of modules whose components land in the ranges of the components of the inclusion of a subcomplex factors through it.

theorem CategoryTheory.Subobject.factors_iff_forall_mem_range {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} (S : Subobject L) (g : K ⟶ L) : S.Factors g ↔ ∀ (n : ι) (x : ↑(K.X n)), (ModuleCat.Hom.hom (g.f n)) x ∈ (ModuleCat.Hom.hom (S.arrow.f n)).range

A morphism of complexes of modules factors through a subcomplex exactly when each of its components lands in the range of the corresponding component of the inclusion.

theorem CategoryTheory.Subobject.range_arrow_f_hom_le {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} {L : HomologicalComplex (ModuleCat R) c} {S T : Subobject L} (h : S ≤ T) (n : ι) : (ModuleCat.Hom.hom (S.arrow.f n)).range ≤ (ModuleCat.Hom.hom (T.arrow.f n)).range

The degreewise ranges of the inclusions of subcomplexes are monotone in the subcomplex.

theorem CategoryTheory.Subobject.d_mem_range_arrow_f_hom {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} {L : HomologicalComplex (ModuleCat R) c} (S : Subobject L) (i j : ι) {x : ↑(L.X i)} (hx : x ∈ (ModuleCat.Hom.hom (S.arrow.f i)).range) : (ModuleCat.Hom.hom (L.d i j)) x ∈ (ModuleCat.Hom.hom (S.arrow.f j)).range

The differentials of L send the degreewise range of the inclusion of a subcomplex into the range in the next degree.

theorem CategoryTheory.Subobject.exists_sub_d_mem_range_arrow_f_hom_of_isZero_homology_cokernel {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} {L : HomologicalComplex (ModuleCat R) c} {S T : Subobject L} (h : S ≤ T) {i j k : ι} (hi : c.prev j = i) (hk : c.next j = k) (hH : Limits.IsZero ((Limits.cokernel (S.ofLE T h)).homology j)) {z : ↑(L.X j)} (hz : z ∈ (ModuleCat.Hom.hom (T.arrow.f j)).range) (hdz : (ModuleCat.Hom.hom (L.d j k)) z = 0) : ∃ y ∈ (ModuleCat.Hom.hom (T.arrow.f i)).range, z - (ModuleCat.Hom.hom (L.d i j)) y ∈ (ModuleCat.Hom.hom (S.arrow.f j)).range

The elementwise form of the vanishing of H^j(T/S) for subcomplexes S ≤ T: a cycle of L lying in T is, up to an element of S, the boundary of an element of T.