Shifts of twisted objects

Let C be a differential graded category. The twisted objects (⊕ᵢ Xᵢ[rᵢ], δ) of the additive closure of the shift closure of C are shifted summandwise: the shift by n is the twisted object (⊕ᵢ Xᵢ[rᵢ + n], δ), whose twisting matrix has the same entries as δ, viewed as morphisms of C. Since Hom(Xᵢ[rᵢ + n], Xⱼ[rⱼ + n]) = Hom(Xᵢ, Xⱼ)[rⱼ - rᵢ] = Hom(Xᵢ[rᵢ], Xⱼ[rⱼ]) in the shift closure, with the same differential and composition signs, this is the image of the twisted object under the DG functor induced by the shift X[r] ↦ X[r + n] of the shift closure (TauCeti.DGShiftClosure.shiftFunctor). So the shift is a DG functor TauCeti.DGTwistedObject.shiftFunctor n, which does not change the matrix entries of morphisms.

What makes P⟦n⟧ the shift of P is a closed invertible morphism P ⟶ P⟦n⟧ of degree -n: composing with it identifies Hom(Z, P⟦n⟧) with Hom(Z, P)[n] and Hom(P⟦n⟧, Z) with Hom(P, Z)[-n]. It is the diagonal matrix TauCeti.DGTwistedObject.toShift whose entry at the summand Xᵢ[rᵢ] is (-1)^(n * rᵢ) times the identity of Xᵢ (TauCeti.DGShiftClosure.toShift), that is, the comparison morphism TauCeti.DGAdditiveClosure.toShift of the underlying objects. The signs make it natural up to the Koszul sign, f ≫ σ_Q = (-1)^(n * p) • σ_P ≫ f⟦n⟧ for f of degree p (TauCeti.DGTwistedObject.dgComp_toShift). Applied to the twisting matrix, of degree one, this says that σ_P is closed for the twisted differential d σ + (-1)^n • σ ≫ δ⟦n⟧ - δ ≫ σ. Without the signs it would not be: the identity entries alone would leave the error ((-1)^n - (-1)^(n * (1 + rⱼ - rᵢ))) • δᵢⱼ in the entry from Xᵢ to Xⱼ. The diagonal matrix TauCeti.DGTwistedObject.fromShift with the same entries is its inverse, of degree n.

The shifts do not compose strictly: P⟦a⟧⟦b⟧ has summands Xᵢ[rᵢ + a + b] and P⟦a + b⟧ has summands Xᵢ[rᵢ + (a + b)]. They are identified by closed degree-zero isomorphisms built from the comparison morphisms: TauCeti.DGTwistedObject.shiftAddHom P a b is the composite P⟦a + b⟧ ⟶ P ⟶ P⟦b⟧ ⟶ P⟦a⟧⟦b⟧ whose last map is the shift by b of P ⟶ P⟦a⟧. Composing directly through P ⟶ P⟦a⟧ ⟶ P⟦a⟧⟦b⟧ instead gives (-1)^(a * b) times shiftAddHom P a b (TauCeti.DGTwistedObject.shiftAddHom_eq_negOnePow_smul_dgComp), by the Koszul-sign naturality of the comparison morphisms. This second description makes the associativity and unit coherences of these isomorphisms a cancellation of comparison morphisms, the signs (-1)^((a + b) * c + a * b) and (-1)^(a * (b + c) + b * c) agreeing.

In the same way the shifts commute up to the closed degree-zero isomorphism TauCeti.DGTwistedObject.shiftCommHom P a b, the composite of comparison morphisms P⟦a⟧⟦b⟧ ⟶ P⟦a⟧ ⟶ P ⟶ P⟦b⟧ ⟶ P⟦b⟧⟦a⟧. The shift by b of the comparison morphism P⟦a⟧ ⟶ P is (-1)^(a * b) times this isomorphism followed by the comparison morphism P⟦b⟧⟦a⟧ ⟶ P⟦b⟧ (TauCeti.DGTwistedObject.dgMap_fromShift); this is the sign by which the shift of a cone differs from the cone of the shifted morphism.

Shifts are the second ingredient, with extensions (see TauCeti/CategoryTheory/DG/Twisted/Extension.lean), of the cone (Q ⊕ P⟦1⟧, δ) of a closed degree-zero morphism u : P ⟶ Q of twisted objects, along the closed degree-one morphism P⟦1⟧ ⟶ P ⟶ Q.

Main definitions

• TauCeti.DGTwistedObject.shiftFunctor: the DG functor shifting every summand of a twisted object by n.
• TauCeti.DGTwistedObject.toShift and TauCeti.DGTwistedObject.fromShift: the comparison morphisms P ⟶ P⟦n⟧ of degree -n and P⟦n⟧ ⟶ P of degree n.
• TauCeti.DGTwistedObject.shiftAddHom and TauCeti.DGTwistedObject.shiftAddInv: the mutually inverse closed degree-zero morphisms P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ and P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧.
• TauCeti.DGTwistedObject.shiftCommHom: the closed degree-zero isomorphism P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧.

Main results

• TauCeti.DGTwistedObject.dgHomEquiv_toShift and TauCeti.DGTwistedObject.dgHomEquiv_fromShift: the comparison morphisms are those of the underlying objects of the additive closure.
• TauCeti.DGTwistedObject.dgHomEquiv_twist_shiftFunctor_obj and TauCeti.DGTwistedObject.dgHomEquiv_dgMap_shiftFunctor: the shift does not change the matrix entries of the twist or of a morphism, as morphisms of C.
• TauCeti.DGTwistedObject.dgDifferential_toShift and TauCeti.DGTwistedObject.dgDifferential_fromShift: the comparison morphisms are closed.
• TauCeti.DGTwistedObject.dgComp_toShift_fromShift and TauCeti.DGTwistedObject.dgComp_fromShift_toShift: they are mutually inverse (with _assoc forms for reassociated composites).
• TauCeti.DGTwistedObject.dgComp_toShift and TauCeti.DGTwistedObject.dgComp_fromShift: they are natural up to the Koszul sign, and TauCeti.DGTwistedObject.toShift_dgComp_dgMap_assoc and TauCeti.DGTwistedObject.dgMap_dgComp_fromShift_assoc are the sign-free forms for degree-zero morphisms.
• TauCeti.DGTwistedObject.dgComp_shiftAddHom_shiftAddInv and TauCeti.DGTwistedObject.dgComp_shiftAddInv_shiftAddHom: the comparisons of iterated shifts are inverse.
• TauCeti.DGTwistedObject.dgMap_dgComp_shiftAddHom: shiftAddHom is natural.
• TauCeti.DGTwistedObject.shiftAddHom_assoc, TauCeti.DGTwistedObject.shiftAddHom_zero_add and TauCeti.DGTwistedObject.shiftAddHom_add_zero: the associativity and unit coherences of shiftAddHom.
• TauCeti.DGTwistedObject.dgComp_shiftCommHom_shiftCommHom: shiftCommHom P a b and shiftCommHom P b a are inverse, and TauCeti.DGTwistedObject.shiftCommHom_eq_dgComp_shiftAddInv expresses shiftCommHom through the comparisons of iterated shifts.
• TauCeti.DGTwistedObject.dgMap_fromShift: the shift of a comparison morphism, and TauCeti.DGTwistedObject.dgMap_fromShift_self its form for the shift by its own degree, where TauCeti.DGTwistedObject.shiftCommHom_self makes the comparison of shifts the identity.

References

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

The shift functor

@[reducible, inline]

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

The DG functor shifting the twisted objects of the additive closure of the shift closure by n: it sends (⊕ᵢ Xᵢ[rᵢ], δ) to (⊕ᵢ Xᵢ[rᵢ + n], δ), the entries of the twisting matrix and of every morphism being unchanged as morphisms of C.

theorem TauCeti.DGTwistedObject.dgHomEquiv_twist_shiftFunctor_obj {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (i j : P.obj.ι) : (DGAdditiveClosure.dgHomEquiv R ((shiftFunctor R n).obj P).obj ((shiftFunctor R n).obj P).obj 1) ((shiftFunctor R n).obj P).twist i j = (DGShiftClosure.shiftHomEquiv R (P.obj.X i) (P.obj.X j) n 1) ((DGAdditiveClosure.dgHomEquiv R P.obj P.obj 1) P.twist i j)

The shift does not change the entries of the twisting matrix, as morphisms of C.

theorem TauCeti.DGTwistedObject.dgHomEquiv_dgMap_shiftFunctor {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {p : ℤ} (f : DGHom R p P Q) (i : P.obj.ι) (j : Q.obj.ι) : (DGAdditiveClosure.dgHomEquiv R ((shiftFunctor R n).obj P).obj ((shiftFunctor R n).obj Q).obj p) ((dgHomEquiv R ((shiftFunctor R n).obj P) ((shiftFunctor R n).obj Q) p) (((shiftFunctor R n).dgMap p) f)) i j = (DGShiftClosure.shiftHomEquiv R (P.obj.X i) (Q.obj.X j) n p) ((DGAdditiveClosure.dgHomEquiv R P.obj Q.obj p) ((dgHomEquiv R P Q p) f) i j)

The shift does not change the entries of a morphism, as morphisms of C.

theorem TauCeti.DGTwistedObject.shiftFunctor_obj_ofObj {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) (M : DGAdditiveClosure (DGShiftClosure C)) : (shiftFunctor R n).obj (ofObj R M) = ofObj R { ι := M.ι, fintype := M.fintype, X := fun (i : M.ι) => { obj := (M.X i).obj, shift := (M.X i).shift + n } }

The shift of an object of the additive closure with the zero twist is the shifted object with the zero twist.

The comparison morphisms of twisted objects

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

The comparison morphism P ⟶ P⟦n⟧ of degree -n: the diagonal matrix whose entry at the summand Xᵢ[rᵢ] is (-1)^(n * rᵢ) times the identity of Xᵢ.

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

The comparison morphism P⟦n⟧ ⟶ P of degree n: the diagonal matrix whose entry at the summand Xᵢ[rᵢ] is (-1)^(n * rᵢ) times the identity of Xᵢ.

@[simp]

theorem TauCeti.DGTwistedObject.dgHomEquiv_toShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) : (dgHomEquiv R P ((shiftFunctor R n).obj P) (-n)) (P.toShift n) = DGAdditiveClosure.toShift R P.obj n

The matrix of P ⟶ P⟦n⟧ is the comparison morphism of the underlying objects.

@[simp]

theorem TauCeti.DGTwistedObject.dgHomEquiv_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) : (dgHomEquiv R ((shiftFunctor R n).obj P) P n) (P.fromShift n) = DGAdditiveClosure.fromShift R P.obj n

The matrix of P⟦n⟧ ⟶ P is the inverse comparison morphism of the underlying objects.

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

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

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

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

@[simp]

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

The comparison morphism P ⟶ P⟦n⟧ is closed for the twisted differential: by naturality, δ ≫ σ = (-1)^n • σ ≫ δ⟦n⟧, which cancels the twisting terms of D σ.

@[simp]

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

The comparison morphisms P ⟶ P⟦n⟧ ⟶ P compose to the identity of P.

@[simp]

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

The comparison morphisms P⟦n⟧ ⟶ P ⟶ P⟦n⟧ compose to the identity of P⟦n⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_toShift_fromShift_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) {Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {q m : ℤ} (x : DGHom R q P Z) (h : n + q = m) (h' : -n + m = q) : dgComp R (P.toShift n) (dgComp R (P.fromShift n) x h) h' = x

The comparison morphisms P ⟶ P⟦n⟧ ⟶ P followed by x compose to x.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_fromShift_toShift_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) {Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {q m : ℤ} (x : DGHom R q ((shiftFunctor R n).obj P) Z) (h : -n + q = m) (h' : n + m = q) : dgComp R (P.fromShift n) (dgComp R (P.toShift n) x h) h' = x

The comparison morphisms P⟦n⟧ ⟶ P ⟶ P⟦n⟧ followed by x compose to x.

theorem TauCeti.DGTwistedObject.toShift_dgComp_dgMap_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) {P Q Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (f : DGHom R 0 P Q) {q m : ℤ} (x : DGHom R q ((shiftFunctor R n).obj Q) Z) (h : -n + q = m) : dgComp R (P.toShift n) (dgComp R (((shiftFunctor R n).dgMap 0) f) x ⋯) h = dgComp R f (dgComp R (Q.toShift n) x h) ⋯

The comparison morphisms are natural in degree zero: for f : P ⟶ Q of degree zero, P ⟶ P⟦n⟧ followed by the shift of f and x is f followed by Q ⟶ Q⟦n⟧ and x.

theorem TauCeti.DGTwistedObject.dgMap_dgComp_fromShift_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) {P Q Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (f : DGHom R 0 P Q) {q m : ℤ} (x : DGHom R q Q Z) (h : n + q = m) : dgComp R (((shiftFunctor R n).dgMap 0) f) (dgComp R (Q.fromShift n) x h) ⋯ = dgComp R (P.fromShift n) (dgComp R f x ⋯) h

The inverse comparison morphisms are natural in degree zero: for f : P ⟶ Q of degree zero, the shift of f followed by Q⟦n⟧ ⟶ Q and x is P⟦n⟧ ⟶ P followed by f and x.

@[simp]

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

The comparison morphism P⟦n⟧ ⟶ P is closed, as the inverse of a closed morphism.

Degree bookkeeping

The coherences below compare composites of comparison morphisms whose degrees are integer expressions such as -a + -b and a + -(a + b), which agree only propositionally. The general rewriting rules TauCeti.dgComp_assoc_eq_castDeg, TauCeti.castDeg_dgComp_eq_castDeg, TauCeti.dgComp_castDeg_eq_castDeg and TauCeti.dgId_dgComp_eq_castDeg, together with the following rules for the comparison morphisms, bring such composites to a normal form: a degree transport castDeg of a right-associated composite whose intermediate degrees are the sums of the degrees of the factors. Two composites of the same factors then agree up to the outer degree transport. The rules are applied with simp -proj, which keeps the shifted objects (shiftFunctor R n).obj P folded so that the comparison lemmas about TauCeti.DGTwistedObject.toShift and TauCeti.DGTwistedObject.fromShift keep matching.

The comparison of iterated shifts

noncomputable def TauCeti.DGTwistedObject.shiftAddHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : DGHom R 0 ((shiftFunctor R (a + b)).obj P) ((shiftFunctor R b).obj ((shiftFunctor R a).obj P))

The comparison P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧, a closed degree-zero isomorphism: the comparison morphisms P⟦a + b⟧ ⟶ P ⟶ P⟦b⟧ followed by the shift by b of the comparison morphism P ⟶ P⟦a⟧.

noncomputable def TauCeti.DGTwistedObject.shiftAddInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : DGHom R 0 ((shiftFunctor R b).obj ((shiftFunctor R a).obj P)) ((shiftFunctor R (a + b)).obj P)

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧, inverse to TauCeti.DGTwistedObject.shiftAddHom: the shift by b of the comparison morphism P⟦a⟧ ⟶ P followed by the comparison morphisms P⟦b⟧ ⟶ P ⟶ P⟦a + b⟧.

theorem TauCeti.DGTwistedObject.shiftAddHom_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftAddHom a b = dgComp R (P.fromShift (a + b)) (dgComp R (P.toShift b) (((shiftFunctor R b).dgMap (-a)) (P.toShift a)) ⋯) ⋯

The comparison P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ is P⟦a + b⟧ ⟶ P ⟶ P⟦b⟧ followed by the shift of P ⟶ P⟦a⟧.

theorem TauCeti.DGTwistedObject.shiftAddInv_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftAddInv a b = dgComp R (((shiftFunctor R b).dgMap a) (P.fromShift a)) (dgComp R (P.fromShift b) (P.toShift (a + b)) ⋯) ⋯

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧ is the shift of P⟦a⟧ ⟶ P followed by P⟦b⟧ ⟶ P ⟶ P⟦a + b⟧.

theorem TauCeti.DGTwistedObject.shiftAddHom_eq_negOnePow_smul_dgComp {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftAddHom a b = (a * b).negOnePow • dgComp R (P.fromShift (a + b)) (dgComp R (P.toShift a) (((shiftFunctor R a).obj P).toShift b) ⋯) ⋯

Through P ⟶ P⟦a⟧ ⟶ P⟦a⟧⟦b⟧ instead, the comparison P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ acquires the Koszul sign (-1)^(a * b).

theorem TauCeti.DGTwistedObject.shiftAddInv_eq_negOnePow_smul_dgComp {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftAddInv a b = (a * b).negOnePow • dgComp R (((shiftFunctor R a).obj P).fromShift b) (dgComp R (P.fromShift a) (P.toShift (a + b)) ⋯) ⋯

Through P⟦a⟧⟦b⟧ ⟶ P⟦a⟧ ⟶ P instead, the comparison P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧ acquires the Koszul sign (-1)^(a * b).

@[simp]

theorem TauCeti.DGTwistedObject.dgDifferential_shiftAddHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : (dgDifferential R 0) (P.shiftAddHom a b) = 0

The comparison P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ is closed.

@[simp]

theorem TauCeti.DGTwistedObject.dgDifferential_shiftAddInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : (dgDifferential R 0) (P.shiftAddInv a b) = 0

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧ is closed.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftAddHom_shiftAddInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : dgComp R (P.shiftAddHom a b) (P.shiftAddInv a b) ⋯ = dgId R ((shiftFunctor R (a + b)).obj P)

The comparisons P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧ compose to the identity.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftAddInv_shiftAddHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : dgComp R (P.shiftAddInv a b) (P.shiftAddHom a b) ⋯ = dgId R ((shiftFunctor R b).obj ((shiftFunctor R a).obj P))

The comparisons P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ compose to the identity.

theorem TauCeti.DGTwistedObject.dgMap_dgComp_shiftAddHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (a b : ℤ) (f : DGHom R 0 P Q) : dgComp R (((shiftFunctor R (a + b)).dgMap 0) f) (Q.shiftAddHom a b) ⋯ = dgComp R (P.shiftAddHom a b) (((shiftFunctor R b).dgMap 0) (((shiftFunctor R a).dgMap 0) f)) ⋯

The comparison P⟦a + b⟧ ⟶ P⟦a⟧⟦b⟧ is natural in degree-zero morphisms f : P ⟶ Q.

theorem TauCeti.DGTwistedObject.shiftAddHom_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b c : ℤ) : dgComp R (P.shiftAddHom (a + b) c) (((shiftFunctor R c).dgMap 0) (P.shiftAddHom a b)) ⋯ = dgComp R (dgComp R (P.fromShift (a + b + c)) (P.toShift (a + (b + c))) ⋯) (dgComp R (P.shiftAddHom a (b + c)) (((shiftFunctor R a).obj P).shiftAddHom b c) ⋯) ⋯

Associativity of the comparisons: P⟦a + b + c⟧ ⟶ P⟦a + b⟧⟦c⟧ ⟶ P⟦a⟧⟦b⟧⟦c⟧ agrees with P⟦a + b + c⟧ ⟶ P⟦a + (b + c)⟧ ⟶ P⟦a⟧⟦b + c⟧ ⟶ P⟦a⟧⟦b⟧⟦c⟧, whose first map is the comparison P⟦a + b + c⟧ ⟶ P ⟶ P⟦a + (b + c)⟧.

theorem TauCeti.DGTwistedObject.shiftAddHom_zero_add {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) : P.shiftAddHom 0 n = dgComp R (dgComp R (P.fromShift (0 + n)) (P.toShift n) ⋯) (((shiftFunctor R n).dgMap 0) (P.toShift 0)) ⋯

Left unit law of the comparisons: P⟦0 + n⟧ ⟶ P⟦0⟧⟦n⟧ is the comparison P⟦0 + n⟧ ⟶ P ⟶ P⟦n⟧ followed by the shift by n of P ⟶ P⟦0⟧.

theorem TauCeti.DGTwistedObject.shiftAddHom_add_zero {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (n : ℤ) : P.shiftAddHom n 0 = dgComp R (dgComp R (P.fromShift (n + 0)) (P.toShift n) ⋯) (((shiftFunctor R n).obj P).toShift 0) ⋯

Right unit law of the comparisons: P⟦n + 0⟧ ⟶ P⟦n⟧⟦0⟧ is the comparison P⟦n + 0⟧ ⟶ P ⟶ P⟦n⟧ followed by P⟦n⟧ ⟶ P⟦n⟧⟦0⟧.

The commutation of shifts

noncomputable def TauCeti.DGTwistedObject.shiftCommHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : DGHom R 0 ((shiftFunctor R b).obj ((shiftFunctor R a).obj P)) ((shiftFunctor R a).obj ((shiftFunctor R b).obj P))

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧, a closed degree-zero isomorphism: the comparison morphisms P⟦a⟧⟦b⟧ ⟶ P⟦a⟧ ⟶ P ⟶ P⟦b⟧ ⟶ P⟦b⟧⟦a⟧.

theorem TauCeti.DGTwistedObject.shiftCommHom_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftCommHom a b = dgComp R (((shiftFunctor R a).obj P).fromShift b) (dgComp R (P.fromShift a) (dgComp R (P.toShift b) (((shiftFunctor R b).obj P).toShift a) ⋯) ⋯) ⋯

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ is P⟦a⟧⟦b⟧ ⟶ P⟦a⟧ ⟶ P ⟶ P⟦b⟧ ⟶ P⟦b⟧⟦a⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgDifferential_shiftCommHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : (dgDifferential R 0) (P.shiftCommHom a b) = 0

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ is closed.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftCommHom_shiftCommHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : dgComp R (P.shiftCommHom a b) (P.shiftCommHom b a) ⋯ = dgId R ((shiftFunctor R b).obj ((shiftFunctor R a).obj P))

The comparisons P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ ⟶ P⟦a⟧⟦b⟧ compose to the identity.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftCommHom_shiftCommHom_assoc {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) {Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {m : ℤ} (x : DGHom R m ((shiftFunctor R b).obj ((shiftFunctor R a).obj P)) Z) : dgComp R (P.shiftCommHom a b) (dgComp R (P.shiftCommHom b a) x ⋯) ⋯ = x

The comparisons P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ ⟶ P⟦a⟧⟦b⟧ followed by x are x.

theorem TauCeti.DGTwistedObject.units_smul_dgComp_shiftCommHom_units_smul_dgComp_shiftCommHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (ε : ℤˣ) (a b : ℤ) {Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {m : ℤ} (x : DGHom R m ((shiftFunctor R b).obj ((shiftFunctor R a).obj P)) Z) : ε • dgComp R (P.shiftCommHom a b) (ε • dgComp R (P.shiftCommHom b a) x ⋯) ⋯ = x

A sign times the comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧, followed by the same sign times the comparison P⟦b⟧⟦a⟧ ⟶ P⟦a⟧⟦b⟧ and then x, is x.

theorem TauCeti.DGTwistedObject.shiftCommHom_eq_dgComp_shiftAddInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : P.shiftCommHom a b = dgComp R (P.shiftAddInv a b) (dgComp R (dgComp R (P.fromShift (a + b)) (P.toShift (b + a)) ⋯) (P.shiftAddHom b a) ⋯) ⋯

The comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ is the comparison P⟦a⟧⟦b⟧ ⟶ P⟦a + b⟧, followed by the comparison P⟦a + b⟧ ⟶ P ⟶ P⟦b + a⟧ and the comparison P⟦b + a⟧ ⟶ P⟦b⟧⟦a⟧.

theorem TauCeti.DGTwistedObject.dgMap_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a b : ℤ) : ((shiftFunctor R b).dgMap a) (P.fromShift a) = (a * b).negOnePow • dgComp R (P.shiftCommHom a b) (((shiftFunctor R b).obj P).fromShift a) ⋯

The shift of a comparison morphism: the shift by b of the comparison morphism P⟦a⟧ ⟶ P is (-1)^(a * b) times the comparison P⟦a⟧⟦b⟧ ⟶ P⟦b⟧⟦a⟧ followed by the comparison morphism P⟦b⟧⟦a⟧ ⟶ P⟦b⟧.

@[simp]

theorem TauCeti.DGTwistedObject.shiftCommHom_self {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a : ℤ) : P.shiftCommHom a a = dgId R ((shiftFunctor R a).obj ((shiftFunctor R a).obj P))

The comparison P⟦a⟧⟦a⟧ ⟶ P⟦a⟧⟦a⟧ exchanging two equal shifts is the identity.

theorem TauCeti.DGTwistedObject.dgMap_fromShift_self {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) (a : ℤ) : ((shiftFunctor R a).dgMap a) (P.fromShift a) = (a * a).negOnePow • ((shiftFunctor R a).obj P).fromShift a

The shift of a comparison morphism by its own degree: the shift by a of the comparison morphism P⟦a⟧ ⟶ P is (-1)^(a * a) times the comparison morphism P⟦a⟧⟦a⟧ ⟶ P⟦a⟧.