Reducing matrix factorizations to two-periodic complexes

If a ring homomorphism sends the potential of a matrix factorization to zero, extension of scalars turns its two curved differential equations into square-zero equations. In particular, reduction modulo the ideal generated by the potential gives a two-periodic complex over the hypersurface quotient. The construction acts on closed even morphisms and hence is a functor.

Scalar extension first gives a finite-projective matrix factorization of the image potential. When that image is zero, forgetting finite projectivity gives a square-zero duplex and a two-periodic complex. The reduction modulo the potential is the periodic complex used in Eisenbud, Homological algebra on a complete intersection, with an application to group representations, Trans. Amer. Math. Soc. 260 (1980), Section 5.

noncomputable def TauCeti.MatrixFactorization.baseChangeFunctor {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) : CategoryTheory.Functor (MatrixFactorization S w) (MatrixFactorization T (f w))

Extension of scalars carries a finite-projective matrix factorization of w to one of f w, without requiring the potential to vanish.

Equations

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

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_obj_X₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (X : MatrixFactorization S w) : ((baseChangeFunctor f).obj X).obj.X₀.obj = (ModuleCat.extendScalars f).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₀)

The even object of the scalar-extended factorization is the scalar extension of the original even module.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_obj_X₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (X : MatrixFactorization S w) : ((baseChangeFunctor f).obj X).obj.X₁.obj = (ModuleCat.extendScalars f).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₁)

The odd object of the scalar-extended factorization is the scalar extension of the original odd module.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_obj_d₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (X : MatrixFactorization S w) : (CategoryTheory.forget₂ (FGModuleCat T) (ModuleCat T)).map ((baseChangeFunctor f).obj X).obj.d₀ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₀)

The even-to-odd differential of the scalar-extended factorization is the scalar extension of d₀.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_obj_d₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (X : MatrixFactorization S w) : (CategoryTheory.forget₂ (FGModuleCat T) (ModuleCat T)).map ((baseChangeFunctor f).obj X).obj.d₁ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₁)

The odd-to-even differential of the scalar-extended factorization is the scalar extension of d₁.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_map_f₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : (CategoryTheory.forget₂ (FGModuleCat T) (ModuleCat T)).map ((baseChangeFunctor f).map g).hom.f₀ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₀)

The even component of a map in the scalar-extended factorization is the scalar extension of f₀.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeFunctor_map_f₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : (CategoryTheory.forget₂ (FGModuleCat T) (ModuleCat T)).map ((baseChangeFunctor f).map g).hom.f₁ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₁)

The odd component of a map in the scalar-extended factorization is the scalar extension of f₁.

instance TauCeti.MatrixFactorization.baseChangeFunctor_additive {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) : (baseChangeFunctor f).Additive

Scalar extension preserves addition of closed even maps.

noncomputable def TauCeti.MatrixFactorization.baseChangeToCurvedDuplex {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) : CategoryTheory.Functor (MatrixFactorization S w) (CurvedDuplex (ModuleCat T) 0)

Extension of scalars along a map killing the potential sends a finite-projective matrix factorization to a square-zero duplex. The target components are the tensor products of the original components with the target ring.

Equations

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

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_obj_X₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((baseChangeToCurvedDuplex f hw).obj X).X₀ = (ModuleCat.extendScalars f).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₀)

The even object of the square-zero duplex is the scalar extension of the original even module.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_obj_X₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((baseChangeToCurvedDuplex f hw).obj X).X₁ = (ModuleCat.extendScalars f).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₁)

The odd object of the square-zero duplex is the scalar extension of the original odd module.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_obj_d₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((baseChangeToCurvedDuplex f hw).obj X).d₀ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₀)

The even-to-odd differential of the square-zero duplex is the scalar extension of d₀.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_obj_d₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((baseChangeToCurvedDuplex f hw).obj X).d₁ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₁)

The odd-to-even differential of the square-zero duplex is the scalar extension of d₁.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_map_f₀ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : ((baseChangeToCurvedDuplex f hw).map g).f₀ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₀)

The even component of a map in the square-zero duplex is the scalar extension of f₀.

@[simp]

theorem TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_map_f₁ {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : ((baseChangeToCurvedDuplex f hw).map g).f₁ = (ModuleCat.extendScalars f).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₁)

The odd component of a map in the square-zero duplex is the scalar extension of f₁.

instance TauCeti.MatrixFactorization.baseChangeToCurvedDuplex_additive {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) : (baseChangeToCurvedDuplex f hw).Additive

Extension of scalars is additive on closed even maps of matrix factorizations.

noncomputable def TauCeti.MatrixFactorization.toPeriodicComplex {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) : CategoryTheory.Functor (MatrixFactorization S w) (HomologicalComplex (ModuleCat T) (ComplexShape.up (ZMod 2)))

The two-periodic complex obtained by reducing a matrix factorization along a ring map that kills its potential.

Equations

• TauCeti.MatrixFactorization.toPeriodicComplex f hw = (TauCeti.MatrixFactorization.baseChangeToCurvedDuplex f hw).comp (TauCeti.CurvedDuplex.toPeriodicComplex (ModuleCat T) T)

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_obj_X_zero {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((toPeriodicComplex f hw).obj X).X 0 = ((baseChangeToCurvedDuplex f hw).obj X).X₀

The zero component of the two-periodic complex is the even component of the square-zero duplex.

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_obj_X_one {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((toPeriodicComplex f hw).obj X).X 1 = ((baseChangeToCurvedDuplex f hw).obj X).X₁

The one component of the two-periodic complex is the odd component of the square-zero duplex.

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_obj_d_zero_one {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((toPeriodicComplex f hw).obj X).d 0 1 = ((baseChangeToCurvedDuplex f hw).obj X).d₀

The differential from zero to one is the even differential of the square-zero duplex.

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_obj_d_one_zero {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) (X : MatrixFactorization S w) : ((toPeriodicComplex f hw).obj X).d 1 0 = ((baseChangeToCurvedDuplex f hw).obj X).d₁

The differential from one to zero is the odd differential of the square-zero duplex.

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_map_f_zero {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : ((toPeriodicComplex f hw).map g).f 0 = ((baseChangeToCurvedDuplex f hw).map g).f₀

The zero component of a periodic map is the even component of the duplex map.

@[simp]

theorem TauCeti.MatrixFactorization.toPeriodicComplex_map_f_one {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) {X Y : MatrixFactorization S w} (g : X ⟶ Y) : ((toPeriodicComplex f hw).map g).f 1 = ((baseChangeToCurvedDuplex f hw).map g).f₁

The one component of a periodic map is the odd component of the duplex map.

instance TauCeti.MatrixFactorization.toPeriodicComplex_additive {S T : Type u} [CommRing S] [CommRing T] {w : S} (f : S →+* T) (hw : f w = 0) : (toPeriodicComplex f hw).Additive

noncomputable def TauCeti.MatrixFactorization.quotientPeriodicComplex {S : Type u} [CommRing S] {w : S} : CategoryTheory.Functor (MatrixFactorization S w) (HomologicalComplex (ModuleCat (S ⧸ Ideal.span {w})) (ComplexShape.up (ZMod 2)))

The two-periodic complex over S/(w) associated to a matrix factorization of w.

Equations

• TauCeti.MatrixFactorization.quotientPeriodicComplex = TauCeti.MatrixFactorization.toPeriodicComplex (Ideal.Quotient.mk (Ideal.span {w})) ⋯

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_obj_X_zero {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (quotientPeriodicComplex.obj X).X 0 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₀)

The even object of the hypersurface quotient complex is the scalar extension of the original even module.

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_obj_X_one {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (quotientPeriodicComplex.obj X).X 1 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).obj ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).obj X.obj.X₁)

The odd object of the hypersurface quotient complex is the scalar extension of the original odd module.

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_obj_d_zero_one {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (quotientPeriodicComplex.obj X).d 0 1 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₀)

The zero-to-one differential of the hypersurface quotient complex is the scalar extension of d₀.

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_obj_d_one_zero {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : (quotientPeriodicComplex.obj X).d 1 0 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map X.obj.d₁)

The one-to-zero differential of the hypersurface quotient complex is the scalar extension of d₁.

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_map_f_zero {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (g : X ⟶ Y) : (quotientPeriodicComplex.map g).f 0 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₀)

The zero component of a map in the hypersurface quotient complex is the scalar extension of f₀.

@[simp]

theorem TauCeti.MatrixFactorization.quotientPeriodicComplex_map_f_one {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (g : X ⟶ Y) : (quotientPeriodicComplex.map g).f 1 = (ModuleCat.extendScalars (Ideal.Quotient.mk (Ideal.span {w}))).map ((CategoryTheory.forget₂ (FGModuleCat S) (ModuleCat S)).map g.hom.f₁)

The one component of a map in the hypersurface quotient complex is the scalar extension of f₁.

instance TauCeti.MatrixFactorization.quotientPeriodicComplex_additive {S : Type u} [CommRing S] {w : S} : quotientPeriodicComplex.Additive