The cone of a closed morphism of twisted objects

Let C be a differential graded category and let u : P ⟶ Q be a closed degree-zero morphism of twisted objects of the additive closure of the shift closure of C. Its cone TauCeti.DGTwistedObject.cone u is the twisted object (Q ⊕ P⟦1⟧, δ) whose twisting matrix has the twists of Q and of the shift P⟦1⟧ on the diagonal and, in the block from P⟦1⟧ to Q, the degree-one morphism P⟦1⟧ ⟶ P ⟶ Q obtained by composing u with the comparison morphism TauCeti.DGTwistedObject.fromShift (TauCeti.DGTwistedObject.coneMorphism). It is the extension of P⟦1⟧ by Q along this morphism (see TauCeti/CategoryTheory/DG/Twisted/Extension.lean), which supplies its Maurer–Cartan equation, the closed degree-zero morphisms Q ⟶ cone u ⟶ P⟦1⟧ with zero composite, and their graded splitting. In particular, a closed morphism f : X ⟶ Y of C, viewed as a morphism of one-term twisted objects X[0] ⟶ Y[0], has a cone whose underlying object is Y[0] ⊕ X[1].

These maps give the candidate triangle P ⟶ Q ⟶ cone u ⟶ P⟦1⟧ of the pretriangulated envelope. In the homotopy category both remaining consecutive composites vanish: u followed by the inclusion of Q is the differential of minus the comparison morphism P ⟶ P⟦1⟧ followed by the inclusion of P⟦1⟧, and the projection onto P⟦1⟧ followed by the shift of u is the differential of minus the projection onto Q followed by the comparison morphism Q ⟶ Q⟦1⟧. The second computation uses the Koszul-sign naturality of the comparison morphisms (TauCeti.DGTwistedObject.dgComp_toShift), whose sign is trivial in degree zero.

The cone depends only on the homotopy class of u: if u - u' = d k for a degree -1 morphism k : P ⟶ Q, then cone u and cone u' are isomorphic in the homotopy category, by the isomorphism of extensions along homotopic morphisms applied to minus P⟦1⟧ ⟶ P followed by k.

The cone of the zero morphism is the extension along zero, the direct sum Q ⊕ P⟦1⟧ of twisted objects. If u has an inverse u' : Q ⟶ P of degree zero, then u' followed by the comparison morphism P ⟶ P⟦1⟧ is a degree -1 inverse of the twisting entry P⟦1⟧ ⟶ Q, so the cone of an isomorphism, and in particular Cone(id_P), is contractible: it is a zero object of the homotopy category.

The shift of a cone is the cone of the shifted morphism: for n : ℤ, the closed degree-zero isomorphism (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) (TauCeti.DGTwistedObject.shiftConeHom) is the shift of the projection onto Q on the summand Q⟦n⟧, and (-1)^n times the comparison P⟦1⟧⟦n⟧ ⟶ P⟦n⟧⟦1⟧ of TauCeti.DGTwistedObject.shiftCommHom on the summand P⟦1⟧⟦n⟧. It is closed because the shift by n of the twisting entry P⟦1⟧ ⟶ P ⟶ Q of cone u is (-1)^n times this comparison followed by the twisting entry P⟦n⟧⟦1⟧ ⟶ P⟦n⟧ ⟶ Q⟦n⟧ of cone (u⟦n⟧) (TauCeti.DGTwistedObject.dgMap_coneMorphism).

Main definitions

• TauCeti.DGTwistedObject.coneMorphism: a degree-zero morphism P ⟶ Q as the degree-one morphism P⟦1⟧ ⟶ Q.
• TauCeti.DGTwistedObject.cone: the cone of a closed degree-zero morphism.
• TauCeti.DGTwistedObject.coneIsoOfHomotopy: the isomorphism in the homotopy category between the cones of homotopic morphisms.
• TauCeti.DGTwistedObject.shiftConeHom and TauCeti.DGTwistedObject.shiftConeInv: the mutually inverse closed degree-zero morphisms (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) and cone (u⟦n⟧) ⟶ (cone u)⟦n⟧.
• TauCeti.DGTwistedObject.shiftConeIso: the induced isomorphism (cone u)⟦n⟧ ≅ cone (u⟦n⟧) in the homotopy category.

Main results

• TauCeti.DGTwistedObject.dgDifferential_coneMorphism: the degree-one morphism underlying a closed morphism is closed.
• TauCeti.DGTwistedObject.dgDifferential_dgComp_toShift_extensionInr_cone and TauCeti.DGTwistedObject.homOf_comp_homOf_extensionInl_cone_eq_zero: u followed by the inclusion of Q into the cone is a boundary, so it vanishes in the homotopy category.
• TauCeti.DGTwistedObject.dgDifferential_dgComp_extensionFst_toShift_cone and TauCeti.DGTwistedObject.homOf_extensionSnd_cone_comp_map_homOf_eq_zero: the projection of the cone onto P⟦1⟧ followed by the shift of u is a boundary, so it vanishes in the homotopy category.
• TauCeti.DGTwistedObject.dgDifferential_neg_dgComp_fromShift: a homotopy from u to u' gives a homotopy between the twisting entries of their cones.
• TauCeti.DGTwistedObject.cone_zero: the cone of the zero morphism is the direct sum Q ⊕ P⟦1⟧.
• TauCeti.DGTwistedObject.isZero_cone_of_dgComp_eq_dgId: the cone of an isomorphism is a zero object of the homotopy category.
• TauCeti.DGTwistedObject.isZero_of_cone_dgId: Cone(id_P) is contractible.
• TauCeti.DGTwistedObject.dgMap_coneMorphism: the shift of the twisting entry of a cone.
• TauCeti.DGTwistedObject.dgComp_shiftConeHom_shiftConeInv and TauCeti.DGTwistedObject.dgComp_shiftConeInv_shiftConeHom: the comparisons of cones are inverse.

References

• A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.4.
• Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, whose isomorphism CochainComplex.mappingCone.shiftIso between shifted mapping cones and mapping cones of shifted morphisms is followed for the shifts of cones.

noncomputable def TauCeti.DGTwistedObject.coneMorphism (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u : DGHom R 0 P Q) : DGHom R 1 ((shiftFunctor R 1).obj P) Q

A degree-zero morphism u : P ⟶ Q of twisted objects, as the degree-one morphism P⟦1⟧ ⟶ P ⟶ Q: the comparison morphism TauCeti.DGTwistedObject.fromShift followed by u.

theorem TauCeti.DGTwistedObject.coneMorphism_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u : DGHom R 0 P Q) : coneMorphism R u = dgComp R (P.fromShift 1) u ⋯

The degree-one morphism underlying u is P⟦1⟧ ⟶ P followed by u.

@[simp]

theorem TauCeti.DGTwistedObject.coneMorphism_zero {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) : coneMorphism R 0 = 0

The degree-one morphism underlying the zero morphism is zero.

@[simp]

theorem TauCeti.DGTwistedObject.coneMorphism_add {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u u' : DGHom R 0 P Q) : coneMorphism R (u + u') = coneMorphism R u + coneMorphism R u'

The degree-one morphism underlying a sum is the sum of the underlying morphisms.

@[simp]

theorem TauCeti.DGTwistedObject.coneMorphism_neg {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u : DGHom R 0 P Q) : coneMorphism R (-u) = -coneMorphism R u

The degree-one morphism underlying -u is minus the one underlying u.

@[simp]

theorem TauCeti.DGTwistedObject.coneMorphism_sub {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u u' : DGHom R 0 P Q) : coneMorphism R (u - u') = coneMorphism R u - coneMorphism R u'

The degree-one morphism underlying a difference is the difference of the underlying morphisms.

theorem TauCeti.DGTwistedObject.dgDifferential_coneMorphism {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) : (dgDifferential R 1) (coneMorphism R u) = 0

The degree-one morphism P⟦1⟧ ⟶ Q underlying a closed morphism u : P ⟶ Q is closed.

theorem TauCeti.DGTwistedObject.dgComp_coneMorphism {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q Z : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {q n : ℤ} (u : DGHom R 0 P Q) (k : DGHom R q Q Z) (h : 1 + q = n) : dgComp R (coneMorphism R u) k h = dgComp R (P.fromShift 1) (dgComp R u k ⋯) h

The morphism P⟦1⟧ ⟶ Q underlying u followed by k is P⟦1⟧ ⟶ P followed by u and k; unlike TauCeti.DGTwistedObject.coneMorphism_def, this rewrites coneMorphism R u only where it is composed, not where it is the twist of a cone.

@[reducible, inline]

noncomputable abbrev TauCeti.DGTwistedObject.cone {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u : DGHom R 0 P Q) (hu : (dgDifferential R 0) u = 0) : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))

The cone of a closed degree-zero morphism u : P ⟶ Q of twisted objects: the twisted object (Q ⊕ P⟦1⟧, δ) whose twisting matrix has the twists of Q and P⟦1⟧ on the diagonal and the morphism P⟦1⟧ ⟶ P ⟶ Q underlying u in the block from P⟦1⟧ to Q.

The triangle of a cone

theorem TauCeti.DGTwistedObject.dgDifferential_dgComp_toShift_extensionInr_cone {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) : (dgDifferential R (-1)) (dgComp R (P.toShift 1) (extensionInr R ⋯) ⋯) = -dgComp R u (extensionInl R ⋯) ⋯

The composite P ⟶ Q ⟶ cone u is null-homotopic: the comparison morphism P ⟶ P⟦1⟧ followed by the inclusion of P⟦1⟧ into the cone has differential minus u followed by the inclusion of Q.

theorem TauCeti.DGTwistedObject.homOf_comp_homOf_extensionInl_cone_eq_zero {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) : CategoryTheory.CategoryStruct.comp (DGHomotopyCategory.homOf R u ⋯) (DGHomotopyCategory.homOf R (extensionInl R ⋯) ⋯) = 0

The composite P ⟶ Q ⟶ cone u vanishes in the homotopy category.

theorem TauCeti.DGTwistedObject.dgDifferential_dgComp_extensionFst_toShift_cone {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) : (dgDifferential R (-1)) (dgComp R (extensionFst R ⋯) (Q.toShift 1) ⋯) = -dgComp R (extensionSnd R ⋯) (((shiftFunctor R 1).dgMap 0) u) ⋯

The composite cone u ⟶ P⟦1⟧ ⟶ Q⟦1⟧ is null-homotopic: the projection of the cone onto Q followed by the comparison morphism Q ⟶ Q⟦1⟧ has differential minus the projection onto P⟦1⟧ followed by the shift of u.

theorem TauCeti.DGTwistedObject.homOf_extensionSnd_cone_comp_map_homOf_eq_zero {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) : CategoryTheory.CategoryStruct.comp (DGHomotopyCategory.homOf R (extensionSnd R ⋯) ⋯) ((shiftFunctor R 1).mapDGHomotopyCategory.map (DGHomotopyCategory.homOf R u ⋯)) = 0

The composite cone u ⟶ P⟦1⟧ ⟶ Q⟦1⟧ vanishes in the homotopy category.

@[simp]

theorem TauCeti.DGTwistedObject.cone_zero {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) : cone 0 ⋯ = Q.extension ((shiftFunctor R 1).obj P) 0 ⋯

The cone of the zero morphism is the direct sum Q ⊕ P⟦1⟧: the extension along the zero morphism, whose twisting matrix has the twists of Q and P⟦1⟧ on the diagonal and vanishes off it.

Cones of homotopic morphisms

theorem TauCeti.DGTwistedObject.dgDifferential_neg_dgComp_fromShift {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u u' : DGHom R 0 P Q} {k : DGHom R (-1) P Q} (hk : (dgDifferential R (-1)) k = u - u') : (dgDifferential R 0) (-dgComp R (P.fromShift 1) k ⋯) = coneMorphism R u - coneMorphism R u'

If u - u' = d k for a degree -1 morphism k : P ⟶ Q, then the twisting entries of the cones of u and u' differ by the differential of minus P⟦1⟧ ⟶ P followed by k.

@[reducible, inline]

noncomputable abbrev TauCeti.DGTwistedObject.coneIsoOfHomotopy {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u u' : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (hu' : (dgDifferential R 0) u' = 0) {k : DGHom R (-1) P Q} (hk : (dgDifferential R (-1)) k = u - u') : DGHomotopyCategory.of R (cone u hu) ≅ DGHomotopyCategory.of R (cone u' hu')

Cones of homotopic morphisms are isomorphic: if u - u' = d k for a degree -1 morphism k : P ⟶ Q, then cone u and cone u' are isomorphic in the homotopy category. The isomorphism is the identity on Q and on P⟦1⟧, together with minus P⟦1⟧ ⟶ P followed by k in the block from P⟦1⟧ to Q.

Cones of isomorphisms are contractible

theorem TauCeti.DGTwistedObject.isZero_cone_of_dgComp_eq_dgId {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} {u' : DGHom R 0 Q P} (hu : (dgDifferential R 0) u = 0) (huu' : dgComp R u u' ⋯ = dgId R P) (hu'u : dgComp R u' u ⋯ = dgId R Q) : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R (cone u hu))

The cone of an isomorphism is contractible: if the closed degree-zero morphism u : P ⟶ Q has a two-sided inverse u' : Q ⟶ P of degree zero, then its cone is a zero object of the homotopy category of twisted objects.

theorem TauCeti.DGTwistedObject.isZero_of_cone_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (P : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))) : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R (cone (dgId R P) ⋯))

The cone of an identity is contractible: Cone(id_P) is a zero object of the homotopy category of twisted objects.

Shifts of cones

theorem TauCeti.DGTwistedObject.dgMap_coneMorphism {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} (u : DGHom R 0 P Q) (n : ℤ) : ((shiftFunctor R n).dgMap 1) (coneMorphism R u) = n.negOnePow • dgComp R (P.shiftCommHom 1 n) (coneMorphism R (((shiftFunctor R n).dgMap 0) u)) ⋯

The shift of the twisting entry of a cone: the shift by n of the degree-one morphism P⟦1⟧ ⟶ P ⟶ Q underlying u is (-1)^n times the comparison P⟦1⟧⟦n⟧ ⟶ P⟦n⟧⟦1⟧ followed by the degree-one morphism P⟦n⟧⟦1⟧ ⟶ P⟦n⟧ ⟶ Q⟦n⟧ underlying the shift of u.

noncomputable def TauCeti.DGTwistedObject.shiftConeHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : DGHom R 0 ((shiftFunctor R n).obj (cone u hu)) (cone (((shiftFunctor R n).dgMap 0) u) ⋯)

The comparison (cone u)⟦n⟧ ⟶ cone (u⟦n⟧): the shift of the projection onto Q followed by the inclusion of Q⟦n⟧, plus (-1)^n times the shift of the projection onto P⟦1⟧ followed by the comparison P⟦1⟧⟦n⟧ ⟶ P⟦n⟧⟦1⟧ and the inclusion of P⟦n⟧⟦1⟧. It is a closed isomorphism with inverse TauCeti.DGTwistedObject.shiftConeInv.

noncomputable def TauCeti.DGTwistedObject.shiftConeInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : DGHom R 0 (cone (((shiftFunctor R n).dgMap 0) u) ⋯) ((shiftFunctor R n).obj (cone u hu))

The comparison cone (u⟦n⟧) ⟶ (cone u)⟦n⟧: the projection onto Q⟦n⟧ followed by the shift of the inclusion of Q, plus (-1)^n times the projection onto P⟦n⟧⟦1⟧ followed by the comparison P⟦n⟧⟦1⟧ ⟶ P⟦1⟧⟦n⟧ and the shift of the inclusion of P⟦1⟧.

theorem TauCeti.DGTwistedObject.shiftConeHom_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : shiftConeHom hu n = dgComp R (((shiftFunctor R n).dgMap 0) (extensionFst R ⋯)) (extensionInl R ⋯) ⋯ + n.negOnePow • dgComp R (((shiftFunctor R n).dgMap 0) (extensionSnd R ⋯)) (dgComp R (P.shiftCommHom 1 n) (extensionInr R ⋯) ⋯) ⋯

theorem TauCeti.DGTwistedObject.shiftConeInv_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : shiftConeInv hu n = dgComp R (extensionFst R ⋯) (((shiftFunctor R n).dgMap 0) (extensionInl R ⋯)) ⋯ + n.negOnePow • dgComp R (extensionSnd R ⋯) (dgComp R (P.shiftCommHom n 1) (((shiftFunctor R n).dgMap 0) (extensionInr R ⋯)) ⋯) ⋯

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_dgMap_extensionInl_shiftConeHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (((shiftFunctor R n).dgMap 0) (extensionInl R ⋯)) (shiftConeHom hu n) ⋯ = extensionInl R ⋯

The shift of the inclusion of Q into cone u followed by the comparison (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) is the inclusion of Q⟦n⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_dgMap_extensionInr_shiftConeHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (((shiftFunctor R n).dgMap 0) (extensionInr R ⋯)) (shiftConeHom hu n) ⋯ = n.negOnePow • dgComp R (P.shiftCommHom 1 n) (extensionInr R ⋯) ⋯

The shift of the inclusion of P⟦1⟧ into cone u followed by the comparison (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) is (-1)^n times the comparison P⟦1⟧⟦n⟧ ⟶ P⟦n⟧⟦1⟧ followed by the inclusion of P⟦n⟧⟦1⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftConeHom_extensionSnd {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (shiftConeHom hu n) (extensionSnd R ⋯) ⋯ = n.negOnePow • dgComp R (((shiftFunctor R n).dgMap 0) (extensionSnd R ⋯)) (P.shiftCommHom 1 n) ⋯

The comparison (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) followed by the projection onto P⟦n⟧⟦1⟧ is (-1)^n times the shift of the projection onto P⟦1⟧ followed by the comparison P⟦1⟧⟦n⟧ ⟶ P⟦n⟧⟦1⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_extensionInl_shiftConeInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (extensionInl R ⋯) (shiftConeInv hu n) ⋯ = ((shiftFunctor R n).dgMap 0) (extensionInl R ⋯)

The inclusion of Q⟦n⟧ into cone (u⟦n⟧) followed by the comparison cone (u⟦n⟧) ⟶ (cone u)⟦n⟧ is the shift of the inclusion of Q.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_extensionInr_shiftConeInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (extensionInr R ⋯) (shiftConeInv hu n) ⋯ = n.negOnePow • dgComp R (P.shiftCommHom n 1) (((shiftFunctor R n).dgMap 0) (extensionInr R ⋯)) ⋯

The inclusion of P⟦n⟧⟦1⟧ into cone (u⟦n⟧) followed by the comparison cone (u⟦n⟧) ⟶ (cone u)⟦n⟧ is (-1)^n times the comparison P⟦n⟧⟦1⟧ ⟶ P⟦1⟧⟦n⟧ followed by the shift of the inclusion of P⟦1⟧.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftConeHom_shiftConeInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (shiftConeHom hu n) (shiftConeInv hu n) ⋯ = dgId R ((shiftFunctor R n).obj (cone u hu))

The comparisons (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) ⟶ (cone u)⟦n⟧ compose to the identity.

@[simp]

theorem TauCeti.DGTwistedObject.dgComp_shiftConeInv_shiftConeHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : dgComp R (shiftConeInv hu n) (shiftConeHom hu n) ⋯ = dgId R (cone (((shiftFunctor R n).dgMap 0) u) ⋯)

The comparisons cone (u⟦n⟧) ⟶ (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) compose to the identity.

@[simp]

theorem TauCeti.DGTwistedObject.dgDifferential_shiftConeHom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : (dgDifferential R 0) (shiftConeHom hu n) = 0

The comparison (cone u)⟦n⟧ ⟶ cone (u⟦n⟧) is closed.

@[simp]

theorem TauCeti.DGTwistedObject.dgDifferential_shiftConeInv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : (dgDifferential R 0) (shiftConeInv hu n) = 0

The comparison cone (u⟦n⟧) ⟶ (cone u)⟦n⟧ is closed, as the inverse of a closed morphism.

noncomputable def TauCeti.DGTwistedObject.shiftConeIso {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : DGHomotopyCategory.of R ((shiftFunctor R n).obj (cone u hu)) ≅ DGHomotopyCategory.of R (cone (((shiftFunctor R n).dgMap 0) u) ⋯)

The shift of a cone is the cone of the shift: in the homotopy category, (cone u)⟦n⟧ is isomorphic to cone (u⟦n⟧), through the comparisons TauCeti.DGTwistedObject.shiftConeHom and TauCeti.DGTwistedObject.shiftConeInv.

@[simp]

theorem TauCeti.DGTwistedObject.shiftConeIso_hom {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : (shiftConeIso hu n).hom = DGHomotopyCategory.homOf R (shiftConeHom hu n) ⋯

@[simp]

theorem TauCeti.DGTwistedObject.shiftConeIso_inv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {P Q : DGTwistedObject R (DGAdditiveClosure (DGShiftClosure C))} {u : DGHom R 0 P Q} (hu : (dgDifferential R 0) u = 0) (n : ℤ) : (shiftConeIso hu n).inv = DGHomotopyCategory.homOf R (shiftConeInv hu n) ⋯