Matrix factorizations form a Frobenius exact category

The componentwise split exact structure on finite-projective matrix factorizations has enough relative projectives and injectives, and both classes consist precisely of the contractible factorizations. The disk sum on the components of a factorization supplies its injective presentation; the disk sum on its parity shift supplies its projective presentation. The kernels and cokernels stay finite projective because their components are direct summands of the disk components.

A morphism factors through a relative projective exactly when it is null-homotopic. Thus the stable category is additively and scalar-linearly equivalent to HMF(S,w), here MatrixFactorization.HomotopyCategory. This is an equivalence of additive categories; no compatibility with a prescribed shift or cone triangulation is asserted here.

References

• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), Sections 2–3.
• D. Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Proc. Steklov Inst. Math. 246 (2004), Sections 1.2 and 3.
• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, for the stable triangulation this Frobenius structure supports.

The construction restricts the disk presentations of TauCeti.Algebra.Homology.Curved.Frobenius and uses MorphismIdeal.lift for the comparison.

theorem TauCeti.MatrixFactorization.splitExact_isInjective_of_mem_nullHomotopic {S : Type u} [CommRing S] {w : S} {X : MatrixFactorization S w} (hX : CategoryTheory.CategoryStruct.id X ∈ nullHomotopic.hom X X) : (splitExact S w).isInjective X

Contractible matrix factorizations are relatively injective for the componentwise split exact structure.

theorem TauCeti.MatrixFactorization.splitExact_isProjective_of_mem_nullHomotopic {S : Type u} [CommRing S] {w : S} {X : MatrixFactorization S w} (hX : CategoryTheory.CategoryStruct.id X ∈ nullHomotopic.hom X X) : (splitExact S w).isProjective X

Contractible matrix factorizations are relatively projective for the componentwise split exact structure.

theorem TauCeti.MatrixFactorization.splitExact_isInflation_toDiskSum {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (splitExact S w).IsInflation X.toDiskSum

The canonical embedding into the disk sum is a componentwise split inflation.

theorem TauCeti.MatrixFactorization.splitExact_enoughInjectives (S : Type u) [CommRing S] (w : S) : (splitExact S w).EnoughInjectives

Every finite-projective matrix factorization embeds componentwise split into a contractible finite-projective factorization.

theorem TauCeti.MatrixFactorization.splitExact_enoughProjectives (S : Type u) [CommRing S] (w : S) : (splitExact S w).EnoughProjectives

Every finite-projective matrix factorization is a componentwise split quotient of a contractible finite-projective factorization.

theorem TauCeti.MatrixFactorization.splitExact_isInjective_iff {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (splitExact S w).isInjective X ↔ CategoryTheory.CategoryStruct.id X ∈ nullHomotopic.hom X X

The relative injectives are exactly the contractible finite-projective factorizations.

theorem TauCeti.MatrixFactorization.splitExact_isProjective_iff {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (splitExact S w).isProjective X ↔ CategoryTheory.CategoryStruct.id X ∈ nullHomotopic.hom X X

The relative projectives are exactly the contractible finite-projective factorizations.

theorem TauCeti.MatrixFactorization.splitExact_isFrobenius (S : Type u) [CommRing S] (w : S) : (splitExact S w).IsFrobenius

Finite-projective matrix factorizations form a Frobenius exact category, with contractible factorizations as the projective-injective objects. No regularity assumption is needed.

theorem TauCeti.MatrixFactorization.splitExact_projectiveStableIdeal_eq (S : Type u) [CommRing S] (w : S) : (splitExact S w).projectiveStableIdeal = nullHomotopic

Stable factorization through a relative projective is exactly null-homotopy.

noncomputable def TauCeti.MatrixFactorization.stableToHomotopy (S : Type u) [CommRing S] (w : S) : CategoryTheory.Functor (splitExact S w).ProjectiveStableCategory HomotopyCategory

The canonical stable-to-homotopy comparison sends a stable class to its homotopy class.

Equations

• TauCeti.MatrixFactorization.stableToHomotopy S w = (TauCeti.MatrixFactorization.splitExact S w).projectiveStableIdeal.lift TauCeti.MatrixFactorization.nullHomotopic.quotientFunctor ⋯

theorem TauCeti.MatrixFactorization.projectiveStableFunctor_comp_stableToHomotopy (S : Type u) [CommRing S] (w : S) : (splitExact S w).projectiveStableFunctor.comp (stableToHomotopy S w) = nullHomotopic.quotientFunctor

The comparison agrees with the homotopy quotient on matrix factorizations.

@[simp]

theorem TauCeti.MatrixFactorization.stableToHomotopy_obj (S : Type u) [CommRing S] (w : S) (X : MatrixFactorization S w) : (stableToHomotopy S w).obj ((splitExact S w).projectiveStableFunctor.obj X) = nullHomotopic.quotientFunctor.obj X

On objects the comparison preserves the represented matrix factorization.

theorem TauCeti.MatrixFactorization.stableToHomotopy_map (S : Type u) [CommRing S] (w : S) {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (stableToHomotopy S w).map ((splitExact S w).projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (nullHomotopic.quotientFunctor.map f) (CategoryTheory.eqToHom ⋯))

On morphisms the comparison takes the stable class to the homotopy class of the same map, up to the identification of objects stableToHomotopy_obj.

instance TauCeti.MatrixFactorization.instAdditiveProjectiveStableCategorySplitExactHomotopyCategoryStableToHomotopy (S : Type u) [CommRing S] (w : S) : (stableToHomotopy S w).Additive

The stable-to-homotopy comparison is additive.

instance TauCeti.MatrixFactorization.instLinearProjectiveStableCategorySplitExactHomotopyCategoryStableToHomotopy (S : Type u) [CommRing S] (w : S) : CategoryTheory.Functor.Linear S (stableToHomotopy S w)

The stable-to-homotopy comparison is scalar-linear.

instance TauCeti.MatrixFactorization.instIsEquivalenceProjectiveStableCategorySplitExactHomotopyCategoryStableToHomotopy (S : Type u) [CommRing S] (w : S) : (stableToHomotopy S w).IsEquivalence

The comparison is an equivalence because the two quotients kill the same ideal.

noncomputable def TauCeti.MatrixFactorization.stableHomotopyEquivalence (S : Type u) [CommRing S] (w : S) : (splitExact S w).ProjectiveStableCategory ≌ HomotopyCategory

The stable category of finite-projective matrix factorizations with componentwise split conflations is equivalent to their homotopy category HMF(S,w).

Equations

• TauCeti.MatrixFactorization.stableHomotopyEquivalence S w = (TauCeti.MatrixFactorization.stableToHomotopy S w).asEquivalence

@[simp]

theorem TauCeti.MatrixFactorization.stableHomotopyEquivalence_functor (S : Type u) [CommRing S] (w : S) : (stableHomotopyEquivalence S w).functor = stableToHomotopy S w

instance TauCeti.MatrixFactorization.instAdditiveProjectiveStableCategorySplitExactHomotopyCategoryFunctorStableHomotopyEquivalence (S : Type u) [CommRing S] (w : S) : (stableHomotopyEquivalence S w).functor.Additive

instance TauCeti.MatrixFactorization.instLinearProjectiveStableCategorySplitExactHomotopyCategoryFunctorStableHomotopyEquivalence (S : Type u) [CommRing S] (w : S) : CategoryTheory.Functor.Linear S (stableHomotopyEquivalence S w).functor

noncomputable def TauCeti.MatrixFactorization.homotopyQuotientCompStableInverseIso (S : Type u) [CommRing S] (w : S) : nullHomotopic.quotientFunctor.comp (stableHomotopyEquivalence S w).inverse ≅ (splitExact S w).projectiveStableFunctor

The inverse comparison sends the homotopy class of a factorization back to its stable class, naturally in matrix factorizations.

Equations

• TauCeti.MatrixFactorization.homotopyQuotientCompStableInverseIso S w = (CategoryTheory.eqToIso ⋯).compInverseIso