Factoring matrix-factorization homotopies through disks

The disk sum on the two components of a finite-projective matrix factorization is again finite projective. Every null-homotopic morphism factors through this contractible object, and every map factoring through it is null-homotopic. A contractible factorization is therefore a retract of such a sum. These facts are the factorization input for comparing the homotopy category with the stable category of the componentwise split exact structure.

The disk sum is functorial (diskSumMap), and the projection diskSumToParityShift onto the parity shift completes the inclusion toDiskSum to a componentwise split short complex X ⟶ diskSum X ⟶ X[1], which presents the stable suspension of X.

The disk construction follows Frenkel, Khovanov and Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Sections 2–3.

noncomputable def TauCeti.MatrixFactorization.diskSum {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : MatrixFactorization S w

The direct sum of the odd disk and the parity-shifted even disk of a matrix factorization. Both components are the finite projective module X₁ ⊞ X₀.

Equations

• X.diskSum = TauCeti.MatrixFactorization.ofCurvedDuplex X.obj.diskSum ⋯ ⋯

@[simp]

theorem TauCeti.MatrixFactorization.diskSum_obj {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum.obj = X.obj.diskSum

@[simp]

theorem TauCeti.MatrixFactorization.diskSum_X₀ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum.obj.X₀ = (X.obj.X₁ ⊞ X.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.diskSum_X₁ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum.obj.X₁ = (X.obj.X₁ ⊞ X.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.diskSum_d₀ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum.obj.d₀ = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X.obj.X₁) (-(w • CategoryTheory.CategoryStruct.id X.obj.X₀))

@[simp]

theorem TauCeti.MatrixFactorization.diskSum_d₁ {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum.obj.d₁ = CategoryTheory.Limits.biprod.map (w • CategoryTheory.CategoryStruct.id X.obj.X₁) (-CategoryTheory.CategoryStruct.id X.obj.X₀)

noncomputable def TauCeti.MatrixFactorization.toDiskSum {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X ⟶ X.diskSum

The canonical map from a factorization into its disk sum.

Equations

• X.toDiskSum = { hom := X.obj.toDiskSum }

noncomputable def TauCeti.MatrixFactorization.fromDiskSum {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀) : X.diskSum ⟶ Y

An odd homotopy determines a map from the disk sum to its target.

Equations

• TauCeti.MatrixFactorization.fromDiskSum h₀ h₁ = { hom := TauCeti.CurvedDuplex.fromDiskSum h₀ h₁ }

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_hom {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.toDiskSum.hom = X.obj.toDiskSum

@[simp]

theorem TauCeti.MatrixFactorization.fromDiskSum_hom_f₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀) : (fromDiskSum h₀ h₁).hom.f₀ = CategoryTheory.Limits.biprod.desc h₁ (CategoryTheory.CategoryStruct.comp h₀ Y.obj.d₁)

@[simp]

theorem TauCeti.MatrixFactorization.fromDiskSum_hom_f₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀) : (fromDiskSum h₀ h₁).hom.f₁ = CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.comp h₁ Y.obj.d₀) (-h₀)

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_comp_fromDiskSum {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (h₀ : X.obj.X₀ ⟶ Y.obj.X₁) (h₁ : X.obj.X₁ ⟶ Y.obj.X₀) : CategoryTheory.CategoryStruct.comp X.toDiskSum (fromDiskSum h₀ h₁) = { hom := CurvedDuplex.nullHomotopicMap h₀ h₁ }

The composite through the disk sum is the boundary of the given odd homotopy.

noncomputable def TauCeti.MatrixFactorization.diskSumToParityShift {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSum ⟶ parityShift.obj X

The projection from the disk sum of a factorization onto its parity shift. Together with toDiskSum X it forms a short complex X ⟶ diskSum X ⟶ X[1] which splits in both components.

Equations

• X.diskSumToParityShift = { hom := X.obj.diskSumToParityShift }

@[simp]

theorem TauCeti.MatrixFactorization.diskSumToParityShift_hom {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : X.diskSumToParityShift.hom = X.obj.diskSumToParityShift

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_comp_diskSumToParityShift {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : CategoryTheory.CategoryStruct.comp X.toDiskSum X.diskSumToParityShift = 0

The inclusion into the disk sum, followed by the projection onto the parity shift, vanishes.

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_comp_diskSumToParityShift_assoc {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) {Z : MatrixFactorization S w} (h : parityShift.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp X.toDiskSum (CategoryTheory.CategoryStruct.comp X.diskSumToParityShift h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion into the disk sum, followed by the projection onto the parity shift, vanishes.

noncomputable def TauCeti.MatrixFactorization.diskSumMap {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : X.diskSum ⟶ Y.diskSum

The map induced on disk sums by a morphism of matrix factorizations.

Equations

• TauCeti.MatrixFactorization.diskSumMap f = { hom := TauCeti.CurvedDuplex.diskSumMap f.hom }

@[simp]

theorem TauCeti.MatrixFactorization.diskSumMap_hom {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (diskSumMap f).hom = CurvedDuplex.diskSumMap f.hom

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_comp_diskSumMap {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.toDiskSum (diskSumMap f) = CategoryTheory.CategoryStruct.comp f Y.toDiskSum

The inclusion into the disk sum is natural.

@[simp]

theorem TauCeti.MatrixFactorization.toDiskSum_comp_diskSumMap_assoc {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) {Z : MatrixFactorization S w} (h : Y.diskSum ⟶ Z) : CategoryTheory.CategoryStruct.comp X.toDiskSum (CategoryTheory.CategoryStruct.comp (diskSumMap f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.toDiskSum h)

The inclusion into the disk sum is natural.

@[simp]

theorem TauCeti.MatrixFactorization.diskSumToParityShift_comp_parityShift_map {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.diskSumToParityShift (parityShift.map f) = CategoryTheory.CategoryStruct.comp (diskSumMap f) Y.diskSumToParityShift

The projection from the disk sum onto the parity shift is natural.

@[simp]

theorem TauCeti.MatrixFactorization.diskSumToParityShift_comp_parityShift_map_assoc {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) {Z : MatrixFactorization S w} (h : parityShift.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp X.diskSumToParityShift (CategoryTheory.CategoryStruct.comp (parityShift.map f) h) = CategoryTheory.CategoryStruct.comp (diskSumMap f) (CategoryTheory.CategoryStruct.comp Y.diskSumToParityShift h)

The projection from the disk sum onto the parity shift is natural.

theorem TauCeti.MatrixFactorization.id_diskSum_mem_nullHomotopic {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) : CategoryTheory.CategoryStruct.id X.diskSum ∈ nullHomotopic.hom X.diskSum X.diskSum

The disk sum is contractible in the matrix-factorization homotopy category.

theorem TauCeti.MatrixFactorization.mem_nullHomotopic_iff_factors_diskSum {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : f ∈ nullHomotopic.hom X Y ↔ ∃ (a : X ⟶ X.diskSum) (b : X.diskSum ⟶ Y), CategoryTheory.CategoryStruct.comp a b = f

A map of matrix factorizations is null-homotopic exactly when it factors through the disk sum on its source.

noncomputable def TauCeti.MatrixFactorization.retractDiskSum {S : Type u} [CommRing S] {w : S} (X : MatrixFactorization S w) (h : CategoryTheory.CategoryStruct.id X ∈ nullHomotopic.hom X X) : CategoryTheory.Retract X X.diskSum

A contractible finite-projective matrix factorization is a retract of the disk sum on its two components.

Equations

• X.retractDiskSum h = { i := Classical.choose ⋯, r := Classical.choose ⋯, retract := ⋯ }