Parity shift and the shift of two-periodic complexes

Under the equivalence between curvature-zero duplexes and two-periodic complexes, swapping the parity pieces and negating both differentials is the shift by one. The same comparison descends through null homotopies to the equivalence of homotopy categories.

The two shift conventions follow I. Frenkel, M. Khovanov, and O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), §§2–3, and T. Stai, The triangulated hull of periodic complexes, Math. Res. Lett. 25 (2018), §3, respectively.

def TauCeti.CurvedDuplex.parityShiftToPeriodicComplexIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] : (parityShift C 0).comp (toPeriodicComplex C R) ≅ (toPeriodicComplex C R).comp (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod 2))) 1)

The periodic complex of the parity shift is canonically isomorphic to the degree-one shift of the periodic complex. The components of this isomorphism are identities.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftToPeriodicComplexIso_hom_f_zero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : ((parityShiftToPeriodicComplexIso C R).hom.app X).f 0 = CategoryTheory.CategoryStruct.id X.X₁

The even component of the shift comparison is the identity on the old odd component.

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftToPeriodicComplexIso_hom_f_one (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : ((parityShiftToPeriodicComplexIso C R).hom.app X).f 1 = CategoryTheory.CategoryStruct.id X.X₀

The odd component of the shift comparison is the identity on the old even component.

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftToPeriodicComplexIso_inv_f_zero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : ((parityShiftToPeriodicComplexIso C R).inv.app X).f 0 = CategoryTheory.CategoryStruct.id X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftToPeriodicComplexIso_inv_f_one (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : ((parityShiftToPeriodicComplexIso C R).inv.app X).f 1 = CategoryTheory.CategoryStruct.id X.X₀

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.parityShiftToPeriodicComplexIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] : (parityShiftEquivalence C 0).functor.comp (periodicComplexEquivalence C R).functor ≅ (periodicComplexEquivalence C R).functor.comp (CategoryTheory.shiftFunctor (_root_.HomotopyCategory C (ComplexShape.up (ZMod 2))) 1)

The homotopy-category equivalence transports the parity shift to the degree-one periodic shift.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.parityShiftToPeriodicComplexIso_hom_app_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : (parityShiftToPeriodicComplexIso C R).hom.app ((nullHomotopic C 0).quotientFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))).map ((CurvedDuplex.parityShiftToPeriodicComplexIso C R).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))) 1).hom.app ((CurvedDuplex.toPeriodicComplex C R).obj X)) (CategoryTheory.eqToHom ⋯)))

On a duplex, the homotopy-category comparison is the image of the complex-level comparison, followed by the quotient's shift comparison.

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.parityShiftToPeriodicComplexIso_inv_app_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w) [Semiring R] [CategoryTheory.Linear R C] (X : CurvedDuplex C 0) : (parityShiftToPeriodicComplexIso C R).inv.app ((nullHomotopic C 0).quotientFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))) 1).inv.app ((CurvedDuplex.toPeriodicComplex C R).obj X)) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))).map ((CurvedDuplex.parityShiftToPeriodicComplexIso C R).inv.app X)) (CategoryTheory.eqToHom ⋯)))

On a duplex, the inverse homotopy-category comparison is the quotient's inverse shift comparison followed by the image of the inverse complex-level comparison.