Curved duplexes with the componentwise split exact structure are Frobenius

Let C be an R-linear additive category and w : R. The componentwise split exact structure (ExactStructure.split C).curvedDuplex w on curved duplexes of curvature w has as conflations the short complexes of curved duplexes which split in both components, not necessarily compatibly with the differentials. This file proves that it is a Frobenius exact structure whose projective and injective objects are exactly the contractible duplexes, those whose identity is null-homotopic, and that its stable category is the homotopy category CurvedDuplex.HomotopyCategory C w.

The proofs use the elementary disks of TauCeti.Algebra.Homology.Curved.DiskFactorization. Every duplex X embeds by a componentwise split inflation into the contractible disk sum CurvedDuplex.diskSum X, and the disk sum of its parity shift maps onto it by a componentwise split deflation. A contractible duplex extends maps across componentwise split inflations and lifts them along componentwise split deflations, through the null-homotopic map built from a contraction and the componentwise retractions or sections.

Since the structure is Frobenius, its stable category is triangulated by Happel's theorem TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated. Matrix factorizations of w over a commutative ring S are the curved duplexes in ModuleCat S with finitely generated projective components, and the disks on such components are again matrix factorizations. At w = 0 the result is the curved-duplex counterpart of the two-periodic case of TauCeti.ExactStructure.homologicalComplex_split_isFrobenius.

Main results

• TauCeti.ExactStructure.curvedDuplex_split_isInjective_iff and TauCeti.ExactStructure.curvedDuplex_split_isProjective_iff: the relatively injective and relatively projective curved duplexes are the contractible ones.
• TauCeti.ExactStructure.curvedDuplex_split_isFrobenius: the componentwise split exact structure on curved duplexes is Frobenius.
• TauCeti.ExactStructure.curvedDuplex_split_projectiveStableIdeal_eq: a morphism of curved duplexes factors through a relative projective exactly when it is null-homotopic.
• TauCeti.ExactStructure.curvedDuplexSplitStableHomotopyEquivalence: the stable category of the componentwise split exact structure is equivalent to the homotopy category of curved duplexes, through the comparison TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy which sends the stable class of a morphism to its homotopy class.

References

• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3, for curved complexes and duplexes, their disks and their homotopy categories.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1, for the corresponding statement on complexes with the componentwise split exact structure.
• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

theorem TauCeti.ExactStructure.curvedDuplex_split_isInjective_of_mem_nullHomotopic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X : CurvedDuplex C w} (h : CategoryTheory.CategoryStruct.id X ∈ (CurvedDuplex.nullHomotopic C w).hom X X) : ((split C).curvedDuplex w).isInjective X

A contractible curved duplex is relatively injective for the componentwise split exact structure.

theorem TauCeti.ExactStructure.curvedDuplex_split_isProjective_of_mem_nullHomotopic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {X : CurvedDuplex C w} (h : CategoryTheory.CategoryStruct.id X ∈ (CurvedDuplex.nullHomotopic C w).hom X X) : ((split C).curvedDuplex w).isProjective X

A contractible curved duplex is relatively projective for the componentwise split exact structure.

theorem TauCeti.ExactStructure.curvedDuplex_split_isInflation_toDiskSum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (X : CurvedDuplex C w) : ((split C).curvedDuplex w).IsInflation X.toDiskSum

The canonical map from a curved duplex into the disk sum on its components is a componentwise split inflation.

theorem TauCeti.ExactStructure.exists_curvedDuplex_split_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (X : CurvedDuplex C w) : ∃ (P : CurvedDuplex C w) (p : P ⟶ X), ((split C).curvedDuplex w).IsDeflation p ∧ CategoryTheory.CategoryStruct.id P ∈ (CurvedDuplex.nullHomotopic C w).hom P P

Every curved duplex is a componentwise split quotient of a contractible one, the disk sum on the components of its parity shift.

theorem TauCeti.ExactStructure.curvedDuplex_split_enoughInjectives (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).EnoughInjectives

Every curved duplex is a componentwise split subobject of a contractible one, the disk sum on its components.

theorem TauCeti.ExactStructure.curvedDuplex_split_enoughProjectives (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).EnoughProjectives

Every curved duplex is a componentwise split quotient of a contractible one.

theorem TauCeti.ExactStructure.curvedDuplex_split_isInjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (X : CurvedDuplex C w) : ((split C).curvedDuplex w).isInjective X ↔ CategoryTheory.CategoryStruct.id X ∈ (CurvedDuplex.nullHomotopic C w).hom X X

The relatively injective curved duplexes are the contractible ones. For the componentwise split exact structure, a curved duplex is relatively injective exactly when its identity is null-homotopic.

theorem TauCeti.ExactStructure.curvedDuplex_split_isProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (X : CurvedDuplex C w) : ((split C).curvedDuplex w).isProjective X ↔ CategoryTheory.CategoryStruct.id X ∈ (CurvedDuplex.nullHomotopic C w).hom X X

The relatively projective curved duplexes are the contractible ones. For the componentwise split exact structure, a curved duplex is relatively projective exactly when its identity is null-homotopic.

theorem TauCeti.ExactStructure.curvedDuplex_split_isFrobenius (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).IsFrobenius

Curved duplexes form a Frobenius exact category. The componentwise split exact structure on curved duplexes of curvature w is Frobenius, and its projective-injective objects are the contractible duplexes (curvedDuplex_split_isProjective_iff).

theorem TauCeti.ExactStructure.curvedDuplex_split_projectiveStableIdeal_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).projectiveStableIdeal = CurvedDuplex.nullHomotopic C w

A morphism of curved duplexes factors through a relative projective of the componentwise split exact structure exactly when it is null-homotopic: the projective stable ideal is the ideal of null-homotopic morphisms.

theorem TauCeti.ExactStructure.curvedDuplex_split_projectiveStableIdeal_eq_kerIdeal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).projectiveStableIdeal = (CurvedDuplex.nullHomotopic C w).quotientFunctor.kerIdeal

The projective stable ideal of the componentwise split exact structure is the kernel of the quotient functor to the homotopy category of curved duplexes.

noncomputable def TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Functor ((split C).curvedDuplex w).ProjectiveStableCategory (CurvedDuplex.HomotopyCategory C w)

The canonical comparison from the componentwise split stable category of curved duplexes to their homotopy category, sending the stable class of a morphism to its homotopy class.

Equations

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

theorem TauCeti.ExactStructure.projectiveStableFunctor_comp_curvedDuplexSplitStableToHomotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).projectiveStableFunctor.comp (curvedDuplexSplitStableToHomotopy C w) = (CurvedDuplex.nullHomotopic C w).quotientFunctor

The comparison restricts to the homotopy quotient on curved duplexes.

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy_obj_projectiveStableFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (X : CurvedDuplex C w) : (curvedDuplexSplitStableToHomotopy C w).obj (((split C).curvedDuplex w).projectiveStableFunctor.obj X) = (CurvedDuplex.nullHomotopic C w).quotientFunctor.obj X

The comparison sends the stable image of a curved duplex to its image in the homotopy category.

theorem TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy_map_projectiveStableFunctor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (curvedDuplexSplitStableToHomotopy C w).map (((split C).curvedDuplex w).projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CurvedDuplex.nullHomotopic C w).quotientFunctor.map f) (CategoryTheory.eqToHom ⋯))

The comparison sends the stable class of a morphism to its homotopy class, up to the identification of objects curvedDuplexSplitStableToHomotopy_obj_projectiveStableFunctor_obj.

instance TauCeti.ExactStructure.instAdditiveProjectiveStableCategoryCurvedDuplexCurvedDuplexSplitHomotopyCategoryCurvedDuplexSplitStableToHomotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (curvedDuplexSplitStableToHomotopy C w).Additive

The stable-to-homotopy comparison preserves addition of morphisms.

instance TauCeti.ExactStructure.instLinearProjectiveStableCategoryCurvedDuplexCurvedDuplexSplitHomotopyCategoryCurvedDuplexSplitStableToHomotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Functor.Linear R (curvedDuplexSplitStableToHomotopy C w)

The stable-to-homotopy comparison preserves the scalars of the linear structure.

instance TauCeti.ExactStructure.instIsEquivalenceProjectiveStableCategoryCurvedDuplexCurvedDuplexSplitHomotopyCategoryCurvedDuplexSplitStableToHomotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (curvedDuplexSplitStableToHomotopy C w).IsEquivalence

The comparison is an equivalence: the stable quotient and the homotopy quotient kill the same morphisms.

noncomputable def TauCeti.ExactStructure.curvedDuplexSplitStableHomotopyEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : ((split C).curvedDuplex w).ProjectiveStableCategory ≌ CurvedDuplex.HomotopyCategory C w

The stable category of the componentwise split exact structure on curved duplexes is equivalent to the homotopy category of curved duplexes.

Equations

• TauCeti.ExactStructure.curvedDuplexSplitStableHomotopyEquivalence C w = (TauCeti.ExactStructure.curvedDuplexSplitStableToHomotopy C w).asEquivalence

@[simp]

theorem TauCeti.ExactStructure.curvedDuplexSplitStableHomotopyEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (curvedDuplexSplitStableHomotopyEquivalence C w).functor = curvedDuplexSplitStableToHomotopy C w

The functor of the stable/homotopy equivalence is the canonical comparison.