The K-projective model, and the second consumer of DGFullSubcategory

dg-enhancements-e8, part four. DdgProj A is the full dg subcategory of C^dg A on the K-projective complexes.

Why this file exists

dg-enhancements-e8 asks for a reusable full dg subcategory root and for a second consumer of it, and this is the second consumer. The point is not that the K-projective model is needed downstream today -- dg-enhancements-e9 is stated for the K-injective side -- but that a root with one consumer is indistinguishable from a one-off. Every line below that is not the predicate itself is inherited, which is the claim being tested.

The duality is in Mathlib, not here

Each step is the mirror of KInjective.lean with rightOrthogonal replaced by leftOrthogonal, and in every case the mirrored lemma is one Mathlib already has:

K-injective	K-projective
isKInjective_iff_rightOrthogonal	isKProjective_iff_leftOrthogonal
IsKInjective.rightOrthogonal	IsKProjective.leftOrthogonal
(L⟦n⟧).IsKInjective	(K⟦n⟧).IsKProjective
isKInjective_of_injective (below)	isKProjective_of_projective (above)

The bound flips with the variance, which is the one asymmetry worth reading twice: an inhabitant here is IsStrictlyLE d with projective terms, not IsStrictlyGE d with injective ones.

ObjectProperty.ext_of_isTriangulatedClosed₃ is used on the same side in both files, because the mapping cone is the third vertex either way; it is the orthogonality that is dualised, not the triangle.

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

A mapping cone of a map between K-projective complexes is K-projective. The mirror of isKInjective_mappingCone, across leftOrthogonal.

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

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

Equations

• K.IsKProjectiveObj = (CategoryTheory.Cdg.of A K).IsKProjective

theorem CategoryTheory.Cdg.isKProjectiveObj_iff {A : Type u} [Category.{v, u} A] [Abelian A] (K : Cdg A) : K.IsKProjectiveObj ↔ (of A K).IsKProjective

IsKProjectiveObj is Mathlib's IsKProjective, read through Cdg.of.

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

The dg category of K-projective complexes, as the full dg subcategory of C^dg A on them.

Equations

• CategoryTheory.Cdg.DdgProj A = CategoryTheory.DGFullSubcategory CategoryTheory.Cdg.IsKProjectiveObj

@[implicit_reducible]

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

The K-projective model is a dg category, by DGFullSubcategory.

Equations

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

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

A K-projective complex, as an object of the model.

Equations

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

def CategoryTheory.Cdg.DdgProj.ofLE {A : Type u} [Category.{v, u} A] [Abelian A] (K : CochainComplex A ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), Projective (K.X n)] : DdgProj A

A strictly bounded-above complex of projectives is an object of the model. Note the direction: bounded above with projective terms, dual to Ddg.ofGE.

Equations

• CategoryTheory.Cdg.DdgProj.ofLE K d = CategoryTheory.Cdg.DdgProj.mk K ⋯

The three closure conditions, mirrored

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

IsKProjectiveObj holds of a zero complex.

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

IsKProjectiveObj is closed under shifts.

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

IsKProjectiveObj is closed under cones.

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

The K-projective model is pretriangulated, by the same theorem and the same three inputs as the K-injective one.