The shift on the closed category of dg functors

For pretriangulated D, DGFunctor.shiftedFunctor shifts a dg functor F : C ⟶ D by an integer. The comparison transformations already say that shifting by zero changes nothing and that shifting by n and then by m agrees with shifting by n + m. This file packages exactly that data as

HasShift (Z0 (DGFunctor C D)) ℤ.

Z0 is the right categorical boundary. The raw type DGFunctor C D is enriched over complexes and has no ordinary category structure; in Z0, its morphisms are the closed degree-zero homogeneous natural transformations, and all four comparison transformations are therefore honest categorical morphisms. No second shift abstraction is introduced: the package is Mathlib's ShiftMkCore, hence its associativity and unit laws are the standard ones consumed by shiftFunctorAdd and shiftFunctorZero.

Direction of the additive comparison

DGFunctor.shiftedFunctorAdd points from the iterated shift to the total shift. Mathlib's ShiftMkCore.add points the other way, from the total shift to the iterated shift, so its hom is shiftedFunctorAddInv and its inv is shiftedFunctorAdd. The associativity field is not reproved pointwise: the two candidate homs are identified because their inverse paths are precisely shiftedFunctorAddAssocLeft and shiftedFunctorAddAssocRight, whose equality is shiftedFunctorAdd_assoc.

The two unit fields are the remaining content. On the right they reduce to the inverse of the zero comparison on F[n]; on the left they are the shift of the inverse zero comparison on F. Both are consequences of the existing IsShiftBy comparison calculus.

noncomputable def CategoryTheory.DGFunctor.z0ShiftFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n : ℤ) : Functor (Z0 (DGFunctor C D)) (Z0 (DGFunctor C D))

Shift closed degree-zero transformations pointwise. Closedness is exactly what makes the result a morphism of Z0 (DGFunctor C D).

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.z0ShiftFunctor_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n : ℤ) (F : Z0 (DGFunctor C D)) : (z0ShiftFunctor n).obj F = (Z0.of (DGFunctor C D) F).shiftedFunctor n

theorem CategoryTheory.DGFunctor.z0ShiftFunctor_map_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n : ℤ) {F G : Z0 (DGFunctor C D)} (α : F ⟶ G) : ↑((z0ShiftFunctor n).map α) = HomogeneousNatTrans.shiftedDegreeZero (↑α) n

The underlying transformation of the shifted Z0 morphism.

noncomputable def CategoryTheory.DGFunctor.z0ShiftFunctorZeroIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : z0ShiftFunctor 0 ≅ Functor.id (Z0 (DGFunctor C D))

The zero-shift comparison as a natural isomorphism of closed dg functors.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.z0ShiftFunctorZeroIso_hom_app_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : Z0 (DGFunctor C D)) : ↑(z0ShiftFunctorZeroIso.hom.app F) = (Z0.of (DGFunctor C D) F).shiftedFunctorZero

@[simp]

theorem CategoryTheory.DGFunctor.z0ShiftFunctorZeroIso_inv_app_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : Z0 (DGFunctor C D)) : ↑(z0ShiftFunctorZeroIso.inv.app F) = (Z0.of (DGFunctor C D) F).shiftedFunctorZeroInv

noncomputable def CategoryTheory.DGFunctor.z0ShiftFunctorAddIso' {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m nm : ℤ) (hnm : n + m = nm) : z0ShiftFunctor nm ≅ (z0ShiftFunctor n).comp (z0ShiftFunctor m)

The additive comparison as a natural isomorphism, with a free total degree. The direction is Mathlib's: total shift to iterated shift.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_hom_app_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m nm : ℤ) (hnm : n + m = nm) (F : Z0 (DGFunctor C D)) : ↑((z0ShiftFunctorAddIso' n m nm hnm).hom.app F) = (Z0.of (DGFunctor C D) F).shiftedFunctorAddInv n m nm hnm

@[simp]

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_inv_app_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m nm : ℤ) (hnm : n + m = nm) (F : Z0 (DGFunctor C D)) : ↑((z0ShiftFunctorAddIso' n m nm hnm).inv.app F) = (Z0.of (DGFunctor C D) F).shiftedFunctorAdd n m nm hnm

noncomputable def CategoryTheory.DGFunctor.z0ShiftFunctorAddIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m : ℤ) : z0ShiftFunctor (n + m) ≅ (z0ShiftFunctor n).comp (z0ShiftFunctor m)

The additive comparison at the definitional total degree.

Equations

• CategoryTheory.DGFunctor.z0ShiftFunctorAddIso n m = CategoryTheory.DGFunctor.z0ShiftFunctorAddIso' n m (n + m) ⋯

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_hom_app_zero_right {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n nm : ℤ) (hnm : n + 0 = nm) (F : Z0 (DGFunctor C D)) : (z0ShiftFunctorAddIso' n 0 nm hnm).hom.app F = CategoryStruct.comp (eqToHom ⋯) (z0ShiftFunctorZeroIso.inv.app ((z0ShiftFunctor n).obj F))

The right unit law for the additive comparison, in free-degree form.

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_hom_app_zero_left {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n nm : ℤ) (hnm : 0 + n = nm) (F : Z0 (DGFunctor C D)) : (z0ShiftFunctorAddIso' 0 n nm hnm).hom.app F = CategoryStruct.comp (eqToHom ⋯) ((z0ShiftFunctor n).map (z0ShiftFunctorZeroIso.inv.app F))

The left unit law for the additive comparison, in free-degree form.

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_hom_app_congr {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m nm nm' : ℤ) (h : n + m = nm) (h' : n + m = nm') (F : Z0 (DGFunctor C D)) : (z0ShiftFunctorAddIso' n m nm h).hom.app F = CategoryStruct.comp (eqToHom ⋯) ((z0ShiftFunctorAddIso' n m nm' h').hom.app F)

Additive comparisons at propositionally equal total degrees differ only by the corresponding eqToHom.

theorem CategoryTheory.DGFunctor.z0ShiftFunctorAddIso'_assoc {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m k nm mk r : ℤ) (hnm : n + m = nm) (hmk : m + k = mk) (hleft : nm + k = r) (hright : n + mk = r) (F : Z0 (DGFunctor C D)) : CategoryStruct.comp ((z0ShiftFunctorAddIso' nm k r hleft).hom.app F) ((z0ShiftFunctor k).map ((z0ShiftFunctorAddIso' n m nm hnm).hom.app F)) = CategoryStruct.comp ((z0ShiftFunctorAddIso' n mk r hright).hom.app F) ((z0ShiftFunctorAddIso' m k mk hmk).hom.app ((z0ShiftFunctor n).obj F))

Associativity of the additive comparison, in the exact component form required by ShiftMkCore.

The inverse of the left-hand composite is shiftedFunctorAddAssocLeft; the inverse of the right-hand composite is shiftedFunctorAddAssocRight. Thus this is shiftedFunctorAdd_assoc, transported once through Iso.symm, rather than a second pointwise associativity proof.

noncomputable def CategoryTheory.DGFunctor.z0ShiftMkCore {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : ShiftMkCore (Z0 (DGFunctor C D)) ℤ

The explicit shifted dg functors and their canonical comparisons, packaged as Mathlib shift data on the closed category of dg functors.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.DGFunctor.z0HasShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : HasShift (Z0 (DGFunctor C D)) ℤ

Closed dg functors have the pointwise dg shift as a Mathlib HasShift.

Equations

• CategoryTheory.DGFunctor.z0HasShift = CategoryTheory.hasShiftMk (CategoryTheory.Z0 (CategoryTheory.DGFunctor C D)) ℤ CategoryTheory.DGFunctor.z0ShiftMkCore

theorem CategoryTheory.DGFunctor.z0_shiftFunctor_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n : ℤ) : shiftFunctor (Z0 (DGFunctor C D)) n = z0ShiftFunctor n

The ambient shift functor is the pointwise shifted dg functor.

@[simp]

theorem CategoryTheory.DGFunctor.z0_shiftFunctor_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n : ℤ) (F : Z0 (DGFunctor C D)) : (shiftFunctor (Z0 (DGFunctor C D)) n).obj F = (Z0.of (DGFunctor C D) F).shiftedFunctor n

The object selected by the ambient shift is DGFunctor.shiftedFunctor.

theorem CategoryTheory.DGFunctor.z0_shiftFunctorZero_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : shiftFunctorZero (Z0 (DGFunctor C D)) ℤ = z0ShiftFunctorZeroIso

The ambient zero comparison is the dg zero-shift comparison.

theorem CategoryTheory.DGFunctor.z0_shiftFunctorAdd_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (n m : ℤ) : shiftFunctorAdd (Z0 (DGFunctor C D)) n m = z0ShiftFunctorAddIso n m

The ambient additive comparison is the dg additive comparison.