Two-periodic complexes are curved duplexes of curvature zero

A curved duplex X₀ --d₀--> X₁ --d₁--> X₀ of curvature 0 has both composites d₀ ≫ d₁ and d₁ ≫ d₀ equal to zero, so it is the same datum as a two-periodic complex, that is a ZMod 2-indexed complex for the shape ComplexShape.up (ZMod 2), with X₀ in degree 0, X₁ in degree 1, and d₀, d₁ the two differentials. This file makes the identification precise, so that the curvature-zero specialization of curved duplexes inherits Mathlib's homological-complex vocabulary instead of duplicating it:

• CurvedDuplex.periodicComplexEquivalence is the equivalence between curved duplexes of curvature zero and two-periodic complexes, with functor CurvedDuplex.toPeriodicComplex and inverse CurvedDuplex.ofPeriodicComplex;
• CurvedDuplex.nonempty_homotopy_toPeriodicComplex_map_zero_iff identifies the null-homotopic morphisms d h + h d of duplexes with the morphisms of two-periodic complexes homotopic to zero in Mathlib's sense, and CurvedDuplex.kerIdeal_toPeriodicComplex_comp_quotient restates this as an equality of ideals;
• CurvedDuplex.HomotopyCategory.periodicComplexEquivalence is the induced equivalence between the homotopy category of curved duplexes of curvature zero and Mathlib's homotopy category HomotopyCategory C (ComplexShape.up (ZMod 2)) of two-periodic complexes; it restricts to CurvedDuplex.toPeriodicComplex along the quotient functors, and its inverse restricts to CurvedDuplex.ofPeriodicComplex up to the isomorphism CurvedDuplex.HomotopyCategory.quotientCompPeriodicComplexEquivalenceInverseIso.

For nonzero curvature, the composites need not vanish, so a curved duplex need not be a complex; this file makes no comparison outside curvature zero.

References

• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3 (curved complexes and duplexes and their homotopy categories).
• Torkil Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.

@[implicit_reducible]

def TauCeti.CurvedDuplex.toPeriodicComplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor (CurvedDuplex C 0) (HomologicalComplex C (ComplexShape.up (ZMod 2)))

The two-periodic complex attached to a curved duplex of curvature zero: the even component sits in degree 0, the odd component in degree 1, and the differentials are d₀ and d₁.

@[implicit_reducible]

def TauCeti.CurvedDuplex.ofPeriodicComplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor (HomologicalComplex C (ComplexShape.up (ZMod 2))) (CurvedDuplex C 0)

The curved duplex of curvature zero attached to a two-periodic complex K: its components are K.X 0 and K.X 1, and its differentials are K.d 0 1 and K.d 1 0.

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_obj_X₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((ofPeriodicComplex C R).obj K).X₀ = K.X 0

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_obj_X₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((ofPeriodicComplex C R).obj K).X₁ = K.X 1

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_map_f₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] {X✝ Y✝ : HomologicalComplex C (ComplexShape.up (ZMod 2))} (φ : X✝ ⟶ Y✝) : ((ofPeriodicComplex C R).map φ).f₀ = φ.f 0

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_obj_d₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((ofPeriodicComplex C R).obj K).d₁ = K.d 1 0

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_map_f₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] {X✝ Y✝ : HomologicalComplex C (ComplexShape.up (ZMod 2))} (φ : X✝ ⟶ Y✝) : ((ofPeriodicComplex C R).map φ).f₁ = φ.f 1

@[simp]

theorem TauCeti.CurvedDuplex.ofPeriodicComplex_obj_d₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((ofPeriodicComplex C R).obj K).d₀ = K.d 0 1

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_obj_X_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) : ((toPeriodicComplex C R).obj X).X 0 = X.X₀

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_obj_X_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) : ((toPeriodicComplex C R).obj X).X 1 = X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_obj_d_zero_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) : ((toPeriodicComplex C R).obj X).d 0 1 = X.d₀

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_obj_d_one_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) : ((toPeriodicComplex C R).obj X).d 1 0 = X.d₁

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_map_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {X Y : CurvedDuplex C 0} (f : X ⟶ Y) : ((toPeriodicComplex C R).map f).f 0 = f.f₀

@[simp]

theorem TauCeti.CurvedDuplex.toPeriodicComplex_map_f_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {X Y : CurvedDuplex C 0} (f : X ⟶ Y) : ((toPeriodicComplex C R).map f).f 1 = f.f₁

instance TauCeti.CurvedDuplex.instAdditiveOfNatHomologicalComplexZModNatUpToPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (toPeriodicComplex C R).Additive

instance TauCeti.CurvedDuplex.instLinearOfNatHomologicalComplexZModNatUpToPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (toPeriodicComplex C R)

instance TauCeti.CurvedDuplex.instAdditiveHomologicalComplexZModOfNatNatUpOfPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (ofPeriodicComplex C R).Additive

instance TauCeti.CurvedDuplex.instLinearHomologicalComplexZModOfNatNatUpOfPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (ofPeriodicComplex C R)

def TauCeti.CurvedDuplex.periodicComplexEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : CurvedDuplex C 0 ≌ HomologicalComplex C (ComplexShape.up (ZMod 2))

Curved duplexes of curvature zero are two-periodic complexes: the functors toPeriodicComplex and ofPeriodicComplex are mutually inverse equivalences.

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : (periodicComplexEquivalence C R).inverse = ofPeriodicComplex C R

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : (periodicComplexEquivalence C R).functor = toPeriodicComplex C R

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_counitIso_hom_app_f_zero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((periodicComplexEquivalence C R).counitIso.hom.app K).f 0 = CategoryTheory.CategoryStruct.id (K.X 0)

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_counitIso_hom_app_f_one (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((periodicComplexEquivalence C R).counitIso.hom.app K).f 1 = CategoryTheory.CategoryStruct.id (K.X 1)

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_counitIso_inv_app_f_zero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((periodicComplexEquivalence C R).counitIso.inv.app K).f 0 = CategoryTheory.CategoryStruct.id (K.X 0)

@[simp]

theorem TauCeti.CurvedDuplex.periodicComplexEquivalence_counitIso_inv_app_f_one (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] (K : HomologicalComplex C (ComplexShape.up (ZMod 2))) : ((periodicComplexEquivalence C R).counitIso.inv.app K).f 1 = CategoryTheory.CategoryStruct.id (K.X 1)

instance TauCeti.CurvedDuplex.instIsEquivalenceOfNatHomologicalComplexZModNatUpToPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (toPeriodicComplex C R).IsEquivalence

instance TauCeti.CurvedDuplex.instIsEquivalenceHomologicalComplexZModOfNatNatUpOfPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (ofPeriodicComplex C R).IsEquivalence

Homotopies

theorem TauCeti.CurvedDuplex.nonempty_homotopy_toPeriodicComplex_map_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {X Y : CurvedDuplex C 0} (f : X ⟶ Y) : Nonempty (Homotopy ((toPeriodicComplex C R).map f) 0) ↔ ∃ (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀), nullHomotopicMap h₀ h₁ = f

A morphism of curved duplexes of curvature zero is null-homotopic, that is of the form d h + h d for an odd map h, exactly when the corresponding morphism of two-periodic complexes is homotopic to zero.

theorem TauCeti.CurvedDuplex.nonempty_homotopy_toPeriodicComplex_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {X Y : CurvedDuplex C 0} (f g : X ⟶ Y) : Nonempty (Homotopy ((toPeriodicComplex C R).map f) ((toPeriodicComplex C R).map g)) ↔ ∃ (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀), nullHomotopicMap h₀ h₁ = f - g

Two duplex morphisms become homotopic periodic-complex morphisms exactly when their difference is null-homotopic.

theorem TauCeti.CurvedDuplex.kerIdeal_toPeriodicComplex_comp_quotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : ((toPeriodicComplex C R).comp (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2)))).kerIdeal = nullHomotopic C 0

The null-homotopic morphisms of curved duplexes of curvature zero are exactly the morphisms sent to zero in Mathlib's homotopy category of two-periodic complexes.

The homotopy category

@[reducible, inline]

noncomputable abbrev TauCeti.CurvedDuplex.HomotopyCategory.toPeriodicComplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor (HomotopyCategory C 0) (_root_.HomotopyCategory C (ComplexShape.up (ZMod 2)))

The functor from the homotopy category of curved duplexes of curvature zero to the homotopy category of two-periodic complexes induced by toPeriodicComplex.

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.toPeriodicComplex_obj_quotientFunctor_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) : (toPeriodicComplex C R).obj ((nullHomotopic C 0).quotientFunctor.obj X) = (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))).obj ((CurvedDuplex.toPeriodicComplex C R).obj X)

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.toPeriodicComplex_map_quotientFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {X Y : CurvedDuplex C 0} (f : X ⟶ Y) : (toPeriodicComplex C R).map ((nullHomotopic C 0).quotientFunctor.map f) = (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))).map ((CurvedDuplex.toPeriodicComplex C R).map f)

instance TauCeti.CurvedDuplex.HomotopyCategory.instIsEquivalenceOfNatHomotopyCategoryZModNatUpToPeriodicComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (toPeriodicComplex C R).IsEquivalence

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.periodicComplexEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type w') [Semiring R] [CategoryTheory.Linear R C] : HomotopyCategory C 0 ≌ _root_.HomotopyCategory C (ComplexShape.up (ZMod 2))

The homotopy category of curved duplexes of curvature zero is equivalent to Mathlib's homotopy category of two-periodic complexes, through the functor induced by CurvedDuplex.toPeriodicComplex.

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.periodicComplexEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (periodicComplexEquivalence C R).functor = toPeriodicComplex C R

The functor of the homotopy-category equivalence is the induced periodic-complex functor.

instance TauCeti.CurvedDuplex.HomotopyCategory.instAdditiveOfNatHomotopyCategoryZModNatUpFunctorPeriodicComplexEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (periodicComplexEquivalence C R).functor.Additive

instance TauCeti.CurvedDuplex.HomotopyCategory.instLinearOfNatHomotopyCategoryZModNatUpFunctorPeriodicComplexEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (periodicComplexEquivalence C R).functor

theorem TauCeti.CurvedDuplex.HomotopyCategory.quotientFunctor_comp_periodicComplexEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (nullHomotopic C 0).quotientFunctor.comp (periodicComplexEquivalence C R).functor = (CurvedDuplex.toPeriodicComplex C R).comp (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2)))

The equivalence of homotopy categories is induced by CurvedDuplex.toPeriodicComplex.

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.quotientCompPeriodicComplexEquivalenceInverseIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] : (HomotopyCategory.quotient C (ComplexShape.up (ZMod 2))).comp (periodicComplexEquivalence C R).inverse ≅ (ofPeriodicComplex C R).comp (nullHomotopic C 0).quotientFunctor

The inverse of the equivalence of homotopy categories is induced by CurvedDuplex.ofPeriodicComplex.