Mapping cones of finite-projective matrix factorizations

The cone of a morphism of matrix factorizations is the cone of its underlying curved duplex. Its components are biproducts of finite projective modules, so it remains a finite-projective matrix factorization. The usual inclusion and projection give the cone sequence inside the matrix-factorization category, and the cone of an isomorphism is contractible.

The block-matrix cone convention follows I. Frenkel, M. Khovanov, and O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compositio Mathematica 141 (2005), Sections 2–3.

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

The mapping cone of a morphism of finite-projective matrix factorizations.

Equations

• TauCeti.MatrixFactorization.cone f = TauCeti.MatrixFactorization.ofCurvedDuplex (TauCeti.CurvedDuplex.cone f.hom) ⋯ ⋯

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

@[simp]

theorem TauCeti.MatrixFactorization.cone_obj_X₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (cone f).obj.X₀ = (X.obj.X₁ ⊞ Y.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.cone_obj_X₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (cone f).obj.X₁ = (X.obj.X₀ ⊞ Y.obj.X₁)

@[simp]

theorem TauCeti.MatrixFactorization.cone_obj_d₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (cone f).obj.d₀ = CurvedDuplex.coneD₀ f.hom

@[simp]

theorem TauCeti.MatrixFactorization.cone_obj_d₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (cone f).obj.d₁ = CurvedDuplex.coneD₁ f.hom

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

The canonical inclusion of the codomain into the cone.

Equations

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

noncomputable def TauCeti.MatrixFactorization.coneProjection {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : cone f ⟶ parityShift.obj X

The canonical projection of the cone onto the parity shift of the domain.

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def TauCeti.MatrixFactorization.coneParityShiftIso {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : parityShift.obj (cone f) ≅ cone (parityShift.map f)

Parity shift commutes with mapping cones, with a sign on the codomain summand.

Equations

• TauCeti.MatrixFactorization.coneParityShiftIso f = (TauCeti.MatrixFactorization.isProjective S w).isoMk (TauCeti.CurvedDuplex.coneParityShiftIso f.hom)

@[simp]

theorem TauCeti.MatrixFactorization.coneParityShiftIso_hom_hom_f₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (coneParityShiftIso f).hom.hom.f₀ = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X.obj.X₀) (-CategoryTheory.CategoryStruct.id Y.obj.X₁)

@[simp]

theorem TauCeti.MatrixFactorization.coneParityShiftIso_hom_hom_f₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (coneParityShiftIso f).hom.hom.f₁ = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X.obj.X₁) (-CategoryTheory.CategoryStruct.id Y.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.coneParityShiftIso_inv_hom_f₀ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (coneParityShiftIso f).inv.hom.f₀ = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X.obj.X₀) (-CategoryTheory.CategoryStruct.id Y.obj.X₁)

@[simp]

theorem TauCeti.MatrixFactorization.coneParityShiftIso_inv_hom_f₁ {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : (coneParityShiftIso f).inv.hom.f₁ = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X.obj.X₁) (-CategoryTheory.CategoryStruct.id Y.obj.X₀)

@[simp]

theorem TauCeti.MatrixFactorization.coneInclusion_comp_coneProjection {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneProjection f) = 0

The inclusion followed by the projection is zero.

@[simp]

theorem TauCeti.MatrixFactorization.coneInclusion_comp_coneProjection_assoc {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) {Z : MatrixFactorization S w} (h : parityShift.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (CategoryTheory.CategoryStruct.comp (coneProjection f) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion followed by the projection is zero.

theorem TauCeti.MatrixFactorization.comp_coneInclusion_mem_nullHomotopic {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (coneInclusion f) ∈ nullHomotopic.hom X (cone f)

The composite from the domain to its cone is null-homotopic.

@[simp]

theorem TauCeti.MatrixFactorization.quotientFunctor_map_comp_coneInclusion {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (nullHomotopic.quotientFunctor.map f) (nullHomotopic.quotientFunctor.map (coneInclusion f)) = 0

The composite from the domain to its cone vanishes in the homotopy category.

noncomputable def TauCeti.MatrixFactorization.coneMap {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : cone f ⟶ cone g

A commutative square of matrix factorizations induces a map between its cones.

Equations

• TauCeti.MatrixFactorization.coneMap f g a b h = { hom := TauCeti.CurvedDuplex.coneMap f.hom g.hom a.hom b.hom ⋯ }

theorem TauCeti.MatrixFactorization.coneMap_hom {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : (coneMap f g a b h).hom = CurvedDuplex.coneMap f.hom g.hom a.hom b.hom ⋯

@[simp]

theorem TauCeti.MatrixFactorization.coneMap_hom_f₀ {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : (coneMap f g a b h).hom.f₀ = CategoryTheory.Limits.biprod.map a.hom.f₁ b.hom.f₀

@[simp]

theorem TauCeti.MatrixFactorization.coneMap_hom_f₁ {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : (coneMap f g a b h).hom.f₁ = CategoryTheory.Limits.biprod.map a.hom.f₀ b.hom.f₁

@[simp]

theorem TauCeti.MatrixFactorization.coneMap_id {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) : coneMap f f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ = CategoryTheory.CategoryStruct.id (cone f)

The identity square induces the identity on the cone.

theorem TauCeti.MatrixFactorization.coneMap_comp {S : Type u} [CommRing S] {w : S} {X Y X' Y' X'' Y'' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (k : X'' ⟶ Y'') (a : X ⟶ X') (b : Y ⟶ Y') (a' : X' ⟶ X'') (b' : Y' ⟶ Y'') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) (h' : CategoryTheory.CategoryStruct.comp g b' = CategoryTheory.CategoryStruct.comp a' k) : coneMap f k (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯ = CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (coneMap g k a' b' h')

Composing squares composes the induced maps on cones.

instance TauCeti.MatrixFactorization.isIso_coneMap {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) [CategoryTheory.IsIso a] [CategoryTheory.IsIso b] : CategoryTheory.IsIso (coneMap f g a b h)

A square of isomorphisms induces an isomorphism of cones.

@[simp]

theorem TauCeti.MatrixFactorization.coneInclusion_comp_coneMap {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneMap f g a b h) = CategoryTheory.CategoryStruct.comp b (coneInclusion g)

Cone maps commute with the inclusions of their codomains.

@[simp]

theorem TauCeti.MatrixFactorization.coneInclusion_comp_coneMap_assoc {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) {Z : MatrixFactorization S w} (h✝ : cone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (CategoryTheory.CategoryStruct.comp (coneMap f g a b h) h✝) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (coneInclusion g) h✝)

Cone maps commute with the inclusions of their codomains.

@[simp]

theorem TauCeti.MatrixFactorization.coneMap_comp_coneProjection {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) : CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (coneProjection g) = CategoryTheory.CategoryStruct.comp (coneProjection f) (parityShift.map a)

Cone maps commute with the projections to the shifted domains.

@[simp]

theorem TauCeti.MatrixFactorization.coneMap_comp_coneProjection_assoc {S : Type u} [CommRing S] {w : S} {X Y X' Y' : MatrixFactorization S w} (f : X ⟶ Y) (g : X' ⟶ Y') (a : X ⟶ X') (b : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g) {Z : MatrixFactorization S w} (h✝ : parityShift.obj X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (CategoryTheory.CategoryStruct.comp (coneProjection g) h✝) = CategoryTheory.CategoryStruct.comp (coneProjection f) (CategoryTheory.CategoryStruct.comp (parityShift.map a) h✝)

Cone maps commute with the projections to the shifted domains.

theorem TauCeti.MatrixFactorization.isZero_quotientFunctor_obj_cone_isIso {S : Type u} [CommRing S] {w : S} {X Y : MatrixFactorization S w} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.Limits.IsZero (nullHomotopic.quotientFunctor.obj (cone f))

The cone of an isomorphism is contractible and becomes zero in the homotopy category.