Documentation

TauCeti.CommutativeAlgebra.MatrixFactorization.Basic

Finite-projective matrix factorizations #

A matrix factorization of w : S is a curved duplex of S-modules with finitely generated projective components. We use FGModuleCat S for finite generation and take the full subcategory on the objects whose components are projective. Thus its morphisms are exactly the closed even maps of curved duplexes, and its forgetful functor is fully faithful.

The parity shift preserves matrix factorizations. The elementary factorization P --𝟙--> P --w--> P supplies contractible objects whenever P is finitely generated projective. These constructions are used in the homotopy and triangulated categories of matrix factorizations.

The matrix-factorization equations follow D. Eisenbud, Homological algebra on a complete intersection, with an application to group representations, Trans. Amer. Math. Soc. 260 (1980), Section 5, where the components are finite free. The finite-projective formulation follows D. Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Proc. Steklov Inst. Math. 246 (2004), Sections 1.2 and 3. The ambient curved-duplex convention follows TauCeti.Algebra.Homology.Curved.Duplex.

source
@[implicit_reducible]
def TauCeti.MatrixFactorization.isProjective (S : Type u) [CommRing S] (w : S) :
CategoryTheory.ObjectProperty (CurvedDuplex (FGModuleCat S) w)

Curved duplexes whose even and odd components are projective modules. Finite generation is already part of the objects of FGModuleCat S.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.MatrixFactorization (S : Type u) [CommRing S] (w : S) :
    Type (u + 1)

    The category of finite-projective matrix factorizations of the potential w over S. Its arrows are pairs of module maps commuting with both differentials.

    Equations
    Instances For
      source
      instance TauCeti.MatrixFactorization.instProjectiveCarrierX₀FGModuleCatObjCurvedDuplexIsProjective {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
      Module.Projective S ↑X.obj.X₀

      The even component of a matrix factorization is projective.

      source
      instance TauCeti.MatrixFactorization.instProjectiveCarrierX₁FGModuleCatObjCurvedDuplexIsProjective {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
      Module.Projective S ↑X.obj.X₁

      The odd component of a matrix factorization is projective.

      source
      def TauCeti.MatrixFactorization.ofCurvedDuplex {S : Type u} [CommRing S] {w : S} (X : CurvedDuplex (FGModuleCat S) w) (h₀ : Module.Projective S ↑X.X₀) (h₁ : Module.Projective S ↑X.X₁) :
      MatrixFactorization S w

      Construct a finite-projective matrix factorization from a curved duplex and projectivity of its two components.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.MatrixFactorization.ofCurvedDuplex_obj {S : Type u} [CommRing S] {w : S} (X : CurvedDuplex (FGModuleCat S) w) (h₀ : Module.Projective S ↑X.X₀) (h₁ : Module.Projective S ↑X.X₁) :
        (ofCurvedDuplex X h₀ h₁).obj = X
        source
        @[reducible, inline]
        abbrev TauCeti.MatrixFactorization.inclusion {S : Type u} [CommRing S] {w : S} :
        CategoryTheory.Functor (MatrixFactorization S w) (CurvedDuplex (FGModuleCat S) w)

        The fully faithful inclusion of finite-projective matrix factorizations into curved duplexes of finitely generated modules.

        Equations
        Instances For
          source
          @[implicit_reducible]
          def TauCeti.MatrixFactorization.parityShift {S : Type u} [CommRing S] {w : S} :
          CategoryTheory.Functor (MatrixFactorization S w) (MatrixFactorization S w)

          The parity shift swaps the projective components and negates both differentials.

          Equations
          Instances For
            source
            theorem TauCeti.MatrixFactorization.parityShift_comp_inclusion {S : Type u} [CommRing S] {w : S} :
            parityShift.comp inclusion = inclusion.comp (CurvedDuplex.parityShift (FGModuleCat S) w)

            The parity shift commutes with the inclusion into curved duplexes.

            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_obj {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
            (parityShift.obj X).obj = (CurvedDuplex.parityShift (FGModuleCat S) w).obj X.obj
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_map_hom {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
            (parityShift.map f).hom = (CurvedDuplex.parityShift (FGModuleCat S) w).map f.hom
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_obj_X₀ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
            (parityShift.obj X).obj.X₀ = X.obj.X₁
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_obj_X₁ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
            (parityShift.obj X).obj.X₁ = X.obj.X₀
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_obj_d₀ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
            (parityShift.obj X).obj.d₀ = -X.obj.d₁
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_obj_d₁ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
            (parityShift.obj X).obj.d₁ = -X.obj.d₀
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_map_f₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
            (parityShift.map f).hom.f₀ = f.hom.f₁
            source
            @[simp]
            theorem TauCeti.MatrixFactorization.parityShift_map_f₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
            (parityShift.map f).hom.f₁ = f.hom.f₀
            source
            instance TauCeti.MatrixFactorization.instAdditiveParityShift {S : Type u} [CommRing S] {w : S} :
            parityShift.Additive
            source
            def TauCeti.MatrixFactorization.parityShiftCompParityShiftIso {S : Type u} [CommRing S] {w : S} :
            parityShift.comp parityShift ≅ CategoryTheory.Functor.id (MatrixFactorization S w)

            Applying the parity shift twice gives the original matrix factorization.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem TauCeti.MatrixFactorization.parityShiftCompParityShiftIso_hom_app_hom {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
              (parityShiftCompParityShiftIso.hom.app X).hom = (CurvedDuplex.parityShiftCompParityShiftIso (FGModuleCat S) w).hom.app X.obj
              source
              @[simp]
              theorem TauCeti.MatrixFactorization.parityShiftCompParityShiftIso_inv_app_hom {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
              (parityShiftCompParityShiftIso.inv.app X).hom = (CurvedDuplex.parityShiftCompParityShiftIso (FGModuleCat S) w).inv.app X.obj
              source
              def TauCeti.MatrixFactorization.parityShiftEquivalence {S : Type u} [CommRing S] {w : S} :
              MatrixFactorization S w ≌ MatrixFactorization S w

              The parity shift is a self-equivalence of finite-projective matrix factorizations.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem TauCeti.MatrixFactorization.parityShiftEquivalence_inverse {S : Type u} [CommRing S] {w : S} :
                parityShiftEquivalence.inverse = parityShift
                source
                @[simp]
                theorem TauCeti.MatrixFactorization.parityShiftEquivalence_counitIso {S : Type u} [CommRing S] {w : S} :
                parityShiftEquivalence.counitIso = parityShiftCompParityShiftIso
                source
                @[simp]
                theorem TauCeti.MatrixFactorization.parityShiftEquivalence_unitIso {S : Type u} [CommRing S] {w : S} :
                parityShiftEquivalence.unitIso = parityShiftCompParityShiftIso.symm
                source
                @[simp]
                theorem TauCeti.MatrixFactorization.parityShiftEquivalence_functor {S : Type u} [CommRing S] {w : S} :
                parityShiftEquivalence.functor = parityShift
                source
                instance TauCeti.MatrixFactorization.instAdditiveFunctorParityShiftEquivalence {S : Type u} [CommRing S] {w : S} :
                parityShiftEquivalence.functor.Additive
                source
                def TauCeti.MatrixFactorization.disk {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] :
                MatrixFactorization S w

                The elementary contractible factorization on a finitely generated projective module.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.MatrixFactorization.disk_obj {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] :
                  (disk P).obj = CurvedDuplex.disk w P
                  source
                  def TauCeti.MatrixFactorization.diskHomEquiv {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] (X : MatrixFactorization S w) :
                  (disk P ⟶ X) ≃ₗ[S] P ⟶ X.obj.X₀

                  A map from an elementary disk is determined by its even component.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.MatrixFactorization.diskHomEquiv_apply {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] (X : MatrixFactorization S w) (f : disk P ⟶ X) :
                    (diskHomEquiv P X) f = f.hom.f₀
                    source
                    @[simp]
                    theorem TauCeti.MatrixFactorization.diskHomEquiv_symm_apply_hom_f₀ {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] (X : MatrixFactorization S w) (g : P ⟶ X.obj.X₀) :
                    ((diskHomEquiv P X).symm g).hom.f₀ = g
                    source
                    @[simp]
                    theorem TauCeti.MatrixFactorization.diskHomEquiv_symm_apply_hom_f₁ {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] (X : MatrixFactorization S w) (g : P ⟶ X.obj.X₀) :
                    ((diskHomEquiv P X).symm g).hom.f₁ = CategoryTheory.CategoryStruct.comp g X.obj.d₀
                    source
                    def TauCeti.MatrixFactorization.rankOne {S : Type u} [CommRing S] {w : S} (a b : S) (h : a * b = w) :
                    MatrixFactorization S w

                    The rank-one matrix factorization S --a--> S --b--> S of w = a b. Its components are finite free, with no regularity assumption on S or w.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.MatrixFactorization.rankOne_d₀ {S : Type u} [CommRing S] {w : S} (a b : S) (h : a * b = w) :
                      (rankOne a b h).obj.d₀ = a • CategoryTheory.CategoryStruct.id ↧S
                      source
                      @[simp]
                      theorem TauCeti.MatrixFactorization.rankOne_d₁ {S : Type u} [CommRing S] {w : S} (a b : S) (h : a * b = w) :
                      (rankOne a b h).obj.d₁ = b • CategoryTheory.CategoryStruct.id ↧S
                      source
                      @[simp]
                      theorem TauCeti.MatrixFactorization.rankOne_X₀ {S : Type u} [CommRing S] {w : S} (a b : S) (h : a * b = w) :
                      (rankOne a b h).obj.X₀ = ↧S
                      source
                      @[simp]
                      theorem TauCeti.MatrixFactorization.rankOne_X₁ {S : Type u} [CommRing S] {w : S} (a b : S) (h : a * b = w) :
                      (rankOne a b h).obj.X₁ = ↧S

                      Homotopies #

                      source
                      def TauCeti.MatrixFactorization.nullHomotopic {S : Type u} [CommRing S] {w : S} :
                      MorphismIdeal (MatrixFactorization S w)

                      The ideal of morphisms of finite-projective matrix factorizations that are null-homotopic as curved duplex maps. Since the subcategory is full, these are exactly the boundaries of odd maps between the underlying finite projective components.

                      Equations
                      Instances For
                        source
                        theorem TauCeti.MatrixFactorization.comap_parityShift_nullHomotopic {S : Type u} [CommRing S] {w : S} :
                        nullHomotopic.comap parityShift = nullHomotopic

                        Null-homotopic maps are exactly the maps whose parity shifts are null-homotopic.

                        source
                        @[reducible, inline]
                        abbrev TauCeti.MatrixFactorization.HomotopyCategory {S : Type u} [CommRing S] {w : S} :
                        Type (u + 1)

                        The homotopy category of finite-projective matrix factorizations.

                        Equations
                        Instances For
                          source
                          noncomputable def TauCeti.MatrixFactorization.HomotopyCategory.parityShiftEquivalence {S : Type u} [CommRing S] {w : S} :
                          HomotopyCategory ≌ HomotopyCategory

                          The parity shift induces an equivalence of matrix-factorization homotopy categories.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem TauCeti.MatrixFactorization.HomotopyCategory.quotientFunctor_comp_parityShiftEquivalence_functor {S : Type u} [CommRing S] {w : S} :
                            nullHomotopic.quotientFunctor.comp parityShiftEquivalence.functor = parityShift.comp nullHomotopic.quotientFunctor

                            Parity shift commutes with the quotient functor.

                            source
                            instance TauCeti.MatrixFactorization.instAdditiveHomotopyCategoryFunctorParityShiftEquivalence {S : Type u} [CommRing S] {w : S} :
                            HomotopyCategory.parityShiftEquivalence.functor.Additive
                            source
                            @[simp]
                            theorem TauCeti.MatrixFactorization.HomotopyCategory.parityShiftEquivalence_functor_obj_quotientFunctor_obj {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) :
                            parityShiftEquivalence.functor.obj (nullHomotopic.quotientFunctor.obj X) = nullHomotopic.quotientFunctor.obj (parityShift.obj X)

                            On the image of a factorization, the parity shift of the homotopy category is the image of its parity shift.

                            source
                            @[simp]
                            theorem TauCeti.MatrixFactorization.mem_nullHomotopic_iff {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) :
                            f ∈ nullHomotopic.hom X Y ↔ ∃ (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀), CurvedDuplex.nullHomotopicMap h₀ h₁ = f.hom

                            A closed even map is null-homotopic precisely when it is the boundary of an odd map.

                            source
                            theorem TauCeti.MatrixFactorization.id_disk_mem_nullHomotopic {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] :
                            CategoryTheory.CategoryStruct.id (disk P) ∈ nullHomotopic.hom (disk P) (disk P)

                            The identity of an elementary disk is null-homotopic.

                            source
                            theorem TauCeti.MatrixFactorization.isZero_quotientFunctor_obj_disk {S : Type u} [CommRing S] {w : S} (P : FGModuleCat S) [Module.Projective S ↑P] :
                            CategoryTheory.Limits.IsZero (nullHomotopic.quotientFunctor.obj (disk P))

                            An elementary disk is zero in the homotopy category.

                            source
                            theorem TauCeti.MatrixFactorization.quotientFunctor_map_eq_quotientFunctor_map_iff {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f g : X ⟶ Y) :
                            nullHomotopic.quotientFunctor.map f = nullHomotopic.quotientFunctor.map g ↔ ∃ (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀), CurvedDuplex.nullHomotopicMap h₀ h₁ = (f - g).hom

                            Two morphisms of finite-projective matrix factorizations have the same image in the homotopy category exactly when their difference is the boundary of an odd map.