Shifts of finite sums of shifted objects

Let C be a differential graded category. The shift X[r] ↦ X[r + n] of the shift closure of C (TauCeti.DGShiftClosure.shiftFunctor) induces a DG functor on the additive closure of the shift closure, sending ⊕ᵢ Xᵢ[rᵢ] to ⊕ᵢ Xᵢ[rᵢ + n] and leaving every matrix entry unchanged as a morphism of C.

The summandwise comparison morphisms Xᵢ[rᵢ] ⟶ Xᵢ[rᵢ + n] of the shift closure (TauCeti.DGShiftClosure.toShift), whose underlying morphisms are (-1)^(n * rᵢ) times the identity, assemble into the diagonal matrix TauCeti.DGAdditiveClosure.toShift of degree -n from ⊕ᵢ Xᵢ[rᵢ] to ⊕ᵢ Xᵢ[rᵢ + n]. It is closed, has the diagonal matrix TauCeti.DGAdditiveClosure.fromShift of degree n as its inverse, and is natural up to the Koszul sign, f ≫ σ_N = (-1)^(n * p) • σ_M ≫ f⟦n⟧ for f of degree p. These are the comparison morphisms of shifts of twisted objects (see TauCeti/CategoryTheory/DG/Twisted/Shift.lean).

A DG functor F : C ⥤ D induces a DG functor between the additive closures of the shift closures, sending ⊕ᵢ Xᵢ[rᵢ] to ⊕ᵢ (F Xᵢ)[rᵢ]. It commutes with shifting every summand and preserves the comparison morphisms, since it is applied entrywise and preserves identities.

Main definitions

• TauCeti.DGAdditiveClosure.toShift and TauCeti.DGAdditiveClosure.fromShift: the diagonal comparison matrices ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] of degree -n and ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] of degree n.

Main results

• TauCeti.DGAdditiveClosure.dgDifferential_toShift and TauCeti.DGAdditiveClosure.dgDifferential_fromShift: the comparison morphisms are closed.
• TauCeti.DGAdditiveClosure.dgComp_toShift_fromShift and TauCeti.DGAdditiveClosure.dgComp_fromShift_toShift: they are mutually inverse.
• TauCeti.DGAdditiveClosure.dgComp_toShift and TauCeti.DGAdditiveClosure.dgComp_fromShift: they are natural up to the Koszul sign.
• CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_shiftFunctor, CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_toShift and CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_fromShift: the DG functor induced by a DG functor commutes with the shifts and preserves the comparison morphisms.

References

• A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.4.

noncomputable def TauCeti.DGAdditiveClosure.toShift (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : DGHom R (-n) M ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M)

The comparison morphism ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] of degree -n: the diagonal matrix of the comparison morphisms TauCeti.DGShiftClosure.toShift of the summands.

noncomputable def TauCeti.DGAdditiveClosure.fromShift (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : DGHom R n ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M) M

The comparison morphism ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] of degree n: the diagonal matrix of the inverse comparison morphisms TauCeti.DGShiftClosure.fromShift of the summands.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_toShift_self {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) (i : M.ι) : (dgHomEquiv R M ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M) (-n)) (toShift R M n) i i = DGShiftClosure.toShift R (M.X i) n

The diagonal entries of ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] are the comparison morphisms of the summands.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_toShift_of_ne {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) {i j : M.ι} (h : i ≠ j) : (dgHomEquiv R M ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M) (-n)) (toShift R M n) i j = 0

The off-diagonal entries of ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] vanish.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_fromShift_self {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) (i : M.ι) : (dgHomEquiv R ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M) M n) (fromShift R M n) i i = DGShiftClosure.fromShift R (M.X i) n

The diagonal entries of ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] are the inverse comparison morphisms of the summands.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_fromShift_of_ne {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) {i j : M.ι} (h : i ≠ j) : (dgHomEquiv R ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M) M n) (fromShift R M n) i j = 0

The off-diagonal entries of ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] vanish.

theorem TauCeti.DGAdditiveClosure.dgComp_toShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {M N : DGAdditiveClosure (DGShiftClosure C)} (n : ℤ) {p m : ℤ} (f : DGHom R p M N) (h : p + -n = m) : dgComp R f (toShift R N n) h = (n * p).negOnePow • dgComp R (toShift R M n) (((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.dgMap p) f) ⋯

The comparison morphisms are natural up to the Koszul sign: for f : M ⟶ N of degree p, f followed by N ⟶ N⟦n⟧ is (-1)^(n * p) times M ⟶ M⟦n⟧ followed by the shift of f.

theorem TauCeti.DGAdditiveClosure.dgComp_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {M N : DGAdditiveClosure (DGShiftClosure C)} (n : ℤ) {p m : ℤ} (f : DGHom R p M N) (h : p + n = m) : dgComp R (((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.dgMap p) f) (fromShift R N n) h = (n * p).negOnePow • dgComp R (fromShift R M n) f ⋯

The inverse comparison morphisms are natural up to the Koszul sign: for f : M ⟶ N of degree p, the shift of f followed by N⟦n⟧ ⟶ N is (-1)^(n * p) times M⟦n⟧ ⟶ M followed by f.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgDifferential_toShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : (dgDifferential R (-n)) (toShift R M n) = 0

The comparison morphism ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] is closed, as a diagonal matrix of closed morphisms.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgComp_toShift_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : dgComp R (toShift R M n) (fromShift R M n) ⋯ = dgId R M

The comparison morphisms ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] compose to the identity.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgComp_fromShift_toShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : dgComp R (fromShift R M n) (toShift R M n) ⋯ = dgId R ((DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.obj M)

The comparison morphisms ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] compose to the identity.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgDifferential_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure (DGShiftClosure C)) (n : ℤ) : (dgDifferential R n) (fromShift R M n) = 0

The comparison morphism ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] is closed, as the inverse of a closed morphism.

Functoriality

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_shiftFunctor {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (n : ℤ) {M N : TauCeti.DGAdditiveClosure (TauCeti.DGShiftClosure C)} {p : ℤ} (f : TauCeti.DGHom R p M N) : (F.mapDGShiftClosure.mapDGAdditiveClosure.dgMap p) (((TauCeti.DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.dgMap p) f) = ((TauCeti.DGShiftClosure.shiftFunctor R n).mapDGAdditiveClosure.dgMap p) ((F.mapDGShiftClosure.mapDGAdditiveClosure.dgMap p) f)

The DG functor induced by F on additive closures of shift closures commutes with shifting every summand: a matrix of morphisms has the same image under the two composites.

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_toShift {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (M : TauCeti.DGAdditiveClosure (TauCeti.DGShiftClosure C)) (n : ℤ) : (F.mapDGShiftClosure.mapDGAdditiveClosure.dgMap (-n)) (TauCeti.DGAdditiveClosure.toShift R M n) = TauCeti.DGAdditiveClosure.toShift R (F.mapDGShiftClosure.mapDGAdditiveClosure.obj M) n

The DG functor induced by F sends the comparison morphism ⊕ᵢ Xᵢ[rᵢ] ⟶ ⊕ᵢ Xᵢ[rᵢ + n] to the comparison morphism of the image.

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosure_mapDGAdditiveClosure_dgMap_fromShift {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (M : TauCeti.DGAdditiveClosure (TauCeti.DGShiftClosure C)) (n : ℤ) : (F.mapDGShiftClosure.mapDGAdditiveClosure.dgMap n) (TauCeti.DGAdditiveClosure.fromShift R M n) = TauCeti.DGAdditiveClosure.fromShift R (F.mapDGShiftClosure.mapDGAdditiveClosure.obj M) n

The DG functor induced by F sends the comparison morphism ⊕ᵢ Xᵢ[rᵢ + n] ⟶ ⊕ᵢ Xᵢ[rᵢ] to the comparison morphism of the image.