The shift closure of a differential graded category

For a differential graded category C, the shift closure TauCeti.DGShiftClosure C adjoins a formal shift X[r] of every object X by every integer r. Its Hom complexes are shifts of those of C:

Hom(X[r], Y[s]) = Hom(X, Y)[s - r],

with Mathlib's cochain-shift convention K[a]^p = K^(p + a) and differential (-1)^a d_K. So a morphism X[r] ⟶ Y[s] of degree p is a morphism X ⟶ Y of degree p + s - r (TauCeti.DGShiftClosure.dgHomEquiv), and the differential of the shift closure is (-1)^(s - r) times the differential of C.

Composition carries a sign. In Mathlib's enriched factor order, a degree-p morphism f : X[r] ⟶ Y[s] followed by g : Y[s] ⟶ Z[t] composes to (-1)^((t - s) * (p + s - r)) • dgComp f g. In Keller's order, where g ∘ f = (-1)^(p * q) • dgComp f g for g of degree q, the sign becomes (-1)^((s - r) * q). These are the signs for which the formal shifts of cochain complexes are Mathlib's shifted complexes K⟦r⟧, with Hom(K, L)[s - r] ≅ Hom(K⟦r⟧, L⟦s⟧) multiplying the underlying cochain by (-1)^(r * p): see TauCeti/CategoryTheory/DG/ShiftClosure/CochainComplex.lean.

Shifting every object by the same integer n does not change the Hom complexes, so X[r] ↦ X[r + n] is a DG functor TauCeti.DGShiftClosure.shiftFunctor n which is the identity on underlying morphisms of C. The objects X[r] and X[r + n] are related by the closed morphism TauCeti.DGShiftClosure.toShift : X[r] ⟶ X[r + n] of degree -n and its inverse TauCeti.DGShiftClosure.fromShift of degree n, whose underlying morphisms are (-1)^(n * r) times the identity of X. With this sign, toShift is natural up to the Koszul sign: f ≫ toShift = (-1)^(n * p) • toShift ≫ f[n] for f of degree p, and so is fromShift.

A DG functor F : C ⥤ D induces a DG functor F.mapDGShiftClosure between the shift closures, sending X[r] to (F X)[r] and applying F to the underlying morphisms; it commutes with the shifts and preserves the comparison morphisms.

The shift closure is the home of the matrix entries of one-sided twisted complexes, the objects (⊕ᵢ Xᵢ[rᵢ], δ) of the pretriangulated envelope of Bondal and Kapranov.

Main definitions

• TauCeti.DGShiftClosure: the objects X[r] of the shift closure.
• TauCeti.DGShiftClosure.homComplexData: its explicit Hom-complex data.
• TauCeti.DGShiftClosure.dgHomEquiv: degree-n morphisms X[r] ⟶ Y[s] are degree-n + s - r morphisms X ⟶ Y.
• TauCeti.DGShiftClosure.ι: the DG functor X ↦ X[0].
• TauCeti.DGShiftClosure.shiftFunctor: the DG functor X[r] ↦ X[r + n].
• TauCeti.DGShiftClosure.toShift and TauCeti.DGShiftClosure.fromShift: the closed comparison morphisms X[r] ⟶ X[r + n] of degree -n and X[r + n] ⟶ X[r] of degree n.
• CategoryTheory.EnrichedFunctor.mapDGShiftClosure: the DG functor X[r] ↦ (F X)[r] induced by a DG functor F.

Main results

• TauCeti.DGShiftClosure.dgHomEquiv_dgDifferential: the differential is (-1)^(s - r) d.
• TauCeti.DGShiftClosure.dgHomEquiv_dgComp: composition carries the sign (-1)^((t - s) * (p + s - r)).
• TauCeti.DGShiftClosure.dgHomEquiv_negOnePow_smul_dgComp: in Keller's order the sign is (-1)^((s - r) * q).
• TauCeti.DGShiftClosure.dgHomEquiv_dgId: the identity of X[r] is the identity of X.
• TauCeti.DGShiftClosure.isIso_ι_map: X ↦ X[0] is an isomorphism on Hom complexes.
• TauCeti.DGShiftClosure.dgComp_toShift_fromShift and TauCeti.DGShiftClosure.dgComp_fromShift_toShift: the comparison morphisms are mutually inverse.
• TauCeti.DGShiftClosure.dgComp_toShift and TauCeti.DGShiftClosure.dgComp_fromShift: the comparison morphisms are natural up to the Koszul sign.
• CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_shiftHomEquiv, CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_toShift and CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_fromShift: the DG functor induced by F commutes with shifting every object 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.
• B. Keller, Deriving DG categories, Section 1.

structure TauCeti.DGShiftClosure (C : Type u) : Type u

The objects of the shift closure of a differential graded category on the objects C: an object X of C together with an integer r, standing for the formal shift X[r]. The Hom complexes are Hom(X[r], Y[s]) = Hom(X, Y)[s - r]; see TauCeti.DGShiftClosure.homComplexData.

• obj : C

  The underlying object X of the shifted object X[r].

• shift : ℤ

  The shift r of the shifted object X[r].

theorem TauCeti.DGShiftClosure.ext_iff {C : Type u} {x y : DGShiftClosure C} : x = y ↔ x.obj = y.obj ∧ x.shift = y.shift

theorem TauCeti.DGShiftClosure.ext {C : Type u} {x y : DGShiftClosure C} (obj : x.obj = y.obj) (shift : x.shift = y.shift) : x = y

The Hom-complex data

noncomputable def TauCeti.DGShiftClosure.homComplexData (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : DGCategoryData R (DGShiftClosure C)

The explicit Hom-complex data of the shift closure: Hom(X[r], Y[s]) = Hom(X, Y)[s - r], whose differential is (-1)^(s - r) d, with composition the composition of C multiplied by (-1)^((t - s) * (p + s - r)) and identity the identity of C.

@[instance_reducible]

noncomputable instance TauCeti.DGShiftClosure.instDGCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : DGCategory R (DGShiftClosure C)

The shift closure of a differential graded category: the objects X[r], with Hom complexes Hom(X[r], Y[s]) = Hom(X, Y)[s - r].

Morphisms, differential, composition and identity

theorem TauCeti.DGShiftClosure.dgHomComplex_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : DGShiftClosure C) : dgHomComplex R X Y = dgHomComplex R X.obj Y.obj⟦Y.shift - X.shift⟧

The Hom complex Hom(X[r], Y[s]) of the shift closure is the shifted Hom complex Hom(X, Y)[s - r].

noncomputable def TauCeti.DGShiftClosure.dgHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : DGShiftClosure C) (n : ℤ) : DGHom R n X Y ≃ₗ[R] DGHom R (n + (Y.shift - X.shift)) X.obj Y.obj

A morphism X[r] ⟶ Y[s] of degree n in the shift closure is a morphism X ⟶ Y of degree n + (s - r) in C.

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : DGShiftClosure C} (n : ℤ) (f : DGHom R n X Y) : (dgHomEquiv R X Y (n + 1)) ((dgDifferential R n) f) = (Y.shift - X.shift).negOnePow • (ModuleCat.Hom.hom ((dgHomComplex R X.obj Y.obj).d (n + (Y.shift - X.shift)) (n + 1 + (Y.shift - X.shift)))) ((dgHomEquiv R X Y n) f)

The differential of the shift closure is (-1)^(s - r) times the differential of C.

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : DGShiftClosure C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : (dgHomEquiv R X Z n) (dgComp R f g h) = ((Z.shift - Y.shift) * (p + (Y.shift - X.shift))).negOnePow • dgComp R ((dgHomEquiv R X Y p) f) ((dgHomEquiv R Y Z q) g) ⋯

Composition in the shift closure: a degree-p morphism f : X[r] ⟶ Y[s] followed by g : Y[s] ⟶ Z[t] is the composite of the underlying morphisms of C, with the sign (-1)^((t - s) * (p + s - r)).

theorem TauCeti.DGShiftClosure.dgHomEquiv_negOnePow_smul_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : DGShiftClosure C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : (dgHomEquiv R X Z n) ((p * q).negOnePow • dgComp R f g h) = ((Y.shift - X.shift) * q).negOnePow • ((p + (Y.shift - X.shift)) * (q + (Z.shift - Y.shift))).negOnePow • dgComp R ((dgHomEquiv R X Y p) f) ((dgHomEquiv R Y Z q) g) ⋯

The shift-closure composition sign in Keller's order: for f : X[r] ⟶ Y[s] of degree p and g : Y[s] ⟶ Z[t] of degree q, the Keller-ordered composite g ∘ f = (-1)^(p * q) • dgComp f g is the Keller-ordered composite of the underlying morphisms of C, of degrees p + s - r and q + t - s, multiplied by (-1)^((s - r) * q).

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGShiftClosure C) : (dgHomEquiv R X X 0) (dgId R X) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq (dgHomComplex R X.obj X.obj) ⋯).hom) (dgId R X.obj)

The identity of X[r] in the shift closure is the identity of X.

The inclusion X ↦ X[0]

noncomputable def TauCeti.DGShiftClosure.ιHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) (n : ℤ) : DGHom R n X Y ≃ₗ[R] DGHom R n { obj := X, shift := 0 } { obj := Y, shift := 0 }

The action of the inclusion X ↦ X[0] on morphisms of degree n: a degree-n morphism X ⟶ Y of C is a degree-n morphism X[0] ⟶ Y[0] of the shift closure.

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_ιHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) : (dgHomEquiv R { obj := X, shift := 0 } { obj := Y, shift := 0 } n) ((ιHomEquiv R X Y n) f) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq (dgHomComplex R X Y) ⋯).hom) f

The inclusion X ↦ X[0] does not change the underlying morphism.

noncomputable def TauCeti.DGShiftClosure.ι (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C (DGShiftClosure C)

The DG functor X ↦ X[0] from a differential graded category to its shift closure.

@[simp]

theorem TauCeti.DGShiftClosure.ι_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (ι R).obj X = { obj := X, shift := 0 }

The inclusion sends X to X[0].

theorem TauCeti.DGShiftClosure.dgMap_ι (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) : ((ι R).dgMap n) f = (ιHomEquiv R X Y n) f

The inclusion acts on morphisms by TauCeti.DGShiftClosure.ιHomEquiv.

instance TauCeti.DGShiftClosure.isIso_ι_map (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : CategoryTheory.IsIso ((ι R).map X Y)

The inclusion X ↦ X[0] is an isomorphism on Hom complexes: C is a full DG subcategory of its shift closure.

Shifting every object

noncomputable def TauCeti.DGShiftClosure.shiftHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : DGShiftClosure C) (n p : ℤ) : DGHom R p X Y ≃ₗ[R] DGHom R p { obj := X.obj, shift := X.shift + n } { obj := Y.obj, shift := Y.shift + n }

Shifting both objects by n does not change the morphisms: a degree-p morphism X[r] ⟶ Y[s] and a degree-p morphism X[r + n] ⟶ Y[s + n] are both morphisms X ⟶ Y of degree p + (s - r).

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_shiftHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : DGShiftClosure C} {n p : ℤ} (f : DGHom R p X Y) : (dgHomEquiv R { obj := X.obj, shift := X.shift + n } { obj := Y.obj, shift := Y.shift + n } p) ((shiftHomEquiv R X Y n p) f) = (castDeg R ⋯) ((dgHomEquiv R X Y p) f)

Shifting both objects does not change the underlying morphism of C.

theorem TauCeti.DGShiftClosure.shiftHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : DGShiftClosure C} (n p : ℤ) (f : DGHom R p X Y) : (shiftHomEquiv R X Y n (p + 1)) ((dgDifferential R p) f) = (dgDifferential R p) ((shiftHomEquiv R X Y n p) f)

Shifting both objects commutes with the differential: both differentials are (-1)^(s - r) times the differential of C.

theorem TauCeti.DGShiftClosure.shiftHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGShiftClosure C) (n : ℤ) : (shiftHomEquiv R X X n 0) (dgId R X) = dgId R { obj := X.obj, shift := X.shift + n }

Shifting both objects preserves identities.

theorem TauCeti.DGShiftClosure.shiftHomEquiv_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : DGShiftClosure C} (n : ℤ) {p q m : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = m) : (shiftHomEquiv R X Z n m) (dgComp R f g h) = dgComp R ((shiftHomEquiv R X Y n p) f) ((shiftHomEquiv R Y Z n q) g) h

Shifting both objects preserves composition: the composition signs (-1)^((t - s) * (p + s - r)) do not change when r, s and t are shifted by the same integer.

@[reducible, inline]

noncomputable abbrev TauCeti.DGShiftClosure.shiftFunctor (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) (DGShiftClosure C) (DGShiftClosure C)

The DG functor shifting every object of the shift closure by n, X[r] ↦ X[r + n]. It does not change the underlying morphisms of C (TauCeti.DGShiftClosure.shiftHomEquiv).

@[simp]

theorem TauCeti.DGShiftClosure.dgMap_shiftFunctor (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) {X Y : DGShiftClosure C} {p : ℤ} (f : DGHom R p X Y) : ((shiftFunctor R n).dgMap p) f = (shiftHomEquiv R X Y n p) f

The shift by n acts on morphisms by TauCeti.DGShiftClosure.shiftHomEquiv.

instance TauCeti.DGShiftClosure.isIso_shiftFunctor_map (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) (X Y : DGShiftClosure C) : CategoryTheory.IsIso ((shiftFunctor R n).map X Y)

The shift is an isomorphism on Hom complexes.

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

The comparison morphism X[r] ⟶ X[r + n] of degree -n, whose underlying morphism is (-1)^(n * r) times the identity of X.

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

The comparison morphism X[r + n] ⟶ X[r] of degree n, whose underlying morphism is (-1)^(n * r) times the identity of X.

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_toShift (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGShiftClosure C) (n : ℤ) : (dgHomEquiv R X ((shiftFunctor R n).obj X) (-n)) (toShift R X n) = (n * X.shift).negOnePow • (castDeg R ⋯) (dgId R X.obj)

The underlying morphism of X[r] ⟶ X[r + n] is (-1)^(n * r) times the identity of X.

@[simp]

theorem TauCeti.DGShiftClosure.dgHomEquiv_fromShift (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGShiftClosure C) (n : ℤ) : (dgHomEquiv R ((shiftFunctor R n).obj X) X n) (fromShift R X n) = (n * X.shift).negOnePow • (castDeg R ⋯) (dgId R X.obj)

The underlying morphism of X[r + n] ⟶ X[r] is (-1)^(n * r) times the identity of X.

@[simp]

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

The comparison morphism X[r] ⟶ X[r + n] is closed.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

The comparison morphism X[r + n] ⟶ X[r] is closed.

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

The comparison morphisms are natural up to the Koszul sign: for f : X[r] ⟶ Y[s] of degree p, f followed by Y[s] ⟶ Y[s + n] is (-1)^(n * p) times X[r] ⟶ X[r + n] followed by the shift of f.

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

The inverse comparison morphisms are natural up to the Koszul sign: for f : X[r] ⟶ Y[s] of degree p, the shift of f followed by Y[s + n] ⟶ Y[s] is (-1)^(n * p) times X[r + n] ⟶ X[r] followed by f.

Functoriality

noncomputable def CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom {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) (X Y : TauCeti.DGShiftClosure C) (n : ℤ) : TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n { obj := F.obj X.obj, shift := X.shift } { obj := F.obj Y.obj, shift := Y.shift }

The action of a DG functor on morphisms X[r] ⟶ Y[s] of degree n: its action on the underlying morphisms X ⟶ Y of degree n + (s - r).

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgHomEquiv_mapDGShiftClosureHom {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) {X Y : TauCeti.DGShiftClosure C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (TauCeti.DGShiftClosure.dgHomEquiv R { obj := F.obj X.obj, shift := X.shift } { obj := F.obj Y.obj, shift := Y.shift } n) ((F.mapDGShiftClosureHom X Y n) f) = (F.dgMap (n + (Y.shift - X.shift))) ((TauCeti.DGShiftClosure.dgHomEquiv R X Y n) f)

The underlying morphism of the image of a morphism of the shift closure is the image of its underlying morphism.

@[reducible, inline]

noncomputable abbrev CategoryTheory.EnrichedFunctor.mapDGShiftClosure {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) : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) (TauCeti.DGShiftClosure C) (TauCeti.DGShiftClosure D)

The DG functor between shift closures induced by a DG functor F, sending X[r] to (F X)[r] and applying F to the underlying morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_mapDGShiftClosure {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) {X Y : TauCeti.DGShiftClosure C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (F.mapDGShiftClosure.dgMap n) f = (F.mapDGShiftClosureHom X Y n) f

The induced DG functor acts on morphisms by CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom.

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_shiftHomEquiv {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) {X Y : TauCeti.DGShiftClosure C} (n : ℤ) {p : ℤ} (f : TauCeti.DGHom R p X Y) : (F.mapDGShiftClosureHom { obj := X.obj, shift := X.shift + n } { obj := Y.obj, shift := Y.shift + n } p) ((TauCeti.DGShiftClosure.shiftHomEquiv R X Y n p) f) = (TauCeti.DGShiftClosure.shiftHomEquiv R { obj := F.obj X.obj, shift := X.shift } { obj := F.obj Y.obj, shift := Y.shift } n p) ((F.mapDGShiftClosureHom X Y p) f)

The induced DG functor commutes with shifting every object: the images of a morphism under the two composites have the same underlying morphism of D.

@[simp]

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_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) (X : TauCeti.DGShiftClosure C) (n : ℤ) : (F.mapDGShiftClosureHom X ((TauCeti.DGShiftClosure.shiftFunctor R n).obj X) (-n)) (TauCeti.DGShiftClosure.toShift R X n) = TauCeti.DGShiftClosure.toShift R { obj := F.obj X.obj, shift := X.shift } n

The induced DG functor sends the comparison morphism X[r] ⟶ X[r + n] to the comparison morphism (F X)[r] ⟶ (F X)[r + n].

@[simp]

theorem CategoryTheory.EnrichedFunctor.mapDGShiftClosureHom_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) (X : TauCeti.DGShiftClosure C) (n : ℤ) : (F.mapDGShiftClosureHom ((TauCeti.DGShiftClosure.shiftFunctor R n).obj X) X n) (TauCeti.DGShiftClosure.fromShift R X n) = TauCeti.DGShiftClosure.fromShift R { obj := F.obj X.obj, shift := X.shift } n

The induced DG functor sends the comparison morphism X[r + n] ⟶ X[r] to the comparison morphism (F X)[r + n] ⟶ (F X)[r].