Direct sums of finite-projective matrix factorizations

The componentwise direct sum of finite-projective matrix factorizations is again finite projective. Its projections exhibit it as a categorical product and hence, in this preadditive category, a binary biproduct. This provides the additive sums used by the homotopy and Frobenius structures on matrix factorizations.

The direct-sum operation is the finite-projective case of the direct sum of curved duplexes; the matrix-factorization convention follows Eisenbud, Homological algebra on a complete intersection, Section 5.

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

The componentwise direct sum of two finite-projective matrix factorizations.

Equations

• X.biprod Y = TauCeti.MatrixFactorization.ofCurvedDuplex (X.obj.biprod Y.obj) ⋯ ⋯

@[simp]

theorem TauCeti.MatrixFactorization.biprod_obj {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprod Y).obj = X.obj.biprod Y.obj

@[simp]

theorem TauCeti.MatrixFactorization.biprod_X₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprod Y).obj.X₀ = (X.obj.X₀ ⊞ Y.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.biprod_X₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprod Y).obj.X₁ = (X.obj.X₁ ⊞ Y.obj.X₁)

@[simp]

theorem TauCeti.MatrixFactorization.biprod_d₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprod Y).obj.d₀ = CategoryTheory.Limits.biprod.map X.obj.d₀ Y.obj.d₀

@[simp]

theorem TauCeti.MatrixFactorization.biprod_d₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprod Y).obj.d₁ = CategoryTheory.Limits.biprod.map X.obj.d₁ Y.obj.d₁

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

Projection to the first summand.

Equations

• X.biprodFst Y = { hom := X.obj.biprodFst Y.obj }

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

Projection to the second summand.

Equations

• X.biprodSnd Y = { hom := X.obj.biprodSnd Y.obj }

noncomputable def TauCeti.MatrixFactorization.biprodLift {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} (f : Z ⟶ X) (g : Z ⟶ Y) : Z ⟶ X.biprod Y

The map into a direct sum induced by maps into its summands.

Equations

• TauCeti.MatrixFactorization.biprodLift f g = { hom := TauCeti.CurvedDuplex.biprodLift f.hom g.hom }

@[simp]

theorem TauCeti.MatrixFactorization.biprodFst_hom_f₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodFst Y).hom.f₀ = CategoryTheory.Limits.biprod.fst

@[simp]

theorem TauCeti.MatrixFactorization.biprodFst_hom_f₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodFst Y).hom.f₁ = CategoryTheory.Limits.biprod.fst

@[simp]

theorem TauCeti.MatrixFactorization.biprodSnd_hom_f₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodSnd Y).hom.f₀ = CategoryTheory.Limits.biprod.snd

@[simp]

theorem TauCeti.MatrixFactorization.biprodSnd_hom_f₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodSnd Y).hom.f₁ = CategoryTheory.Limits.biprod.snd

@[simp]

theorem TauCeti.MatrixFactorization.biprodLift_hom_f₀ {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} (f : Z ⟶ X) (g : Z ⟶ Y) : (biprodLift f g).hom.f₀ = CategoryTheory.Limits.biprod.lift f.hom.f₀ g.hom.f₀

@[simp]

theorem TauCeti.MatrixFactorization.biprodLift_hom_f₁ {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} (f : Z ⟶ X) (g : Z ⟶ Y) : (biprodLift f g).hom.f₁ = CategoryTheory.Limits.biprod.lift f.hom.f₁ g.hom.f₁

@[simp]

theorem TauCeti.MatrixFactorization.biprodLift_fst {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} (f : Z ⟶ X) (g : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp (biprodLift f g) (X.biprodFst Y) = f

@[simp]

theorem TauCeti.MatrixFactorization.biprodLift_snd {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} (f : Z ⟶ X) (g : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp (biprodLift f g) (X.biprodSnd Y) = g

theorem TauCeti.MatrixFactorization.biprod_hom_ext {S : Type u} [CommRing S] {w : S} {Z X Y : MatrixFactorization S w} {f g : Z ⟶ X.biprod Y} (h₀ : CategoryTheory.CategoryStruct.comp f (X.biprodFst Y) = CategoryTheory.CategoryStruct.comp g (X.biprodFst Y)) (h₁ : CategoryTheory.CategoryStruct.comp f (X.biprodSnd Y) = CategoryTheory.CategoryStruct.comp g (X.biprodSnd Y)) : f = g

Maps into a direct sum are determined by their projections.

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

Inclusion of the first matrix factorization into the componentwise direct sum.

Equations

• X.biprodInl Y = { hom := X.obj.biprodInl Y.obj }

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

Inclusion of the second matrix factorization into the componentwise direct sum.

Equations

• X.biprodInr Y = { hom := X.obj.biprodInr Y.obj }

noncomputable def TauCeti.MatrixFactorization.biprodDesc {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} (f : X ⟶ Z) (g : Y ⟶ Z) : X.biprod Y ⟶ Z

Maps out of both summands induce a map out of their direct sum.

Equations

• TauCeti.MatrixFactorization.biprodDesc f g = { hom := TauCeti.CurvedDuplex.biprodDesc f.hom g.hom }

@[simp]

theorem TauCeti.MatrixFactorization.biprodInl_hom_f₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodInl Y).hom.f₀ = CategoryTheory.Limits.biprod.inl

@[simp]

theorem TauCeti.MatrixFactorization.biprodInl_hom_f₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodInl Y).hom.f₁ = CategoryTheory.Limits.biprod.inl

@[simp]

theorem TauCeti.MatrixFactorization.biprodInr_hom_f₀ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodInr Y).hom.f₀ = CategoryTheory.Limits.biprod.inr

@[simp]

theorem TauCeti.MatrixFactorization.biprodInr_hom_f₁ {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : (X.biprodInr Y).hom.f₁ = CategoryTheory.Limits.biprod.inr

@[simp]

theorem TauCeti.MatrixFactorization.biprodDesc_hom_f₀ {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} (f : X ⟶ Z) (g : Y ⟶ Z) : (biprodDesc f g).hom.f₀ = CategoryTheory.Limits.biprod.desc f.hom.f₀ g.hom.f₀

@[simp]

theorem TauCeti.MatrixFactorization.biprodDesc_hom_f₁ {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} (f : X ⟶ Z) (g : Y ⟶ Z) : (biprodDesc f g).hom.f₁ = CategoryTheory.Limits.biprod.desc f.hom.f₁ g.hom.f₁

@[simp]

theorem TauCeti.MatrixFactorization.biprodInl_desc {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (biprodDesc f g) = f

@[simp]

theorem TauCeti.MatrixFactorization.biprodInr_desc {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (biprodDesc f g) = g

@[simp]

theorem TauCeti.MatrixFactorization.biprodInl_fst {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (X.biprodFst Y) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem TauCeti.MatrixFactorization.biprodInl_snd {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (X.biprodSnd Y) = 0

@[simp]

theorem TauCeti.MatrixFactorization.biprodInr_fst {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (X.biprodFst Y) = 0

@[simp]

theorem TauCeti.MatrixFactorization.biprodInr_snd {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (X.biprodSnd Y) = CategoryTheory.CategoryStruct.id Y

theorem TauCeti.MatrixFactorization.biprod_hom_ext' {S : Type u} [CommRing S] {w : S} {X Y Z : MatrixFactorization S w} {f g : X.biprod Y ⟶ Z} (h₀ : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) f = CategoryTheory.CategoryStruct.comp (X.biprodInl Y) g) (h₁ : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) f = CategoryTheory.CategoryStruct.comp (X.biprodInr Y) g) : f = g

Maps from a direct sum are determined by their restrictions to both summands.

instance TauCeti.MatrixFactorization.hasBinaryProduct {S : Type u} [CommRing S] {w : S} (X Y : MatrixFactorization S w) : CategoryTheory.Limits.HasBinaryProduct X Y

Finite-projective matrix factorizations have componentwise binary products.

instance TauCeti.MatrixFactorization.hasBinaryProducts {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.HasBinaryProducts (MatrixFactorization S w)

Finite-projective matrix factorizations have binary products.

instance TauCeti.MatrixFactorization.hasBinaryBiproducts {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.HasBinaryBiproducts (MatrixFactorization S w)

Finite-projective matrix factorizations have binary biproducts.

noncomputable def TauCeti.MatrixFactorization.zero {S : Type u} [CommRing S] {w : S} : MatrixFactorization S w

The zero matrix factorization has the zero module in both parities.

Equations

• TauCeti.MatrixFactorization.zero = TauCeti.MatrixFactorization.ofCurvedDuplex { X₀ := ↧PUnit.{?u.1 + 1}, X₁ := ↧PUnit.{?u.1 + 1}, d₀ := 0, d₁ := 0, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ } ⋯ ⋯

@[simp]

theorem TauCeti.MatrixFactorization.zero_X₀ {S : Type u} [CommRing S] {w : S} : zero.obj.X₀ = ↧PUnit.{u + 1}

@[simp]

theorem TauCeti.MatrixFactorization.zero_X₁ {S : Type u} [CommRing S] {w : S} : zero.obj.X₁ = ↧PUnit.{u + 1}

@[simp]

theorem TauCeti.MatrixFactorization.zero_d₀ {S : Type u} [CommRing S] {w : S} : zero.obj.d₀ = 0

@[simp]

theorem TauCeti.MatrixFactorization.zero_d₁ {S : Type u} [CommRing S] {w : S} : zero.obj.d₁ = 0

theorem TauCeti.MatrixFactorization.isZero_zero {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.IsZero zero

The zero matrix factorization is both initial and terminal.

instance TauCeti.MatrixFactorization.hasZeroObject {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.HasZeroObject (MatrixFactorization S w)

Finite-projective matrix factorizations have a zero object.

instance TauCeti.MatrixFactorization.hasFiniteProducts {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.HasFiniteProducts (MatrixFactorization S w)

Finite-projective matrix factorizations have finite products.

instance TauCeti.MatrixFactorization.hasFiniteBiproducts {S : Type u} [CommRing S] {w : S} : CategoryTheory.Limits.HasFiniteBiproducts (MatrixFactorization S w)

Finite-projective matrix factorizations have finite biproducts.