Shifted hom-complexes

For a dg category C, each hom-complex dgHom X Y can be shifted by m : ℤ using Mathlib's shift on CochainComplex. This file records what survives that shift: the differential picks up (-1) ^ m, and composition still satisfies Leibniz, associativity, and the unit laws — provided it picks up a Koszul sign.

This is the shift dg-enhancements-e2's summary claimed to deliver and did not; dg-enhancements-e5 (#376) owns it, and the roadmap is corrected alongside.

The sign is derived, not chosen

Mathlib's CochainComplex.shiftFunctor m sends K to the complex that is K.X (i + m) in degree i, with differential m.negOnePow • K.d _ _ (shiftFunctor_obj_X', shiftFunctor_obj_d', both rfl at the pin). Take f of shifted degree p in (dgHom X Y)⟦m⟧ and g of shifted degree q in (dgHom Y Z)⟦n⟧, and ask for a composition ε • dgComp making the Leibniz rule of DGCategory hold verbatim in the shifted complexes. Matching the two terms separately forces

• ε (p, q + 1) = (-1) ^ m * ε (p, q), from the term carrying δ g;
• ε (p + 1, q) = ε (p, q), from the term carrying δ f.

So ε cannot depend on p, and ε = (-1) ^ (q * m) is the solution. The sign is the degree of the element that moves times the shift it moves past, which is the Koszul rule — but it is written here as the conclusion of the two matching conditions rather than as an appeal to that rule.

Associativity and the unit laws are then automatic rather than further constraints; shiftComp_assoc and the two dgId lemmas below confirm this.

Raw degrees, not shifted ones

Every degree argument below is the degree in the underlying hom-complex, and the shift enters only through the sign. Writing shiftComp on shifted degrees instead — with hom-types like (dgHom X Y).X (p + m) — costs a rewrite between (q + 1) + n and (q + n) + 1 in the Leibniz proof, and rewriting an index of HomologicalComplex.X breaks the motive. On raw degrees the statement has the same shape as dgComp itself: three degrees and one equation. The shifted degree is recovered as b - n, which is where the sign's b - n comes from.

def CategoryTheory.DGCategory.shiftD {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (a b : ℤ) : ↑((DGCategoryStruct.dgHom X Y).X a) →+ ↑((DGCategoryStruct.dgHom X Y).X b)

The differential of the m-shifted hom-complex, at raw degrees.

Equations

• CategoryTheory.DGCategory.shiftD m a b = m.negOnePow • AddCommGrpCat.Hom.hom ((CategoryTheory.DGCategoryStruct.dgHom X Y).d a b)

def CategoryTheory.DGCategory.shiftComp {C : Type u} [DGCategory C] (m n : ℤ) {X Y Z : C} (a b c : ℤ) (h : a + b = c) : ↑((DGCategoryStruct.dgHom X Y).X a) →+ ↑((DGCategoryStruct.dgHom Y Z).X b) →+ ↑((DGCategoryStruct.dgHom X Z).X c)

Composition of shifted hom-complexes: dgComp with the Koszul sign that the two Leibniz matching conditions force. m and n are the shifts of the source and middle hom-complexes; b - n is the degree of the second argument in the shifted complex.

Equations

• CategoryTheory.DGCategory.shiftComp m n a b c h = ((b - n) * m).negOnePow • CategoryTheory.DGCategoryStruct.dgComp a b c h

theorem CategoryTheory.DGCategory.shiftD_apply {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (a b : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X a)) : (shiftD m a b) f = m.negOnePow • (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d a b)) f

shiftD applied to an element, unfolded.

theorem CategoryTheory.DGCategory.shiftComp_apply {C : Type u} [DGCategory C] (m n : ℤ) {X Y Z : C} (a b c : ℤ) (h : a + b = c) (f : ↑((DGCategoryStruct.dgHom X Y).X a)) (g : ↑((DGCategoryStruct.dgHom Y Z).X b)) : ((shiftComp m n a b c h) f) g = ((b - n) * m).negOnePow • ((DGCategoryStruct.dgComp a b c h) f) g

shiftComp applied to a pair of elements, unfolded.

theorem CategoryTheory.DGCategory.shiftComp_zero_zero {C : Type u} [DGCategory C] {X Y Z : C} (a b c : ℤ) (h : a + b = c) : shiftComp 0 0 a b c h = DGCategoryStruct.dgComp a b c h

The unshifted case is the original composition, on the nose.

theorem CategoryTheory.DGCategory.shiftD_zero {C : Type u} [DGCategory C] {X Y : C} (a b : ℤ) : shiftD 0 a b = AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d a b)

The unshifted differential is the original differential.

The tie-back to Mathlib's shift

shiftD and the shifted hom-types are not a private convention: they are what CochainComplex.shiftFunctor already does, and both lemmas below are rfl.

theorem CategoryTheory.DGCategory.shiftFunctor_dgHom_X {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (p : ℤ) : ((shiftFunctor (CochainComplex AddCommGrpCat ℤ) m).obj (DGCategoryStruct.dgHom X Y)).X p = (DGCategoryStruct.dgHom X Y).X (p + m)

Degree p of the m-shifted hom-complex is degree p + m of the original. This is CochainComplex.shiftFunctor's own indexing, so the lemma is rfl.

theorem CategoryTheory.DGCategory.shiftFunctor_dgHom_d {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (p p' : ℤ) : AddCommGrpCat.Hom.hom (((shiftFunctor (CochainComplex AddCommGrpCat ℤ) m).obj (DGCategoryStruct.dgHom X Y)).d p p') = shiftD m (p + m) (p' + m)

shiftD is the differential of the shifted hom-complex, not a lookalike: the lemma is rfl, so the (-1) ^ m in shiftD is Mathlib's sign rather than a convention this file introduces.

The four laws

theorem CategoryTheory.DGCategory.shiftComp_leibniz {C : Type u} [DGCategory C] (m n : ℤ) {X Y Z : C} (a b c c' : ℤ) (h : a + b = c) (hc : c + 1 = c') (f : ↑((DGCategoryStruct.dgHom X Y).X a)) (g : ↑((DGCategoryStruct.dgHom Y Z).X b)) : (shiftD (m + n) c c') (((shiftComp m n a b c h) f) g) = ((shiftComp m n a (b + 1) c' ⋯) f) ((shiftD n b (b + 1)) g) + (b - n).negOnePow • ((shiftComp m n (a + 1) b c' ⋯) ((shiftD m a (a + 1)) f)) g

The Leibniz rule survives the shift, in the same shape as the axiom: the sign on the second term is the degree of the first argument's partner in the shifted complex, b - n. This is the lemma the sign was solved for.

theorem CategoryTheory.DGCategory.shiftComp_assoc {C : Type u} [DGCategory C] (m n l : ℤ) {W X Y Z : C} (a b d ab bd abd : ℤ) (hab : a + b = ab) (hbd : b + d = bd) (habd : ab + d = abd) (f : ↑((DGCategoryStruct.dgHom W X).X a)) (g : ↑((DGCategoryStruct.dgHom X Y).X b)) (k : ↑((DGCategoryStruct.dgHom Y Z).X d)) : ((shiftComp (m + n) l ab d abd habd) (((shiftComp m n a b ab hab) f) g)) k = ((shiftComp m (n + l) a bd abd ⋯) f) (((shiftComp n l b d bd hbd) g) k)

Associativity survives the shift with no further sign condition: the two sides carry (b - n) * m + (d - l) * (m + n) and (d - l) * n + (b + d - (n + l)) * m, which are equal as integers.

theorem CategoryTheory.DGCategory.shiftComp_dgId_left {C : Type u} [DGCategory C] (n : ℤ) {X Y : C} (b : ℤ) (g : ↑((DGCategoryStruct.dgHom X Y).X b)) : ((shiftComp 0 n 0 b b ⋯) (DGCategoryStruct.dgId X)) g = g

The identity is a left unit for the shifted composition. Its hom-complex is unshifted, so the sign is ((b - n) * 0) and vanishes.

theorem CategoryTheory.DGCategory.shiftComp_dgId_right {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (a : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X a)) : ((shiftComp m 0 a 0 a ⋯) f) (DGCategoryStruct.dgId Y) = f

The identity is a right unit for the shifted composition. It sits in degree 0 of an unshifted complex, so the sign is ((0 - 0) * m) and vanishes.

theorem CategoryTheory.DGCategory.shiftD_shiftD {C : Type u} [DGCategory C] (m : ℤ) {X Y : C} (a b c : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X a)) : (shiftD m b c) ((shiftD m a b) f) = 0

The shifted differential still squares to zero: the two signs cancel. No hypothesis relates a, b, c — off the diagonal d is zero by shape, so the statement holds for every triple.