The derived seam: H⁰(D^dg A) and DerivedCategory A

dg-enhancements-e9, the theorem the DG track was opened for. The comparison functor is built here, its full faithfulness is proved unconditionally, and the equivalence is derived from one named external input.

The route

D^dg A is the full dg subcategory of C^dg A on the K-injective complexes (dg-enhancements-e8). So the comparison factors through work that already exists:

H⁰(D^dg A) --(ι).h0--> H⁰(C^dg A) --h0Functor--> K(A) --Qh--> D(A)

The middle arrow is dg-enhancements-e4's Cdg.seam, already an equivalence. The first is H⁰ of the inclusion dg functor, and it is fully faithful because the inclusion acts as AddMonoidHom.id on Hom-complexes. Only the last arrow carries new content, and it is where K-injectivity is spent.

What is unconditional, and what is not

Full faithfulness is unconditional. Mathlib's CochainComplex.IsKInjective.Qh_map_bijective says Qh is bijective on morphisms into a K-injective complex. Both objects here are K-injective, so that applies directly and nothing further is assumed.

Essential surjectivity is not, and cannot be at this pin. It asks that every object of D(A) be represented by a K-injective complex, i.e. that K-injective resolutions exist. That is Spaltenstein's theorem, and Mathlib does not have it: Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean cites [spaltenstein1998] in its references and proves no existence statement, and there is no EnoughKInjectives, no kInjectiveResolution and no HasKInjective anywhere in the library at mathlib_rev.

The input, and the line it must not cross

HasKInjectiveResolutions asks exactly for the missing mathematics: every cochain complex admits a quasi-isomorphism to a K-injective one. It is a real, externally checkable statement about A — true for Grothendieck abelian categories — and a caller supplying it is asserting a theorem, not a convenience.

What it deliberately is not is a field asserting that the comparison functor is an equivalence. That would be assuming the conclusion, which is the failure mode dg-enhancements-e8's acceptance names when it forbids a resolution theorem represented by a caller-supplied conclusion field. The distinction is the whole design of this file: the input is upstream of the theorem and the theorem is derived from it.

When someone formalizes Spaltenstein's construction, this class becomes an instance and derivedSeam becomes unconditional with no change to any consumer. That is the seam the design is protecting.

References

• N. Spaltenstein, Resolutions of unbounded complexes, Compositio Math. 65 (1988) — the existence theorem HasKInjectiveResolutions stands in for.
• Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean — the full faithfulness half, which Mathlib does supply.

@[reducible, inline]

abbrev CategoryTheory.Cdg.ddgInclusion {A : Type u} [Category.{v, u} A] [Abelian A] : DGFunctor (Ddg A) (Cdg A)

The inclusion of the K-injective model into the dg category of all cochain complexes, as a dg functor.

Equations

• CategoryTheory.Cdg.ddgInclusion = CategoryTheory.DGFullSubcategory.iota CategoryTheory.Cdg.IsKInjectiveObj

class CategoryTheory.Cdg.HasKInjectiveResolutions (A : Type u) [Category.{v, u} A] [Abelian A] : Prop

Every cochain complex admits a K-injective resolution.

The one external input of this file, and the exact statement Mathlib lacks at mathlib_rev. It holds for Grothendieck abelian categories by Spaltenstein's construction.

Stated as a quasi-isomorphism into a K-injective complex — the mathematics — rather than as any claim about the comparison functor below. See the module docstring on why that distinction is load-bearing.

• exists_kInjective_quasiIso (K : CochainComplex A ℤ) : ∃ (L : CochainComplex A ℤ) (_ : L.IsKInjective) (f : K ⟶ L), QuasiIso f

  Every cochain complex receives a quasi-isomorphism from a K-injective one.

noncomputable def CategoryTheory.Cdg.derivedSeamFunctor {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] : Functor (H0 (Ddg A)) (DerivedCategory A)

The derived seam functor H⁰(D^dg A) ⥤ D(A).

Composite of H⁰ of the inclusion, dg-enhancements-e4's seam, and Mathlib's Qh. The direction is explicit and is the only one this file constructs: nothing here builds a functor out of D(A).

Equations

• CategoryTheory.Cdg.derivedSeamFunctor = CategoryTheory.Cdg.ddgInclusion.h0.comp (CategoryTheory.Cdg.h0Functor.comp DerivedCategory.Qh)

H⁰ of the inclusion is fully faithful

Both are definitional. DGFullSubcategory gives Ddg A the ambient Hom-complexes unchanged, so cocycles and coboundaries between two K-injective objects are literally the ambient ones, and H⁰ of the inclusion is the identity map between two quotients of the same group by the same subgroup.

instance CategoryTheory.Cdg.ddgInclusion_h0_faithful {A : Type u} [Category.{v, u} A] [Abelian A] : ddgInclusion.h0.Faithful

instance CategoryTheory.Cdg.ddgInclusion_h0_full {A : Type u} [Category.{v, u} A] [Abelian A] : ddgInclusion.h0.Full

The composite is fully faithful, unconditionally

The three arrows are bijective on Hom for three different reasons, and only the last one spends K-injectivity. Qh is not fully faithful in general; it is bijective into a K-injective target, which is exactly what the objects of D^dg A are.

@[reducible, inline]

abbrev CategoryTheory.Cdg.underlying {A : Type u} [Category.{v, u} A] [Abelian A] (X : H0 (Ddg A)) : CochainComplex A ℤ

The underlying cochain complex of an object of H⁰(D^dg A).

Equations

• CategoryTheory.Cdg.underlying X = CategoryTheory.Cdg.of A (CategoryTheory.DGFullSubcategory.obj (CategoryTheory.H0.of (CategoryTheory.Cdg.Ddg A) X))

instance CategoryTheory.Cdg.underlying_isKInjective {A : Type u} [Category.{v, u} A] [Abelian A] (X : H0 (Ddg A)) : (underlying X).IsKInjective

theorem CategoryTheory.Cdg.h0Functor_obj_ddgInclusion {A : Type u} [Category.{v, u} A] [Abelian A] (X : H0 (Ddg A)) : h0Functor.obj (ddgInclusion.h0.obj X) = (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj (underlying X)

The seam functor lands on the quotient of the underlying complex; rfl, and it is what lets Mathlib's bijectivity lemma apply.

theorem CategoryTheory.Cdg.derivedSeamFunctor_map_bijective {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] (X Y : H0 (Ddg A)) : Function.Bijective derivedSeamFunctor.map

The derived seam functor is bijective on Hom-sets.

Three bijections, three different reasons: H⁰ of the inclusion because the Hom-complexes are the ambient ones, h0Functor because dg-enhancements-e4 proved it an equivalence, and Qh because the target is K-injective. Only the last is about resolutions, and it assumes nothing.

instance CategoryTheory.Cdg.derivedSeamFunctor_faithful {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] : derivedSeamFunctor.Faithful

instance CategoryTheory.Cdg.derivedSeamFunctor_full {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] : derivedSeamFunctor.Full

Essential surjectivity, and the one place the input is spent

instance CategoryTheory.Cdg.derivedCategoryQ_essSurj {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] : DerivedCategory.Q.EssSurj

Q is essentially surjective because it is a localization functor. Named rather than anonymous: an audited generated name breaks silently on a rename.

instance CategoryTheory.Cdg.derivedSeamFunctor_essSurj {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] [HasKInjectiveResolutions A] : derivedSeamFunctor.EssSurj

The derived seam functor is essentially surjective, given K-injective resolutions.

This is the only declaration in the file that uses HasKInjectiveResolutions, and the use is exactly the expected one: resolve a representing complex, then transport along the resulting quasi-isomorphism.

instance CategoryTheory.Cdg.derivedSeamFunctor_isEquivalence {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] [HasKInjectiveResolutions A] : derivedSeamFunctor.IsEquivalence

Full, faithful and essentially surjective, so an equivalence. Stated the same way dg-enhancements-e4 states it for Cdg.seam.

noncomputable def CategoryTheory.Cdg.derivedSeam {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] [HasKInjectiveResolutions A] : H0 (Ddg A) ≌ DerivedCategory A

The derived seam. H⁰(D^dg A) ≌ D(A).

Full faithfulness is unconditional; only essential surjectivity consumes HasKInjectiveResolutions. The direction is H⁰(D^dg A) ⟶ D(A), and it is derivedSeamFunctor.

Equations

• CategoryTheory.Cdg.derivedSeam = CategoryTheory.Cdg.derivedSeamFunctor.asEquivalence