Homology of subcomplexes

The bottom subobject of a homological complex and the quotient by its top subobject have vanishing homology. These facts apply to any complex shape, assuming only that the homology in the requested degree exists. They supply the vanishing conditions at the ends of a finite filtration.

We also record how quasi-isomorphisms interact with subobjects: the inclusion of Subobject.mk f is a quasi-isomorphism exactly when f is, and the inclusion of a subcomplex A ≤ B is a quasi-isomorphism when the inclusions of A and B are.

filtration. For complexes of modules, the arrow of the subobject generated by a monomorphism has the same degreewise range as the monomorphism.

theorem CategoryTheory.Subobject.isZero_homology_of_eq_bot {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} [Limits.HasZeroObject C] (S : Subobject K) (hS : S = ⊥) (i : ι) [(underlying.obj S).HasHomology i] : Limits.IsZero ((underlying.obj S).homology i)

The bottom subcomplex has vanishing homology.

theorem CategoryTheory.Subobject.isZero_homology_cokernel_of_eq_top {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} (S : Subobject K) (hS : S = ⊤) [Limits.HasCokernel S.arrow] (i : ι) [(Limits.cokernel S.arrow).HasHomology i] : Limits.IsZero ((Limits.cokernel S.arrow).homology i)

The quotient by the top subcomplex has vanishing homology.

theorem CategoryTheory.Subobject.quasiIso_mk_arrow_iff {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} [∀ (i : ι), K.HasHomology i] {A : HomologicalComplex C c} (f : A ⟶ K) [Mono f] [∀ (i : ι), A.HasHomology i] [∀ (i : ι), (underlying.obj (mk f)).HasHomology i] : QuasiIso (mk f).arrow ↔ QuasiIso f

The inclusion of Subobject.mk f is a quasi-isomorphism exactly when f is.

theorem CategoryTheory.Subobject.quasiIso_ofLE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} [∀ (i : ι), K.HasHomology i] {A B : Subobject K} (h : A ≤ B) [∀ (i : ι), (underlying.obj A).HasHomology i] [∀ (i : ι), (underlying.obj B).HasHomology i] (hA : QuasiIso A.arrow) (hB : QuasiIso B.arrow) : QuasiIso (A.ofLE B h)

If the inclusions of subcomplexes A ≤ B are quasi-isomorphisms, then so is the inclusion A ⟶ B.

theorem CategoryTheory.Subobject.range_mk_arrow_f_hom {S : Type u_1} [Ring S] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat S) c} (i : K ⟶ L) [Mono i] (n : ι) : (ModuleCat.Hom.hom ((mk i).arrow.f n)).range = (ModuleCat.Hom.hom (i.f n)).range

In each degree, the arrow of the subobject generated by a monomorphism of complexes of modules has the same range as the monomorphism itself.