D^dg A: the K-injective model of the derived dg enhancement

dg-enhancements-e8, part three. Ddg A is the full dg subcategory of C^dg A on the K-injective complexes. It is the first consumer of DGFullSubcategory; KProjective.lean is the second.

Nothing here constructs a resolution

The whole point of building on Mathlib's CochainComplex.IsKInjective is that this file consumes resolution theory rather than restating it. Concretely, the three closure conditions of DGFullSubcategory.isPretriangulated are discharged as follows, and not one of them is an assumption:

condition	discharged by
ContainsZeroObject	a zero complex receives only the zero map
ClosedUnderShift	Mathlib's instance (L⟦n⟧).IsKInjective
ClosedUnderCone	isKInjective_mappingCone, below

The shift row is exact rather than approximate: Cdg.shiftObj K n is defined as (of A K)⟦n⟧, so Mathlib's instance is about the very object the dg shift witness names. The same holds for cones, where Cdg.coneObj f hf is mappingCone (coneHom f hf).

The one thing Mathlib does not already have

Mathlib proves that K-injectives are the right orthogonal of the acyclic complexes (isKInjective_iff_rightOrthogonal) and that a right orthogonal of a triangulated subcategory is triangulated, but it never puts the two together to say that a mapping cone of a map between K-injectives is K-injective. isKInjective_mappingCone does exactly that and nothing more: move both hypotheses across the orthogonality characterisation, apply ext_of_isTriangulatedClosed₃ to the cone's distinguished triangle in the homotopy category, and move back.

That it is a triangulated-subcategory argument rather than a homotopy construction is the reason it is three lines. A direct proof -- given an acyclic K and a map into the cone, split it and patch the two homotopies -- would be a page, and would be reproving IsTriangulatedClosed₃.

Inhabitation

isKInjective_of_injective is Mathlib's supply of objects: a complex that is strictly bounded below and injective in every degree is K-injective. ofGE packages one as an object of Ddg A, so the model is not vacuous under a hypothesis this repository invented.

theorem CategoryTheory.Cdg.isKInjective_mappingCone {A : Type u} [Category.{v, u} A] [Abelian A] {K L : CochainComplex A ℤ} (φ : K ⟶ L) [K.IsKInjective] [L.IsKInjective] : (CochainComplex.mappingCone φ).IsKInjective

A mapping cone of a map between K-injective complexes is K-injective.

Both hypotheses and the conclusion are moved across isKInjective_iff_rightOrthogonal; in between, the statement is that the right orthogonal of the acyclic complexes is closed under the third vertex of a distinguished triangle, which is Mathlib's ObjectProperty.ext_of_isTriangulatedClosed₃.

def CategoryTheory.Cdg.IsKInjectiveObj {A : Type u} [Category.{v, u} A] [Abelian A] (K : Cdg A) : Prop

The K-injective objects of C^dg A, as a predicate on its objects.

Named rather than written inline, because it is the parameter of Ddg and every closure lemma below is a statement about it.

Equations

• K.IsKInjectiveObj = (CategoryTheory.Cdg.of A K).IsKInjective

theorem CategoryTheory.Cdg.isKInjectiveObj_iff {A : Type u} [Category.{v, u} A] [Abelian A] (K : Cdg A) : K.IsKInjectiveObj ↔ (of A K).IsKInjective

IsKInjectiveObj is Mathlib's IsKInjective, read through Cdg.of.

def CategoryTheory.Cdg.Ddg (A : Type u) [Category.{v, u} A] [Abelian A] : Type (max u v)

D^dg A: the derived dg enhancement on the K-injective model, as the full dg subcategory of C^dg A on the K-injective complexes.

Equations

• CategoryTheory.Cdg.Ddg A = CategoryTheory.DGFullSubcategory CategoryTheory.Cdg.IsKInjectiveObj

@[implicit_reducible]

instance CategoryTheory.Cdg.Ddg.instDGCategoryDdg {A : Type u} [Category.{v, u} A] [Abelian A] : DGCategory (Ddg A)

D^dg A is a dg category, by DGFullSubcategory. No axiom is reproved here; see that file on why every one of them is the ambient one applied.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Cdg.Ddg.mk {A : Type u} [Category.{v, u} A] [Abelian A] (K : Cdg A) (hK : K.IsKInjectiveObj) : Ddg A

A K-injective complex, as an object of D^dg A.

Equations

• CategoryTheory.Cdg.Ddg.mk K hK = CategoryTheory.DGFullSubcategory.mk K hK

def CategoryTheory.Cdg.Ddg.ofGE {A : Type u} [Category.{v, u} A] [Abelian A] (K : CochainComplex A ℤ) (d : ℤ) [K.IsStrictlyGE d] [∀ (n : ℤ), Injective (K.X n)] : Ddg A

A strictly bounded-below complex of injectives is an object of D^dg A. This is the model's non-vacuity, and it rests on Mathlib's isKInjective_of_injective rather than on any hypothesis stated here.

Equations

• CategoryTheory.Cdg.Ddg.ofGE K d = CategoryTheory.Cdg.Ddg.mk K ⋯

The three closure conditions

Each is a statement about IsKInjectiveObj alone, checkable here, and each is discharged by Mathlib.

theorem CategoryTheory.Cdg.containsZeroObject_isKInjectiveObj {A : Type u} [Category.{v, u} A] [Abelian A] [Limits.HasZeroObject A] : DGFullSubcategory.ContainsZeroObject IsKInjectiveObj

IsKInjectiveObj holds of a zero complex: every map into a zero object is the zero map, which is homotopic to zero by Homotopy.ofEq.

theorem CategoryTheory.Cdg.closedUnderShift_isKInjectiveObj {A : Type u} [Category.{v, u} A] [Abelian A] : DGFullSubcategory.ClosedUnderShift IsKInjectiveObj

IsKInjectiveObj is closed under shifts. The shift witness Cdg.isShiftBy names Cdg.shiftObj K n, which is (of A K)⟦n⟧ definitionally, so Mathlib's shift instance applies to it directly.

theorem CategoryTheory.Cdg.closedUnderCone_isKInjectiveObj {A : Type u} [Category.{v, u} A] [Abelian A] : DGFullSubcategory.ClosedUnderCone IsKInjectiveObj

IsKInjectiveObj is closed under cones. The cone witness Cdg.isConeOf names Cdg.coneObj f hf, which is mappingCone (coneHom f hf), so this is isKInjective_mappingCone.

instance CategoryTheory.Cdg.instIsPretriangulatedDdg {A : Type u} [Category.{v, u} A] [Abelian A] [Limits.HasZeroObject A] : IsPretriangulated (Ddg A)

D^dg A is pretriangulated. Every input is a closure property of K-injectivity discharged above; the representability of shifts and cones is inherited from C^dg A by restriction.