Dg categories

Dg categories, their dg functors and elementary constructions, their internal pretriangulated refinement, and raw dg models.

DGCategory is a bespoke class built on Mathlib's CochainComplex.HomComplex (ADR-0010, ADR-0011); it does not extend EnrichedCategory, because the ℤ-graded cochain complexes it would enrich over are not monoidal at the pin. By definition site it therefore lives here, beside the homotopy category it enhances, and not under CategoryTheory/Enriched/. If the enriched encoding (ADR-0010 Option A′) lands, the subtree moves there in the same change.

The triangulated category carried by H⁰ of a pretriangulated dg category is owned here, under DGCategory/Pretriangulated/H0/: the shift, the distinguished triangles built from dg cones, the functorial cone diagrams, and the exactness of the functors DGFunctor.h0 produces are intrinsic to the dg category and mention no other category.

Comparing that structure with a specified ordinary or triangulated category is DerivedAlgGeo.CategoryTheory.Triangulated.DGEnhancement, which owns both the underlying H⁰ presentation and its exact refinement. Nothing in this tree imports it.