Reading H⁰ in a presented category, and in its Grothendieck group #
What is left here after #1320 are the declarations that need something beyond
the dg category: either a chosen ordinary category and the comparison
equivalence of an Enhancement, or the Grothendieck group of the triangulated
structure.
The intrinsic side -- the shift, the distinguished triangles, the functorial
cone diagrams and the exactness of DGFunctor.h0 -- moved to its definition
owner, Algebra/Homology/DGCategory/Pretriangulated/H0/, and nothing there
imports this directory.
ConeFunctor and MorphismCone transport dg cones across a comparison, and
carry that comparison's shift and exactness compatibilities as hypotheses. The
four K0 modules read triangles and twists in K₀, and consume
CategoryTheory/Triangulated/GrothendieckGroup/.