When a full dg subcategory is pretriangulated

dg-enhancements-e8, part two. IsPretriangulated asks for a zero object, a shift of every object, and a cone on every closed degree-zero morphism. This file says exactly what a predicate P must satisfy for the full dg subcategory on P to inherit all three.

The restriction direction, and why only that one

IsShiftBy X n Y and IsConeOf f Z are not data attached to Y and Z: they are representability conditions, each of the form "right composition with one fixed closed element is bijective from every object W". That universal quantifier is what makes this file short, and it is also what makes it one-directional.

In DGFullSubcategory P the quantifier ranges over the objects satisfying P, which are fewer. So an ambient witness is already a witness downstairs, with the same element and the same closedness proof and the bijectivity instantiated at W.obj — that is all isShiftByRestrict and isConeOfRestrict do, and neither needs a single rewrite, because dgHom X Y is dgHom X.obj Y.obj by definition.

The converse is false in general, and it is worth being plain about why: a map compRight W hom p q h can be bijective for every W satisfying P and fail to be bijective for some ambient W. Nothing below asserts that direction, and no later file should reach for it.

Why the hypotheses are closure conditions rather than a supplied conclusion

The three fields of IsPretriangulated (DGFullSubcategory P) could have been taken as inputs. They are not. Each is derived from a statement about P alone:

• ContainsZeroObject P — P holds of some object with vanishing identity;
• ClosedUnderShift P — a shift of a P-object can be chosen in P;
• ClosedUnderCone P — a cone on a closed degree-zero map between P-objects can be chosen in P.

Each of the three is a property of the predicate, checkable where the predicate is defined, and for the K-injective model each is a theorem of Mathlib rather than an assumption this repository makes. That is the point of stating them this way: HomotopyCategory/DGEnhancement/KInjective.lean discharges all three, so nothing about resolutions arrives here as a caller-supplied conclusion.

Ambient witnesses restrict

def CategoryTheory.DGFullSubcategory.isShiftByRestrict {C : Type u} [DGCategory C] {P : C → Prop} {X Y : DGFullSubcategory P} {n : ℤ} (h : IsShiftBy X.obj n Y.obj) : IsShiftBy X n Y

An ambient shift witness is a shift witness in the full dg subcategory: same element, same closedness, bijectivity read at fewer objects.

Equations

• CategoryTheory.DGFullSubcategory.isShiftByRestrict h = { hom := h.hom, hom_closed := ⋯, bijective := ⋯ }

def CategoryTheory.DGFullSubcategory.isConeOfRestrict {C : Type u} [DGCategory C] {P : C → Prop} {X Y Z : DGFullSubcategory P} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (h : IsConeOf f Z.obj) : IsConeOf f Z

An ambient cone witness is a cone witness in the full dg subcategory. Both inclusions and both of their defining identities are the ambient ones.

Equations

• CategoryTheory.DGFullSubcategory.isConeOfRestrict h = { inr := h.inr, inr_closed := ⋯, inl := h.inl, δ_inl := ⋯, bijective := ⋯ }

The closure conditions

def CategoryTheory.DGFullSubcategory.ContainsZeroObject {C : Type u} [DGCategory C] (P : C → Prop) : Prop

P holds of an object whose identity vanishes, so the full dg subcategory has the zero object H⁰ needs.

Equations

• CategoryTheory.DGFullSubcategory.ContainsZeroObject P = ∃ (Z : C), P Z ∧ CategoryTheory.DGCategoryStruct.dgId Z = 0

def CategoryTheory.DGFullSubcategory.ClosedUnderShift {C : Type u} [DGCategory C] (P : C → Prop) : Prop

P is closed under shifts: for every P-object and every degree, some shift of it in that degree again satisfies P. The shift is chosen, not constructed, because IsShiftBy is a representability condition and a dg category has no shift functor.

Equations

• CategoryTheory.DGFullSubcategory.ClosedUnderShift P = ∀ (X : C), P X → ∀ (n : ℤ), ∃ (Y : C), P Y ∧ Nonempty (CategoryTheory.IsShiftBy X n Y)

def CategoryTheory.DGFullSubcategory.ClosedUnderCone {C : Type u} [DGCategory C] (P : C → Prop) : Prop

P is closed under cones: a cone on a closed degree-zero morphism between P-objects can be chosen to satisfy P.

Equations

• CategoryTheory.DGFullSubcategory.ClosedUnderCone P = ∀ {X Y : C}, P X → P Y → ∀ f ∈ CategoryTheory.cocycles X Y, ∃ (Z : C), P Z ∧ Nonempty (CategoryTheory.IsConeOf f Z)

The inheritance theorem

theorem CategoryTheory.DGFullSubcategory.isPretriangulated {C : Type u} [DGCategory C] {P : C → Prop} (hz : ContainsZeroObject P) (hs : ClosedUnderShift P) (hc : ClosedUnderCone P) : IsPretriangulated (DGFullSubcategory P)

A full dg subcategory closed under zero, shifts and cones is pretriangulated. Each field is the corresponding closure condition followed by the matching restriction lemma; no representability is reproved.

theorem CategoryTheory.DGFullSubcategory.closedUnderShift_true {C : Type u} [DGCategory C] [IsPretriangulated C] : ClosedUnderShift fun (x : C) => True

The whole dg category is the full dg subcategory on fun _ => True, and the three closure conditions there are exactly the three fields of IsPretriangulated C. Recorded as a sanity check on the shape of the conditions: if any of them had been stated too strongly, this would fail.

theorem CategoryTheory.DGFullSubcategory.closedUnderCone_true {C : Type u} [DGCategory C] [IsPretriangulated C] : ClosedUnderCone fun (x : C) => True

The cone half of the same sanity check.

theorem CategoryTheory.DGFullSubcategory.containsZeroObject_true {C : Type u} [DGCategory C] [IsPretriangulated C] : ContainsZeroObject fun (x : C) => True

The zero-object half of the same sanity check.