The shift on periodic complexes

An n-periodic complex in a preadditive category C is a family of objects Xⁱ indexed by i : ZMod n with differentials Xⁱ ⟶ Xⁱ⁺¹ whose consecutive composites vanish. We use Mathlib's homological complexes for the shape ComplexShape.up (ZMod n), so that the category, its preadditive and linear structures, evaluation functors, homotopies and the homotopy category HomotopyCategory C (ComplexShape.up (ZMod n)) are all Mathlib's.

This file equips periodic complexes and their homotopy category with a shift by ℤ, following the conventions of Mathlib's shift on cochain complexes: (X⟦k⟧)ⁱ = Xⁱ⁺ᵏ and the differential is multiplied by (-1)ᵏ. The shift by 1 is thus the cyclic shift (X⟦1⟧)ⁱ = Xⁱ⁺¹, d_{X⟦1⟧} = -d_X, and generates the whole shift. Since the grading is cyclic, the shift is periodic: shifting by an even multiple k of the period is isomorphic to the identity, both on complexes and on the homotopy category.

A periodic complex proper has a positive period: ZMod 0 is integer indexing, hence an ordinary complex rather than a finite cyclic grading. None of the constructions below uses positivity of n, so no NeZero n hypothesis is imposed. For n = 0 the formulas degenerate to those of Mathlib's shift on cochain complexes.

Main definitions

• TauCeti.PeriodicComplex.shiftFunctor: the shift by k : ℤ on ZMod n-graded complexes.
• TauCeti.PeriodicComplex.instHasShift: the resulting shift by ℤ on periodic complexes.
• TauCeti.PeriodicComplex.shiftFunctorIsoId: the periodicity isomorphism X⟦k⟧ ≅ X for even k divisible by n.
• Homotopy.periodicShift: the shift of a homotopy.
• TauCeti.PeriodicComplex.homotopyCategoryShiftFunctorIsoId: periodicity in the homotopy category.

References

• Torkil Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.
• The construction mirrors Joël Riou's shift on cochain complexes in Mathlib.Algebra.Homology.HomotopyCategory.Shift.

@[implicit_reducible]

def TauCeti.PeriodicComplex.shiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) : CategoryTheory.Functor (HomologicalComplex C (ComplexShape.up (ZMod n))) (HomologicalComplex C (ComplexShape.up (ZMod n)))

The shift by k : ℤ on ZMod n-graded complexes: it sends K to the complex which is K.X (i + k) in degree i, with the differentials multiplied by (-1)ᵏ.

Equations

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

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_obj_d (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i j : ZMod n) : ((shiftFunctor C n k).obj K).d i j = k.negOnePow • K.d (i + ↑k) (j + ↑k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctor C n k).obj K).X i = K.X (i + ↑k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) {X✝ Y✝ : HomologicalComplex C (ComplexShape.up (ZMod n))} (φ : X✝ ⟶ Y✝) (i : ZMod n) : ((shiftFunctor C n k).map φ).f i = φ.f (i + ↑k)

instance TauCeti.PeriodicComplex.instAdditiveHomologicalComplexZModUpShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) : (shiftFunctor C n k).Additive

instance TauCeti.PeriodicComplex.instLinearHomologicalComplexZModUpShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (shiftFunctor C n k)

def TauCeti.PeriodicComplex.shiftFunctorObjXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k : ℤ) (i m : ZMod n) (hm : m = i + ↑k) : ((shiftFunctor C n k).obj K).X i ≅ K.X m

The canonical isomorphism ((shiftFunctor C n k).obj K).X i ≅ K.X m when m = i + k.

Equations

• TauCeti.PeriodicComplex.shiftFunctorObjXIso K k i m hm = K.XIsoOfEq ⋯

@[implicit_reducible]

def TauCeti.PeriodicComplex.shiftFunctorZero' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (h : k = 0) : shiftFunctor C n k ≅ CategoryTheory.Functor.id (HomologicalComplex C (ComplexShape.up (ZMod n)))

The shift by k identifies to the identity functor when k = 0.

Equations

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

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorZero'_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (h : k = 0) (X : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorZero' C n k h).inv.app X).f i = (X.XIsoOfEq ⋯).inv

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorZero'_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (h : k = 0) (X : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorZero' C n k h).hom.app X).f i = (X.XIsoOfEq ⋯).hom

@[implicit_reducible]

def TauCeti.PeriodicComplex.shiftFunctorAdd' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k₁ k₂ k₁₂ : ℤ) (h : k₁ + k₂ = k₁₂) : shiftFunctor C n k₁₂ ≅ (shiftFunctor C n k₁).comp (shiftFunctor C n k₂)

The compatibility of the shift functors with the addition of integers.

Equations

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

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd'_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k₁ k₂ k₁₂ : ℤ) (h : k₁ + k₂ = k₁₂) (X : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorAdd' C n k₁ k₂ k₁₂ h).hom.app X).f i = (X.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd'_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k₁ k₂ k₁₂ : ℤ) (h : k₁ + k₂ = k₁₂) (X : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorAdd' C n k₁ k₂ k₁₂ h).inv.app X).f i = (X.XIsoOfEq ⋯).inv

@[instance_reducible]

instance TauCeti.PeriodicComplex.instHasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : CategoryTheory.HasShift (HomologicalComplex C (ComplexShape.up (ZMod n))) ℤ

Periodic complexes carry a shift by ℤ, whose shift by 1 is the cyclic shift.

Equations

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

instance TauCeti.PeriodicComplex.instAdditiveHomologicalComplexZModUpShiftFunctorInt_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).Additive

instance TauCeti.PeriodicComplex.instLinearHomologicalComplexZModUpShiftFunctorInt_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_obj_X' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k : ℤ) (i : ZMod n) : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).obj K).X i = K.X (i + ↑k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_map_f' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} (φ : K ⟶ L) (k : ℤ) (i : ZMod n) : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).map φ).f i = φ.f (i + ↑k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctor_obj_d' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k : ℤ) (i j : ZMod n) : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).obj K).d i j = k.negOnePow • K.d (i + ↑k) (j + ↑k)

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k₁ k₂ : ℤ) (i : ZMod n) : ((CategoryTheory.shiftFunctorAdd (HomologicalComplex C (ComplexShape.up (ZMod n))) k₁ k₂).hom.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd_inv_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k₁ k₂ : ℤ) (i : ZMod n) : ((CategoryTheory.shiftFunctorAdd (HomologicalComplex C (ComplexShape.up (ZMod n))) k₁ k₂).inv.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd'_hom_app_f' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k₁ k₂ k₁₂ : ℤ) (h : k₁ + k₂ = k₁₂) (i : ZMod n) : ((CategoryTheory.shiftFunctorAdd' (HomologicalComplex C (ComplexShape.up (ZMod n))) k₁ k₂ k₁₂ h).hom.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorAdd'_inv_app_f' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k₁ k₂ k₁₂ : ℤ) (h : k₁ + k₂ = k₁₂) (i : ZMod n) : ((CategoryTheory.shiftFunctorAdd' (HomologicalComplex C (ComplexShape.up (ZMod n))) k₁ k₂ k₁₂ h).inv.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorZero_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((CategoryTheory.shiftFunctorZero (HomologicalComplex C (ComplexShape.up (ZMod n))) ℤ).hom.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorZero_inv_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((CategoryTheory.shiftFunctorZero (HomologicalComplex C (ComplexShape.up (ZMod n))) ℤ).inv.app K).f i = (K.XIsoOfEq ⋯).hom

def TauCeti.PeriodicComplex.shiftEval (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (i i' : ZMod n) (hi : i + ↑k = i') : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).comp (HomologicalComplex.eval C (ComplexShape.up (ZMod n)) i) ≅ HomologicalComplex.eval C (ComplexShape.up (ZMod n)) i'

Shifting by k and evaluating in degree i identifies to evaluating in degree i' when i + k = i'.

Equations

• TauCeti.PeriodicComplex.shiftEval C n k i i' hi = CategoryTheory.NatIso.ofComponents (fun (K : HomologicalComplex C (ComplexShape.up (ZMod n))) => K.XIsoOfEq hi) ⋯

@[simp]

theorem TauCeti.PeriodicComplex.shiftEval_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (i i' : ZMod n) (hi : i + ↑k = i') (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : (shiftEval C n k i i' hi).hom.app K = (K.XIsoOfEq hi).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftEval_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (i i' : ZMod n) (hi : i + ↑k = i') (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : (shiftEval C n k i i' hi).inv.app K = (K.XIsoOfEq hi).inv

def TauCeti.PeriodicComplex.shiftFunctorIsoId (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) : CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k ≅ CategoryTheory.Functor.id (HomologicalComplex C (ComplexShape.up (ZMod n)))

Periodicity of the shift: shifting by an even integer k which is a multiple of the period is isomorphic to the identity. The degree-i component is the identification Xⁱ⁺ᵏ = Xⁱ; evenness of k is what makes it commute with the differentials.

Equations

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

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorIsoId_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorIsoId C n k hk he).hom.app K).f i = (K.XIsoOfEq ⋯).hom

@[simp]

theorem TauCeti.PeriodicComplex.shiftFunctorIsoId_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ZMod n) : ((shiftFunctorIsoId C n k hk he).inv.app K).f i = (K.XIsoOfEq ⋯).inv

def Homotopy.periodicShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} {φ₁ φ₂ : K ⟶ L} (h : Homotopy φ₁ φ₂) (k : ℤ) : Homotopy ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).map φ₁) ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).map φ₂)

If h : Homotopy φ₁ φ₂ and k : ℤ, this is the induced homotopy between φ₁⟦k⟧' and φ₂⟦k⟧'.

Equations

• h.periodicShift k = { hom := fun (i j : ZMod n) => k.negOnePow • h.hom (i + ↑k) (j + ↑k), zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.periodicShift_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} {φ₁ φ₂ : K ⟶ L} (h : Homotopy φ₁ φ₂) (k : ℤ) (i j : ZMod n) : (h.periodicShift k).hom i j = k.negOnePow • h.hom (i + ↑k) (j + ↑k)

instance TauCeti.PeriodicComplex.instIsCompatibleWithShiftHomologicalComplexZModUpHomotopicInt_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : (homotopic C (ComplexShape.up (ZMod n))).IsCompatibleWithShift ℤ

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.homotopyCategoryHasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : CategoryTheory.HasShift (HomotopyCategory C (ComplexShape.up (ZMod n))) ℤ

The periodic homotopy category carries the shift by ℤ induced from periodic complexes.

Equations

• TauCeti.PeriodicComplex.homotopyCategoryHasShift C n = TauCeti.PeriodicComplex.homotopyCategoryHasShift._aux_1 C n

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.commShiftQuotient (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).CommShift ℤ

The quotient functor to the periodic homotopy category commutes with the shift.

Equations

• TauCeti.PeriodicComplex.commShiftQuotient C n = CategoryTheory.Quotient.functor_commShift (homotopic C (ComplexShape.up (ZMod n))) ℤ

@[simp]

theorem TauCeti.PeriodicComplex.shift_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (k : ℤ) : (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up (ZMod n))) k).obj ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K) = (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k).obj K)

instance TauCeti.PeriodicComplex.instAdditiveHomotopyCategoryZModUpShiftFunctorInt_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) : (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up (ZMod n))) k).Additive

instance TauCeti.PeriodicComplex.instLinearHomotopyCategoryZModUpShiftFunctorInt_tauCeti (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] (k : ℤ) : CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up (ZMod n))) k)

noncomputable def TauCeti.PeriodicComplex.homotopyCategoryShiftFunctorIsoId (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) : CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up (ZMod n))) k ≅ CategoryTheory.Functor.id (HomotopyCategory C (ComplexShape.up (ZMod n)))

Periodicity of the shift on the periodic homotopy category: shifting by an even integer k which is a multiple of the period is isomorphic to the identity.

Equations

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

@[simp]

theorem TauCeti.PeriodicComplex.homotopyCategoryShiftFunctorIsoId_hom_app_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : (homotopyCategoryShiftFunctorIsoId C n k hk he).hom.app ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))) k).inv.app K) ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).map ((shiftFunctorIsoId C n k hk he).hom.app K))

@[simp]

theorem TauCeti.PeriodicComplex.homotopyCategoryShiftFunctorIsoId_inv_app_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) (hk : ↑k = 0) (he : Even k) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : (homotopyCategoryShiftFunctorIsoId C n k hk he).inv.app ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).map ((shiftFunctorIsoId C n k hk he).inv.app K)) ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))) k).hom.app K)