The shift on the homotopy category of matrix factorizations

The parity shift, which swaps the two components of a finite-projective matrix factorization and negates both maps, is a self-equivalence of the homotopy category HMF(S,w), here MatrixFactorization.HomotopyCategory. This file equips HMF(S,w) with the shift by ℤ that it generates, so that the shift by 1 is the parity shift.

This is the shift of Happel's triangulation. Finite-projective matrix factorizations with the componentwise split exact structure form a Frobenius exact category, and every factorization X has the relative injective presentation

X ⟶ diskSum X ⟶ X[1]

whose middle term is the contractible disk sum on the components of X and whose cokernel term is the parity shift X[1]. Since stable suspension may be computed from any relative injective presentation, stable suspension is the parity shift in the stable category. Consequently the equivalence MatrixFactorization.stableToHomotopy between the stable category and HMF(S,w) commutes coherently with the shifts by ℤ: the one generated by stable suspension and the one generated by the parity shift.

Main definitions

• TauCeti.MatrixFactorization.HomotopyCategory.instHasShift: the shift by ℤ on HMF(S,w) generated by the parity shift.
• TauCeti.MatrixFactorization.HomotopyCategory.parityShiftCompQuotientFunctorIso: the image of the parity shift of a factorization is the shift by 1 of its image.
• TauCeti.MatrixFactorization.splitSuspensionPresentation: the componentwise split injective presentation X ⟶ diskSum X ⟶ X[1].
• TauCeti.MatrixFactorization.splitStableSuspensionIsoParityShift: stable suspension of matrix factorizations is the parity shift.
• TauCeti.MatrixFactorization.stableSuspensionCompStableToHomotopyIso: the stable-to-homotopy comparison intertwines stable suspension with the parity shift.
• TauCeti.MatrixFactorization.stableToHomotopyCommShift: the stable-to-homotopy comparison commutes with the shifts by ℤ.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2: suspension in the stable category of a Frobenius category.
• D. Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Proc. Steklov Inst. Math. 246 (2004), Section 3, for the category of finite-projective matrix factorizations and its shift.

The construction follows the curved-duplex version in TauCeti.Algebra.Homology.Curved.Shift, restricted to finite-projective components.

@[instance_reducible]

noncomputable instance TauCeti.MatrixFactorization.HomotopyCategory.instHasShift (S : Type u) [CommRing S] (w : S) : CategoryTheory.HasShift HomotopyCategory ℤ

The shift by ℤ on the homotopy category of matrix factorizations generated by the parity shift.

Equations

• TauCeti.MatrixFactorization.HomotopyCategory.instHasShift S w = TauCeti.MatrixFactorization.HomotopyCategory.parityShiftEquivalence.hasShift

noncomputable def TauCeti.MatrixFactorization.HomotopyCategory.shiftFunctorOneIso (S : Type u) [CommRing S] (w : S) : CategoryTheory.shiftFunctor HomotopyCategory 1 ≅ parityShiftEquivalence.functor

The shift by 1 on the homotopy category of matrix factorizations is the parity shift.

Equations

• TauCeti.MatrixFactorization.HomotopyCategory.shiftFunctorOneIso S w = TauCeti.MatrixFactorization.HomotopyCategory.parityShiftEquivalence.shiftFunctorOneIso

theorem TauCeti.MatrixFactorization.HomotopyCategory.shiftFunctorOneIso_def (S : Type u) [CommRing S] (w : S) : shiftFunctorOneIso S w = parityShiftEquivalence.shiftFunctorOneIso

The identification of the shift by 1 with the parity shift is the one carried by the shift generated by the parity-shift autoequivalence.

instance TauCeti.MatrixFactorization.HomotopyCategory.instAdditiveShiftFunctorInt (S : Type u) [CommRing S] (w : S) (n : ℤ) : (CategoryTheory.shiftFunctor HomotopyCategory n).Additive

Every shift functor of the homotopy category of matrix factorizations is additive.

noncomputable def TauCeti.MatrixFactorization.HomotopyCategory.parityShiftCompQuotientFunctorIso (S : Type u) [CommRing S] (w : S) : parityShift.comp nullHomotopic.quotientFunctor ≅ nullHomotopic.quotientFunctor.comp (CategoryTheory.shiftFunctor HomotopyCategory 1)

The image in the homotopy category of the parity shift of a factorization is the shift by 1 of its image, naturally.

Equations

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

@[simp]

theorem TauCeti.MatrixFactorization.HomotopyCategory.parityShiftCompQuotientFunctorIso_hom_app {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (parityShiftCompQuotientFunctorIso S w).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((shiftFunctorOneIso S w).inv.app (nullHomotopic.quotientFunctor.obj X))

The component of parityShiftCompQuotientFunctorIso at X identifies the image of the parity shift of X with the parity shift of its image, followed by shiftFunctorOneIso.

noncomputable def TauCeti.MatrixFactorization.splitSuspensionPresentation {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (splitExact S w).InjectivePresentation X

The componentwise split injective presentation X ⟶ diskSum X ⟶ X[1] of a matrix factorization: its middle term is the contractible disk sum on the components of X, and its cokernel term is the parity shift of X.

Equations

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

@[simp]

theorem TauCeti.MatrixFactorization.splitSuspensionPresentation_I {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.splitSuspensionPresentation.I = X.diskSum

@[simp]

theorem TauCeti.MatrixFactorization.splitSuspensionPresentation_K {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.splitSuspensionPresentation.K = parityShift.obj X

@[simp]

theorem TauCeti.MatrixFactorization.splitSuspensionPresentation_i {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.splitSuspensionPresentation.i = X.toDiskSum

@[simp]

theorem TauCeti.MatrixFactorization.splitSuspensionPresentation_p {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.splitSuspensionPresentation.p = X.diskSumToParityShift

theorem TauCeti.MatrixFactorization.projectiveStableFunctor_map_splitSuspensionPresentation_cokernelMap {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (splitExact S w).projectiveStableFunctor.map (X.splitSuspensionPresentation.cokernelMap Y.splitSuspensionPresentation f) = (splitExact S w).projectiveStableFunctor.map (parityShift.map f)

In the stable category, the morphism induced by f on the cokernel terms of the disk-sum presentations is the parity shift of f.

noncomputable def TauCeti.MatrixFactorization.splitStableSuspensionIsoParityShift (S : Type u) [CommRing S] (w : S) : (splitExact S w).projectiveStableFunctor.comp ⋯.stableSuspension ≅ parityShift.comp (splitExact S w).projectiveStableFunctor

Stable suspension of matrix factorizations is the parity shift. For the componentwise split exact structure, the stable suspension of (the image of) a finite-projective matrix factorization is (the image of) its parity shift, naturally.

Equations

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

@[simp]

theorem TauCeti.MatrixFactorization.splitStableSuspensionIsoParityShift_hom_app (S : Type u) [CommRing S] (w : S) (X : MatrixFactorization S w) : (splitStableSuspensionIsoParityShift S w).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((splitExact S w).projectiveStableFunctor.map ((⋯.suspensionPresentation X).cokernelMap X.splitSuspensionPresentation (CategoryTheory.CategoryStruct.id X)))

The component of splitStableSuspensionIsoParityShift at X is induced by the identity of X, from the chosen suspension presentation to the disk-sum presentation.

@[simp]

theorem TauCeti.MatrixFactorization.splitStableSuspensionIsoParityShift_inv_app (S : Type u) [CommRing S] (w : S) (X : MatrixFactorization S w) : (splitStableSuspensionIsoParityShift S w).inv.app X = CategoryTheory.CategoryStruct.comp ((splitExact S w).projectiveStableFunctor.map (X.splitSuspensionPresentation.cokernelMap (⋯.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯)

The inverse component of splitStableSuspensionIsoParityShift at X is induced by the identity of X, from the disk-sum presentation to the chosen suspension presentation.

noncomputable def TauCeti.MatrixFactorization.stableSuspensionCompStableToHomotopyIso (S : Type u) [CommRing S] (w : S) : ⋯.stableSuspension.comp (stableToHomotopy S w) ≅ (stableToHomotopy S w).comp HomotopyCategory.parityShiftEquivalence.functor

The comparison from the componentwise split stable category to HMF(S,w) intertwines stable suspension with the parity shift.

Equations

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

theorem TauCeti.MatrixFactorization.stableSuspensionCompStableToHomotopyIso_hom_app (S : Type u) [CommRing S] (w : S) (X : MatrixFactorization S w) : (stableSuspensionCompStableToHomotopyIso S w).hom.app ((splitExact S w).projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (nullHomotopic.quotientFunctor.map ((⋯.suspensionPresentation X).cokernelMap X.splitSuspensionPresentation (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯))

On the stable image of a factorization X, the intertwining isomorphism is the homotopy class of the map induced by the identity of X from the chosen suspension presentation to the disk-sum presentation.

@[instance_reducible]

noncomputable def TauCeti.MatrixFactorization.stableToHomotopyCommShift (S : Type u) [CommRing S] (w : S) : (stableToHomotopy S w).CommShift ℤ

The comparison from the componentwise split stable category to HMF(S,w) commutes with the shifts by ℤ: the one generated by stable suspension and the one generated by the parity shift.

Equations

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

theorem TauCeti.MatrixFactorization.stableToHomotopyCommShift_iso_one (S : Type u) [CommRing S] (w : S) : CategoryTheory.Functor.commShiftIso (stableToHomotopy S w) 1 = CategoryTheory.Functor.isoWhiskerRight ⋯.stableShiftFunctorOneIso (stableToHomotopy S w) ≪≫ stableSuspensionCompStableToHomotopyIso S w ≪≫ (stableToHomotopy S w).isoWhiskerLeft (HomotopyCategory.shiftFunctorOneIso S w).symm

In degree one, the shift compatibility of the stable-to-homotopy comparison is the identification of stable suspension with the parity shift.