C^dg A enhances the homotopy category

Enhancement is a structure with three fields and no inhabitant until this file. dg-enhancements-e6's acceptance asks for exactly that — "it is inhabited by a constructed example before any theorem quantifies over it" — and both halves of the example are already proved:

• Cdg.isPretriangulated (dg-enhancements-e5) supplies the shift, the cone and the zero object;
• Cdg.seam (dg-enhancements-e4) supplies H⁰ (C^dg A) ≌ HomotopyCategory A.

So the enhancement is the two of them adjacent, and it is a def with no proof obligations of its own. That it reads as trivial is the point: the content was paid for in e4 and e5, and an Enhancement that needed new mathematics to inhabit would mean the structure had been mis-stated.

This is C^dg, not K^dg

dg-enhancements-e7 wants K^dg(A) to enhance HomotopyCategory A with an agreement theorem against Mathlib's own triangulated instance. That is a different and stronger statement. What is here is the enhancement whose existence e6 needs in order to quantify over enhancements at all.

noncomputable def CategoryTheory.Cdg.enhancement (A : Type u) [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : Enhancement (HomotopyCategory A (ComplexShape.up ℤ))

C^dg A is a dg enhancement of the homotopy category of A.

Equations

• CategoryTheory.Cdg.enhancement A = { dgCat := CategoryTheory.Cdg A, isDGCategory := CategoryTheory.Cdg.instDGCategory, isPretriangulated := ⋯, equiv := CategoryTheory.Cdg.seam }