Documentation

TauCeti.CommutativeAlgebra.MatrixFactorization.Exact

The componentwise split exact structure on matrix factorizations #

Finite-projective matrix factorizations form an extension-closed full subcategory of curved duplexes of finitely generated modules with the componentwise split exact structure. The induced conflations split in each parity, but their splittings need not commute with the differentials. A componentwise split conflation with finite-projective middle term also has finite-projective outer terms. Consequently the disk presentations stay in this subcategory.

This is the exact structure used to identify the stable category with the matrix-factorization homotopy category. It follows Frenkel, Khovanov and Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Sections 2–3; the finite-projective formulation follows Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Sections 1.2 and 3. The construction reuses ExactStructure.fullSubcategory and the componentwise exact structure on curved duplexes.

source
theorem TauCeti.MatrixFactorization.isExtensionClosed_isProjective {S : Type u} [CommRing S] {w : S} :
((ExactStructure.split (FGModuleCat S)).curvedDuplex w).IsExtensionClosed (isProjective S w)

Finite-projective duplexes are closed under componentwise split extensions.

source
instance TauCeti.MatrixFactorization.containsZero_isProjective {S : Type u} [CommRing S] {w : S} :
(isProjective S w).ContainsZero

The finite-projective subcategory contains a zero duplex.

source
instance TauCeti.MatrixFactorization.isClosedUnderIsomorphisms_isProjective {S : Type u} [CommRing S] {w : S} :
(isProjective S w).IsClosedUnderIsomorphisms

Finite projectivity of the two components is invariant under duplex isomorphisms.

source
instance TauCeti.MatrixFactorization.isClosedUnderBinaryProducts_isProjective {S : Type u} [CommRing S] {w : S} :
(isProjective S w).IsClosedUnderBinaryProducts

The finite-projective subcategory is closed under binary products.

source
theorem TauCeti.MatrixFactorization.isProjective_outer_of_conflation {S : Type u} [CommRing S] {w : S} {T : CategoryTheory.ShortComplex (CurvedDuplex (FGModuleCat S) w)} (hT : ((ExactStructure.split (FGModuleCat S)).curvedDuplex w).Conflation T) (h₂ : isProjective S w T.X₂) :
isProjective S w T.X₁ ∧ isProjective S w T.X₃

In a componentwise split conflation, projectivity of the middle components implies projectivity of both outer components, since each is a direct summand of the middle one.

source
noncomputable def TauCeti.MatrixFactorization.splitExact (S : Type u) [CommRing S] (w : S) :
ExactStructure (MatrixFactorization S w)

The exact structure on finite-projective matrix factorizations whose conflations split on each underlying module, without requiring differential-compatible splittings.

Equations
Instances For
    source
    theorem TauCeti.MatrixFactorization.splitExact_def (S : Type u) [CommRing S] (w : S) :
    splitExact S w = ExactStructure.fullSubcategory (isProjective S w) ⋯

    The componentwise split structure is induced from the ambient curved-duplex structure.

    source
    @[simp]
    theorem TauCeti.MatrixFactorization.splitExact_conflation_iff {S : Type u} [CommRing S] {w : S} (T : CategoryTheory.ShortComplex (MatrixFactorization S w)) :
    (splitExact S w).Conflation T ↔ Nonempty ((T.map inclusion).map (CurvedDuplex.eval₀ (FGModuleCat S) w)).Splitting ∧ Nonempty ((T.map inclusion).map (CurvedDuplex.eval₁ (FGModuleCat S) w)).Splitting

    A conflation of matrix factorizations is precisely a short complex admitting a splitting in each parity.

    source
    theorem TauCeti.MatrixFactorization.isConflationExact_inclusion {S : Type u} [CommRing S] {w : S} :
    (splitExact S w).IsConflationExact ((ExactStructure.split (FGModuleCat S)).curvedDuplex w) inclusion

    The finite-projective inclusion preserves componentwise split conflations.

    source
    @[simp]
    theorem TauCeti.MatrixFactorization.splitExact_isInflation_iff {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
    (splitExact S w).IsInflation f ↔ ((ExactStructure.split (FGModuleCat S)).curvedDuplex w).IsInflation f.hom

    An inflation in the finite-projective subcategory is precisely an ambient componentwise split inflation. Its cokernel remains finite projective.

    source
    @[simp]
    theorem TauCeti.MatrixFactorization.splitExact_isDeflation_iff {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
    (splitExact S w).IsDeflation f ↔ ((ExactStructure.split (FGModuleCat S)).curvedDuplex w).IsDeflation f.hom

    A deflation in the finite-projective subcategory is precisely an ambient componentwise split deflation. Its kernel remains finite projective.