Shifts and cones inside a dg category

dg-enhancements-e5. A dg category has no shift functor and no cone construction the way a triangulated category has: it has representability conditions, and this file states them.

Why these are predicates rather than constructions

X[n] and Cone f are not built from X and f. They are objects of C whose dg module of maps in is prescribed:

• Y is a shift of X by n when dgHom W Y ≅ (dgHom W X)⟦n⟧, naturally in W;
• Z is a cone on a closed degree-zero f : X ⟶ Y when dgHom W Z is the mapping cone of dgHom W X → dgHom W Y, naturally in W.

Both are conditions a dg category may or may not satisfy, so IsPretriangulated is a class asserting that it does.

Which notion this is: strongly pretriangulated

Each condition asks for a strict isomorphism: right composition with the closed witness is bijective in every degree, from every W, so Hom(-, X)[n] and Hom(-, Y) agree in Z⁰ of the dg module category and not merely up to homotopy. That is Drinfeld's strongly pretriangulated, and it is stronger than what Bondal--Kapranov and Keller call pretriangulated, where the shift and the cone need only be representable up to homotopy equivalence.

Strong implies weak, so nothing proved from [IsPretriangulated C] is in doubt; the class simply has fewer inhabitants than its name suggests. The choice costs nothing for the models — every dg category in this repository has strict shifts and cones, and strictness is what lets H⁰ be triangulated by a construction rather than by a homotopy argument — and it loses no object, since every pretriangulated dg category is quasi-equivalent to a strongly pretriangulated one. What it does change is the meaning of any statement that quantifies over dg categories, and there is exactly one of those planned: uniqueness of enhancements, which read over this class is a different and weaker statement than the literature's. See CategoryTheory/Triangulated/DGEnhancement/Basic.lean.

References: Bondal--Kapranov, Enhanced triangulated categories (1990) §3; Drinfeld, DG quotients of DG categories (2004) §2.4; Keller, On differential graded categories, ICM 2006, §4.5.

Naturality is not an axiom here

Each condition is stated as right composition with one fixed element is bijective, and that is what buys the naturality clause for free: composition with a fixed element commutes with composition on the other side by dgComp_assoc, so there is no square left to impose. Stating the iso of dg modules directly would put a graded naturality axiom in the structure and then oblige every witness to prove it.

The degree conventions

Hom^d(K, L) = ∏ₚ Hom(Kᵖ, L^{p+d}), so with L = X[n] the identity-like element of Hom(X, X[n]) sits in degree -n, not n. That is why IsShiftBy.hom has degree -n, and it matches Mathlib: mappingCone.inl is a Cochain F (mappingCone φ) (-1), the inclusion of F[1].

The cone conditions are transcribed from Mathlib's mappingCone API rather than rederived. IsConeOf.δ_inl is mappingCone.δ_inl, and the bijectivity clause is the pair mappingCone.id (surjectivity) and inl_fst/inl_snd/inr_fst/ inr_snd (injectivity).

The zero clause is dg-level, and stronger than it needs to be

IsPretriangulated.exists_zero asks for an object with dgId Z = 0. In a preadditive category that is exactly "Z is a zero object", so the clause says Z⁰ C and H⁰ C have a zero object on the nose.

The literature does not axiomatize this: Cone (𝟙 X) is contractible, so H⁰ gets its zero object from the cone clause alone. Contractibility is a homotopy statement about H⁰, which is dg-enhancements-e6's subject, and deriving the zero object there rather than assuming it here would invert the dependency. The clause is kept, and it costs nothing: every model in this repository has a strict dg zero object.

def CategoryTheory.compRight {C : Type u} [DGCategory C] (W : C) {X Y : C} {n : ℤ} (ε : ↑((DGCategoryStruct.dgHom X Y).X n)) (p q : ℤ) (h : p + n = q) : ↑((DGCategoryStruct.dgHom W X).X p) →+ ↑((DGCategoryStruct.dgHom W Y).X q)

Right composition with a fixed ε : (dgHom X Y).X n, as an additive map on the Hom-complex from any W. This is the map every representability condition below asks to be bijective.

Equations

• CategoryTheory.compRight W ε p q h = (CategoryTheory.DGCategoryStruct.dgComp p n q h).flip ε

@[simp]

theorem CategoryTheory.compRight_apply {C : Type u} [DGCategory C] (W : C) {X Y : C} {n : ℤ} (ε : ↑((DGCategoryStruct.dgHom X Y).X n)) (p q : ℤ) (h : p + n = q) (f : ↑((DGCategoryStruct.dgHom W X).X p)) : (compRight W ε p q h) f = ((DGCategoryStruct.dgComp p n q h) f) ε

structure CategoryTheory.IsShiftBy {C : Type u} [DGCategory C] (X : C) (n : ℤ) (Y : C) : Type v

ε exhibits Y as a shift of X by n: it is closed of degree -n, and right composition with it identifies dgHom W X with dgHom W Y in every degree, for every W.

• hom : ↑((DGCategoryStruct.dgHom X Y).X (-n))

  The identity-like element, of degree -n.

• hom_closed : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d (-n) (-n + 1))) self.hom = 0

  It is closed.

• bijective (W : C) (p q : ℤ) (h : p + -n = q) : Function.Bijective ⇑(compRight W self.hom p q h)

  Right composition with it is bijective in every degree, from every object.

structure CategoryTheory.IsConeOf {C : Type u} [DGCategory C] {X Y : C} (f : ↑((DGCategoryStruct.dgHom X Y).X 0)) (Z : C) : Type v

Z is a cone on the closed degree-zero morphism f : X ⟶ Y: it carries an inclusion inr of Y and a degree -1 inclusion inl of X whose differential is f ≫ inr, and every map into Z splits uniquely along the two.

• inr : ↑((DGCategoryStruct.dgHom Y Z).X 0)

  The inclusion of Y.

• inr_closed : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y Z).d 0 1)) self.inr = 0

  It is closed.

• inl : ↑((DGCategoryStruct.dgHom X Z).X (-1))

  The inclusion of X, of degree -1.

• δ_inl : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Z).d (-1) 0)) self.inl = ((DGCategoryStruct.dgComp 0 0 0 ⋯) f) self.inr

  Its differential is f followed by inr. This is mappingCone.δ_inl.

• bijective (W : C) (p q : ℤ) (hq : p + 1 = q) : Function.Bijective fun (ab : ↑((DGCategoryStruct.dgHom W X).X q) × ↑((DGCategoryStruct.dgHom W Y).X p)) => ((DGCategoryStruct.dgComp q (-1) p ⋯) ab.1) self.inl + ((DGCategoryStruct.dgComp p 0 p ⋯) ab.2) self.inr

  Every map into Z splits uniquely as a ≫ inl + b ≫ inr.

theorem CategoryTheory.dgComp_closed {C : Type u} [DGCategory C] {X Y Z : C} {p q r r' : ℤ} (h : p + q = r) (hr : r + 1 = r') {f : ↑((DGCategoryStruct.dgHom X Y).X p)} {g : ↑((DGCategoryStruct.dgHom Y Z).X q)} (hf : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p (p + 1))) f = 0) (hg : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y Z).d q (q + 1))) g = 0) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Z).d r r')) (((DGCategoryStruct.dgComp p q r h) f) g) = 0

A composite of closed elements is closed. Both Leibniz terms carry a factor that vanishes, so the sign never has to be computed. Stated once here because every construction below composes two or three closed elements.

def CategoryTheory.IsShiftBy.self {C : Type u} [DGCategory C] (X : C) : IsShiftBy X 0 X

Every object is its own shift by zero, witnessed by the identity. The degree--0 and degree-0 Hom-groups are the same group, so no transport is needed.

Equations

• CategoryTheory.IsShiftBy.self X = { hom := CategoryTheory.DGCategoryStruct.dgId X, hom_closed := ⋯, bijective := ⋯ }

noncomputable def CategoryTheory.IsShiftBy.inv {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : ↑((DGCategoryStruct.dgHom Y X).X n)

The element inverse to s.hom. It exists because right composition with s.hom is surjective onto (dgHom Y Y).X 0, which contains dgId Y.

Equations

• s.inv = ⋯.choose

theorem CategoryTheory.IsShiftBy.inv_hom {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : ((DGCategoryStruct.dgComp n (-n) 0 ⋯) s.inv) s.hom = DGCategoryStruct.dgId Y

The defining property of s.inv: composing it with s.hom is the identity of Y.

theorem CategoryTheory.IsShiftBy.hom_inv {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : ((DGCategoryStruct.dgComp (-n) n 0 ⋯) s.hom) s.inv = DGCategoryStruct.dgId X

And the other way round. s.hom is not assumed invertible; this is forced, because right composition with it is injective on (dgHom X X).X 0 and both sides go to s.hom.

theorem CategoryTheory.IsShiftBy.inv_closed {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y X).d n (n + 1))) s.inv = 0

s.inv is closed. The Leibniz rule at (n, -n) has its first term killed by s.hom being closed and its second scaled by a unit, so the differential of s.inv composes to zero with s.hom -- and right composition with s.hom is injective.

Precomposition by a shift

The defining bijectivity of IsShiftBy concerns postcomposition with the shift element. Its inverse also makes precomposition an equivalence in the other Hom-variable. Recording that derived operation once avoids rebuilding the same associativity argument whenever a homogeneous map is regraded by shifting its source.

noncomputable def CategoryTheory.IsShiftBy.precompEquiv {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (W : C) (p q : ℤ) (h : n + p = q) : ↑((DGCategoryStruct.dgHom X W).X p) ≃+ ↑((DGCategoryStruct.dgHom Y W).X q)

Precomposition with the inverse of a chosen shift is an additive equivalence

Hom^p(X, W) ≃ Hom^(n+p)(Y, W).

The inverse precomposes with the shift element itself.

Equations

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

theorem CategoryTheory.IsShiftBy.precompEquiv_apply {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (W : C) (p q : ℤ) (h : n + p = q) (f : ↑((DGCategoryStruct.dgHom X W).X p)) : (s.precompEquiv W p q h) f = ((DGCategoryStruct.dgComp n p q h) s.inv) f

Forward source regrading is left composition with the shift inverse.

theorem CategoryTheory.IsShiftBy.precompEquiv_symm_apply {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (W : C) (p q : ℤ) (h : n + p = q) (g : ↑((DGCategoryStruct.dgHom Y W).X q)) : (s.precompEquiv W p q h).symm g = ((DGCategoryStruct.dgComp (-n) q p ⋯) s.hom) g

Inverse source regrading is left composition with the shift element.

theorem CategoryTheory.IsShiftBy.precompEquiv_d {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (W : C) (p q : ℤ) (h : n + p = q) (f : ↑((DGCategoryStruct.dgHom X W).X p)) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y W).d q (q + 1))) ((s.precompEquiv W p q h) f) = (s.precompEquiv W (p + 1) (q + 1) ⋯) ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X W).d p (p + 1))) f)

Precomposition by a shift inverse commutes with the differential.

theorem CategoryTheory.IsShiftBy.precompEquiv_d_eq_zero_iff {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (W : C) (p q : ℤ) (h : n + p = q) (f : ↑((DGCategoryStruct.dgHom X W).X p)) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y W).d q (q + 1))) ((s.precompEquiv W p q h) f) = 0 ↔ (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X W).d p (p + 1))) f = 0

A homogeneous map is closed if and only if its regrading by a source shift is closed.

noncomputable def CategoryTheory.IsShiftBy.compare {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X n Y') : ↑((DGCategoryStruct.dgHom Y Y').X 0)

The comparison between two shifts of X by n: go back along one and out along the other.

Equations

• s.compare s' = ((CategoryTheory.DGCategoryStruct.dgComp n (-n) 0 ⋯) s.inv) s'.hom

theorem CategoryTheory.IsShiftBy.compare_mem_cocycles {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X n Y') : s.compare s' ∈ cocycles Y Y'

The comparison is closed, so it is a morphism of Z⁰. Both factors are closed, so both Leibniz terms vanish.

theorem CategoryTheory.IsShiftBy.compare_comp_compare {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X n Y') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.compare s')) (s'.compare s) = DGCategoryStruct.dgId Y

The two comparisons are mutually inverse, so any two shifts of X by n are isomorphic in Z⁰ -- and therefore in H⁰. This is what lets a shift functor be built from the existential IsPretriangulated.exists_shift without the choice mattering.

theorem CategoryTheory.IsShiftBy.compare_self {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : s.compare s = DGCategoryStruct.dgId Y

Comparing a shift with itself gives the identity.

theorem CategoryTheory.IsShiftBy.compare_trans {C : Type u} [DGCategory C] {X Y Y' Y'' : C} {n : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') (w : IsShiftBy X n Y'') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.compare t)) (t.compare w) = s.compare w

Comparisons compose. Together with compare_self and compare_comp_compare this makes the shifts of X by n into a contractible groupoid inside Z⁰, which is what every coherence statement about the shift functor ultimately reduces to.

noncomputable def CategoryTheory.IsShiftBy.comp' {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) (nm : ℤ) (hnm : n + m = nm) : IsShiftBy X nm Z

Shifts compose, with the resulting degree carried as a free variable.

The free nm is not decoration. Every coherence statement about a shift functor compares objects indexed by n + 0, 0 + n or (a + b) + c against ones indexed by n, n and a + (b + c), and those are propositionally but not definitionally equal. With the degree fixed as n + m the mismatch can only be crossed by an eqToHom that no rewrite normalises; with it free, the equation n + m = nm is a hypothesis about a variable, and subst removes the problem outright. Mathlib carries CochainComplex.shiftFunctorAdd' for the same reason.

The degree of the composite element is handed to dgComp as -nm directly, rather than asking it to normalise -n + -m in a dependent position.

Equations

• s.comp' u nm hnm = { hom := ((CategoryTheory.DGCategoryStruct.dgComp (-n) (-m) (-nm) ⋯) s.hom) u.hom, hom_closed := ⋯, bijective := ⋯ }

noncomputable def CategoryTheory.IsShiftBy.comp {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) : IsShiftBy X (n + m) Z

Shifts compose, at the definitional degree n + m.

Equations

• s.comp u = s.comp' u (n + m) ⋯

theorem CategoryTheory.IsShiftBy.comp_eq_comp' {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) : s.comp u = s.comp' u (n + m) ⋯

comp is comp' at the definitional degree: the primed form carries the target degree as a free variable, this one fixes it at n + m.

@[simp]

theorem CategoryTheory.IsShiftBy.comp'_hom {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) (nm : ℤ) (hnm : n + m = nm) : (s.comp' u nm hnm).hom = ((DGCategoryStruct.dgComp (-n) (-m) (-nm) ⋯) s.hom) u.hom

@[simp]

theorem CategoryTheory.IsShiftBy.comp_hom {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) : (s.comp u).hom = ((DGCategoryStruct.dgComp (-n) (-m) (-(n + m)) ⋯) s.hom) u.hom

theorem CategoryTheory.IsShiftBy.inv_unique {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) {a : ↑((DGCategoryStruct.dgHom Y X).X n)} (ha : ((DGCategoryStruct.dgComp n (-n) 0 ⋯) a) s.hom = DGCategoryStruct.dgId Y) : a = s.inv

The inverse is determined by its defining equation, because right composition with s.hom is injective.

theorem CategoryTheory.IsShiftBy.comp'_inv {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) (nm : ℤ) (hnm : n + m = nm) : ((DGCategoryStruct.dgComp m n nm ⋯) u.inv) s.inv = (s.comp' u nm hnm).inv

The inverse of a composite shift is the composite of the inverses, in the other order. Proved by inv_unique rather than by unfolding: both invs are Classical.choice, so the only handle on them is their defining equation.

theorem CategoryTheory.IsShiftBy.comp_inv {C : Type u} [DGCategory C] {X Y Z : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) : ((DGCategoryStruct.dgComp m n (n + m) ⋯) u.inv) s.inv = (s.comp u).inv

The unprimed form, at the definitional degree.

theorem CategoryTheory.IsShiftBy.comp'_self_left_inv {C : Type u} [DGCategory C] {X Z : C} {m : ℤ} (u : IsShiftBy X m Z) (h : 0 + m = m) : ((self X).comp' u m h).inv = u.inv

Prefixing with the zero shift changes nothing: the composite's element is dgId ≫ u.hom, so its inverse is u's. Stated on inv rather than as an equality of IsShiftBy structures because the bijective field depends on hom, which would make a structure ext produce a HEq goal for no gain.

theorem CategoryTheory.IsShiftBy.comp'_self_right_inv {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) (h : n + 0 = n) : (s.comp' (self Y) n h).inv = s.inv

And suffixing with it: the composite's element is s.hom ≫ dgId.

noncomputable def CategoryTheory.IsShiftBy.mapShift {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : ↑((DGCategoryStruct.dgHom Y Y').X 0)

The map induced on shifts: go back along the source's shift, across, and out along the target's. compare is the case f = dgId.

This is the action on morphisms that a shift functor on H⁰ would have, and the three lemmas below are its functoriality. The functor itself is not built here: IsPretriangulated.exists_shift gives an existential rather than a choice, and HasShift additionally wants shiftFunctorZero and shiftFunctorAdd coherence.

Equations

• s.mapShift s' f = ((CategoryTheory.DGCategoryStruct.dgComp n (-n) 0 ⋯) (((CategoryTheory.DGCategoryStruct.dgComp n 0 n ⋯) s.inv) f)) s'.hom

theorem CategoryTheory.IsShiftBy.mapShift_mem_cocycles {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') {f : ↑((DGCategoryStruct.dgHom X X').X 0)} (hf : f ∈ cocycles X X') : s.mapShift s' f ∈ cocycles Y Y'

mapShift sends closed elements to closed elements, so it descends to Z⁰. All three factors are closed.

theorem CategoryTheory.IsShiftBy.mapShift_id {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : s.mapShift s (DGCategoryStruct.dgId X) = DGCategoryStruct.dgId Y

The identity is sent to the identity.

theorem CategoryTheory.IsShiftBy.mapShift_comp {C : Type u} [DGCategory C] {X X' X'' Y Y' Y'' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (s'' : IsShiftBy X'' n Y'') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) (g : ↑((DGCategoryStruct.dgHom X' X'').X 0)) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.mapShift s' f)) (s'.mapShift s'' g) = s.mapShift s'' (((DGCategoryStruct.dgComp 0 0 0 ⋯) f) g)

mapShift is compatible with composition. The middle s'.hom and s'.inv annihilate by hom_inv, which is the only place the shift's invertibility is used.

theorem CategoryTheory.IsShiftBy.compare_eq_mapShift {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X n Y') : s.compare s' = s.mapShift s' (DGCategoryStruct.dgId X)

compare is mapShift at the identity. Recorded so the two names cannot drift apart.

theorem CategoryTheory.IsShiftBy.mapShift_add {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (f g : ↑((DGCategoryStruct.dgHom X X').X 0)) : s.mapShift s' (f + g) = s.mapShift s' f + s.mapShift s' g

mapShift is additive in the morphism, because dgComp is biadditive. Needed before it can descend to H⁰, where morphisms are cosets.

theorem CategoryTheory.IsShiftBy.mapShift_mem_coboundaries {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') {f : ↑((DGCategoryStruct.dgHom X X').X 0)} (hf : f ∈ coboundaries X X') : s.mapShift s' f ∈ coboundaries Y Y'

mapShift of a coboundary is a coboundary, so it descends to H⁰.

The primitive is the obvious one, s.inv ≫ h ≫ s'.hom, and its differential picks up a single sign: s'.hom and s.inv are both closed, so of the four Leibniz terms only one survives.

Why n is replaced by m + 1 first

dgComp_leibniz states the shifted degrees as p + 1 and q + 1, and those are not free parameters. Writing the primitive's inner factor at degree n - 1 makes the rule produce n - 1 + 1, which is propositionally but not definitionally n, and the two then sit in different dgHom fibres with no rewrite available that keeps the motive type-correct.

Substituting n = m + 1 fixes it at the source: the inner factor is written at degree m, the rule produces m + 1, and that is n syntactically. The only remaining shift, -1 + 1 against 0, is definitional for integer literals and rfl closes it.

noncomputable def CategoryTheory.IsShiftBy.mapShiftHom {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') : ↑((DGCategoryStruct.dgHom X X').X 0) →+ ↑((DGCategoryStruct.dgHom Y Y').X 0)

mapShift bundled as an additive map, so that map_neg and map_sub are available when it descends to the quotient defining H⁰.

Equations

• s.mapShiftHom s' = AddMonoidHom.mk' (s.mapShift s') ⋯

@[simp]

theorem CategoryTheory.IsShiftBy.mapShiftHom_apply {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : (s.mapShiftHom s') f = s.mapShift s' f

theorem CategoryTheory.IsShiftBy.mapShift_compare {C : Type u} [DGCategory C] {X X' Y Y' Y'' Y''' : C} {n : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y'') (s' : IsShiftBy X' n Y') (t' : IsShiftBy X' n Y''') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.mapShift s' f)) (s'.compare t') = ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.compare t)) (t.mapShift t' f)

Naturality of compare, and it costs nothing: both sides are mapShift of the same morphism, by mapShift_comp and a unit law.

This is the payoff of stating IsShiftBy as representability. A shift functor on H⁰ needs its comparison isomorphisms to be natural, and here that is not a diagram to chase -- it is f ≫ 𝟙 = 𝟙 ≫ f transported through one lemma.

theorem CategoryTheory.IsShiftBy.self_inv {C : Type u} [DGCategory C] (X : C) : (self X).inv = DGCategoryStruct.dgId X

The zero shift's inverse is the identity. Forced, not chosen: inv is Classical.choice on a surjectivity, but inv_hom pins it down.

theorem CategoryTheory.IsShiftBy.mapShift_self {C : Type u} [DGCategory C] (X X' : C) (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : (self X).mapShift (self X') f = f

mapShift along the zero shift is the identity on morphisms. This is what makes shiftFunctor 0 naturally isomorphic to the identity functor.

theorem CategoryTheory.IsShiftBy.mapShift_unique {C : Type u} [DGCategory C] {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) (c : ↑((DGCategoryStruct.dgHom Y Y').X 0)) (h : ((DGCategoryStruct.dgComp (-n) 0 (-n) ⋯) s.hom) c = ((DGCategoryStruct.dgComp 0 (-n) (-n) ⋯) f) s'.hom) : s.mapShift s' f = c

mapShift is determined by the square it makes commute. An element c of degree zero with s.hom ≫ c = f ≫ s'.hom is mapShift s s' f.

mapShift is built from s.inv, which is Classical.choice, so nothing about it can be unfolded. What can be used is that left composition with s.hom is injective -- s.inv is a left inverse for it by inv_hom -- and the defining square is exactly what that injectivity reads off. Every identification of mapShift with a concretely given morphism goes through here.

theorem CategoryTheory.IsShiftBy.compare_unique {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} {Y' : C} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') (c : ↑((DGCategoryStruct.dgHom Y Y').X 0)) (h : ((DGCategoryStruct.dgComp (-n) 0 (-n) ⋯) s.hom) c = t.hom) : s.compare t = c

compare is mapShift at the identity, so it too is determined by its defining square.

theorem CategoryTheory.IsShiftBy.mapShift_comp'_shift {C : Type u} [DGCategory C] {X X' Y Y' Z Z' : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) (s' : IsShiftBy X' n Y') (u' : IsShiftBy Y' m Z') (nm : ℤ) (hnm : n + m = nm) (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : (s.comp' u nm hnm).mapShift (s'.comp' u' nm hnm) f = u.mapShift u' (s.mapShift s' f)

mapShift along a composite shift is mapShift twice. Everything in sight is a composite of the same five factors; the proof is four applications of dgComp_assoc moving the brackets from one side's shape to the other's.

This is the naturality obligation of shiftFunctorAdd in disguise, and it is where comp_inv is needed: the composite shift's inverse has to be recognised as the composite of the inverses before either side can be reassociated.

theorem CategoryTheory.IsShiftBy.mapShift_comp_shift {C : Type u} [DGCategory C] {X X' Y Y' Z Z' : C} {n m : ℤ} (s : IsShiftBy X n Y) (u : IsShiftBy Y m Z) (s' : IsShiftBy X' n Y') (u' : IsShiftBy Y' m Z') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : (s.comp u).mapShift (s'.comp u') f = u.mapShift u' (s.mapShift s' f)

The unprimed form, at the definitional degree.

theorem CategoryTheory.IsShiftBy.mapShift_compare_comp' {C : Type u} [DGCategory C] {X Y Y' Z Z' : C} {n m : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') (u : IsShiftBy Y m Z) (u' : IsShiftBy Y' m Z') (nm : ℤ) (hnm : n + m = nm) : u.mapShift u' (s.compare t) = (s.comp' u nm hnm).compare (t.comp' u' nm hnm)

Shifting a comparison is the comparison of the composites. This is mapShift_comp_shift at the identity, and it is what lets the coherence statements for the shift functor be read entirely in terms of compare.

theorem CategoryTheory.IsShiftBy.mapShift_compare_comp {C : Type u} [DGCategory C] {X Y Y' Z Z' : C} {n m : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') (u : IsShiftBy Y m Z) (u' : IsShiftBy Y' m Z') : u.mapShift u' (s.compare t) = (s.comp u).compare (t.comp u')

The unprimed form, at the definitional degree.

theorem CategoryTheory.IsShiftBy.compare_congr {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (t t' : IsShiftBy X n Y') (h : t.hom = t'.hom) : s.compare t = s.compare t'

compare s t reads t only through t.hom, so two witnesses with the same element compare the same way. This is the whole of what the associativity coherence needs, once both sides are reduced to a single comparison.

theorem CategoryTheory.IsShiftBy.compare_congr_left {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s s' : IsShiftBy X n Y) (t : IsShiftBy X n Y') (h : s.hom = s'.hom) : s.compare t = s'.compare t

compare also reads its source witness only through its closed element.

theorem CategoryTheory.IsShiftBy.comp'_assoc_hom {C : Type u} [DGCategory C] {W X Y Z : C} {a b d : ℤ} (s : IsShiftBy X a Y) (u : IsShiftBy Y b Z) (w : IsShiftBy Z d W) (ab bd abd : ℤ) (hab : a + b = ab) (hbd : b + d = bd) (habd : ab + d = abd) : ((s.comp' u ab hab).comp' w abd habd).hom = (s.comp' (u.comp' w bd hbd) abd ⋯).hom

The two bracketings of a threefold composite shift carry the same element. This is dgComp_assoc on the three homs, and nothing more -- which is why the associativity coherence is not a diagram chase either.

theorem CategoryTheory.IsShiftBy.compare_comp'_right {C : Type u} [DGCategory C] {X Y Z Y' Z' : C} {a b k : ℤ} (s : IsShiftBy X k Y') (t : IsShiftBy X a Y) (v : IsShiftBy Y b Z) (v' : IsShiftBy Y b Z') (hk : a + b = k) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (s.compare (t.comp' v k hk))) (v.compare v') = s.compare (t.comp' v' k hk)

Composing a comparison-into-a-composite with a comparison of the composite's second factor replaces that factor. The middle v.hom ≫ v.inv collapses by hom_inv, which is the only step with content.

theorem CategoryTheory.IsConeOf.comp_inr_mem_coboundaries {C : Type u} [DGCategory C] {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) f) hc.inr ∈ coboundaries X Z

The composite X ⟶ Y ⟶ Cone f is a coboundary: inl is its primitive. This is the whole content of δ_inl, restated so that H⁰ can read it, and it is what makes the cone sequence a triangle in dg-enhancements-e6.

theorem CategoryTheory.IsConeOf.inr_mem_cocycles {C : Type u} [DGCategory C] {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : hc.inr ∈ cocycles Y Z

inr is a cocycle, so it is a morphism of Z⁰.

class CategoryTheory.IsPretriangulated (C : Type u) [DGCategory C] : Prop

A strongly pretriangulated dg category: it has a zero object, a shift in every degree, and a cone on every closed degree-zero morphism, each represented strictly rather than up to homotopy equivalence.

The name is the short one for readability; see the module docstring on why this is Drinfeld's strong notion and not Bondal--Kapranov's.

• exists_zero : ∃ (Z : C), DGCategoryStruct.dgId Z = 0

  Some object has zero identity, so Z⁰ C and H⁰ C have a zero object.

• exists_shift (X : C) (n : ℤ) : ∃ (Y : C), Nonempty (IsShiftBy X n Y)

  Every object has a shift in every degree.

• exists_cone {X Y : C} (f : ↑((DGCategoryStruct.dgHom X Y).X 0)) (hf : f ∈ cocycles X Y) : ∃ (Z : C), Nonempty (IsConeOf f Z)

  Every closed degree-zero morphism has a cone.