Cohomology membership from terms of a complex

A property of objects closed under kernels and cokernels passes from the adjacent terms of a complex to its homology. Closure under isomorphisms then transports this membership to the corresponding object of the derived category. The result applies to unbounded complexes without extension closure.

Main definitions

This file introduces no new carrier, class, or instance.

Main results

• DerivedCategory.cohomologyIn_Q_obj_of_termwise places the localization of a termwise-property complex in the existing cohomology object property.

Implementation notes

The cycle object is a kernel of the outgoing differential. Homology is a cokernel of the map from the predecessor term to cycles. The private helpers use only the three adjacent terms; the public theorem uses every term and the canonical derived homology comparison.

References

The proof uses Mathlib's HomologicalComplex.cyclesIsKernel, HomologicalComplex.homologyIsCokernel, and DerivedCategory.homologyFunctorFactors at the pinned Mathlib revision.

Tags

Derived category; homology; object property.

theorem DerivedCategory.cohomologyIn_Q_obj_of_termwise {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] [P.IsClosedUnderIsomorphisms] (K : CochainComplex A ℤ) (hK : ∀ (i : ℤ), P (K.X i)) : cohomologyIn P (Q.obj K)

Kernel closure gives the cycles property and cokernel closure gives the homology property. The derived homology factorization transports this to cohomologyIn P after localization; extension closure is unnecessary.