Documentation

TauCeti.CommutativeAlgebra.MatrixFactorization.HomotopyInclusion

Finite matrix factorizations in the curved homotopy category #

The inclusion of finite-projective matrix factorizations among curved duplexes descends to homotopy categories. It is fully faithful: an odd homotopy between finite-projective factorizations is exactly an odd homotopy between their underlying curved duplexes. Thus the finite-projective homotopy category has precisely the same morphisms between its objects as the ambient curved homotopy category.

The embedding is moreover a triangle functor for the triangulations of both homotopy categories obtained from their componentwise split Frobenius structures. It commutes with the parity shifts, hence with the shifts by ℤ they generate, and it sends the distinguished triangle of a componentwise split short complex of finite-projective factorizations to the distinguished triangle of the same short complex of curved duplexes. Being full, it then has a triangulated essential image by Mathlib's general instance for full triangle functors.

This comparison uses the full-subcategory presentation of matrix factorizations and the quotient-by-ideal construction. It is the homotopy-level form of the finite-projective inclusion used in Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Sections 1.2 and 3.

Main results #

source
noncomputable def TauCeti.MatrixFactorization.homotopyInclusion {S : Type u} [CommRing S] {w : S} :
CategoryTheory.Functor HomotopyCategory (CurvedDuplex.HomotopyCategory (FGModuleCat S) w)

The finite-projective matrix-factorization homotopy category embeds in the homotopy category of all curved duplexes of finitely generated modules.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.MatrixFactorization.homotopyInclusion_obj {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
    homotopyInclusion.obj (nullHomotopic.quotientFunctor.obj X) = (CurvedDuplex.nullHomotopic (FGModuleCat S) w).quotientFunctor.obj X.obj

    The embedding of homotopy categories agrees on objects with the inclusion of matrix factorizations followed by the curved-duplex quotient.

    source
    theorem TauCeti.MatrixFactorization.homotopyInclusion_map {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (homotopyInclusion.map (nullHomotopic.quotientFunctor.map f)) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((CurvedDuplex.nullHomotopic (FGModuleCat S) w).quotientFunctor.map f.hom)

    On morphisms, the homotopy embedding sends a class to the class of the same closed even map, viewed as a map of curved duplexes.

    source
    instance TauCeti.MatrixFactorization.instFaithfulHomotopyCategoryHomotopyCategoryFGModuleCatHomotopyInclusion {S : Type u} [CommRing S] {w : S} :
    homotopyInclusion.Faithful

    A homotopy class of finite-projective factorizations is zero in the curved-duplex homotopy category only if it was already zero in the matrix-factorization homotopy category.

    source
    instance TauCeti.MatrixFactorization.instFullHomotopyCategoryHomotopyCategoryFGModuleCatHomotopyInclusion {S : Type u} [CommRing S] {w : S} :
    homotopyInclusion.Full

    Every homotopy class between two finite-projective factorizations in the ambient curved homotopy category is represented by a map of finite-projective factorizations.

    source
    theorem TauCeti.MatrixFactorization.quotientFunctor_comp_homotopyInclusion {S : Type u} [CommRing S] {w : S} :
    nullHomotopic.quotientFunctor.comp homotopyInclusion = inclusion.comp (CurvedDuplex.nullHomotopic (FGModuleCat S) w).quotientFunctor

    The homotopy embedding restricts the curved-duplex quotient functor along the inclusion of finite-projective factorizations.

    source
    theorem TauCeti.MatrixFactorization.parityShiftEquivalence_functor_comp_homotopyInclusion {S : Type u} [CommRing S] {w : S} :
    HomotopyCategory.parityShiftEquivalence.functor.comp homotopyInclusion = homotopyInclusion.comp (CurvedDuplex.HomotopyCategory.parityShiftEquivalence (FGModuleCat S) w).functor

    The homotopy embedding commutes with the parity shifts of the two homotopy categories.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.MatrixFactorization.instCommShiftHomotopyCategoryHomotopyCategoryFGModuleCatHomotopyInclusionInt {S : Type u} [CommRing S] {w : S} :
    homotopyInclusion.CommShift ℤ

    The homotopy embedding commutes with the shifts by ℤ generated by the parity shifts.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem TauCeti.MatrixFactorization.homotopyInclusion_commShiftIso_one {S : Type u} [CommRing S] {w : S} :
    CategoryTheory.Functor.commShiftIso homotopyInclusion 1 = CategoryTheory.Functor.isoWhiskerRight (HomotopyCategory.shiftFunctorOneIso S w) homotopyInclusion ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ homotopyInclusion.isoWhiskerLeft (CurvedDuplex.HomotopyCategory.shiftFunctorOneIso (FGModuleCat S) w).symm

    In degree one, the shift compatibility of the homotopy embedding identifies the parity shifts of the two homotopy categories.

    source
    instance TauCeti.MatrixFactorization.instIsTriangulatedHomotopyCategoryHomotopyCategoryFGModuleCatHomotopyInclusion {S : Type u} [CommRing S] {w : S} :
    homotopyInclusion.IsTriangulated

    The homotopy embedding of matrix factorizations is a triangle functor. The image of the distinguished triangle of a componentwise split short complex of finite-projective factorizations is the distinguished triangle of the same short complex of curved duplexes.