The componentwise exact structure on curved duplexes

Let E be a Quillen exact structure on an R-linear additive category C and let w : R. The category CurvedDuplex C w of curved duplexes of curvature w carries the componentwise exact structure E.curvedDuplex w: a short complex of curved duplexes is a conflation when its even and its odd components are conflations of E. No limits or colimits are assumed in C: the kernels, cokernels, pushouts and pullbacks required by the axioms are those supplied componentwise by E, assembled into curved duplexes by the componentwise limits and colimits of TauCeti.Algebra.Homology.Curved.Limits.

Specializing E to the split exact structure gives the componentwise split exact structure (ExactStructure.split C).curvedDuplex w, whose conflations are the short complexes of curved duplexes which split in both components, though not necessarily compatibly with the differentials. It is Frobenius, with the contractible duplexes as its projective-injective objects (TauCeti.ExactStructure.curvedDuplex_split_isFrobenius).

Main definitions

• TauCeti.ExactStructure.curvedDuplex: the componentwise exact structure on CurvedDuplex C w.

Main results

• TauCeti.CurvedDuplex.isKernelCokernelPair_of_eval: a short complex of curved duplexes which is a kernel–cokernel pair in both components is a kernel–cokernel pair.
• TauCeti.ExactStructure.curvedDuplex_conflation_iff, TauCeti.ExactStructure.curvedDuplex_isInflation_iff and TauCeti.ExactStructure.curvedDuplex_isDeflation_iff: conflations, inflations and deflations are detected componentwise.
• TauCeti.ExactStructure.isConflationExact_eval₀_curvedDuplex and TauCeti.ExactStructure.isConflationExact_eval₁_curvedDuplex: the evaluation functors preserve conflations.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480, Section 9, for the corresponding degreewise exact structure on chain complexes.
• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3, where curved complexes are given the componentwise split exact structure.

theorem TauCeti.CurvedDuplex.isKernelCokernelPair_of_eval {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} {S : CategoryTheory.ShortComplex (CurvedDuplex C w)} (h₀ : IsKernelCokernelPair (S.map (eval₀ C w))) (h₁ : IsKernelCokernelPair (S.map (eval₁ C w))) : IsKernelCokernelPair S

A short complex of curved duplexes which is a kernel–cokernel pair in both components is a kernel–cokernel pair: kernels and cokernels of curved duplexes may be computed componentwise.

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

The componentwise exact structure on curved duplexes. A short complex of curved duplexes is a conflation when its even and its odd components are conflations of E.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.curvedDuplex_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (w : R) (S : CategoryTheory.ShortComplex (CurvedDuplex C w)) : (E.curvedDuplex w).Conflation S ↔ E.Conflation (S.map (CurvedDuplex.eval₀ C w)) ∧ E.Conflation (S.map (CurvedDuplex.eval₁ C w))

A short complex of curved duplexes is a conflation for the componentwise exact structure exactly when both of its components are conflations.

@[simp]

theorem TauCeti.ExactStructure.curvedDuplex_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (E.curvedDuplex w).IsInflation f ↔ E.IsInflation f.f₀ ∧ E.IsInflation f.f₁

A morphism of curved duplexes is an inflation for the componentwise exact structure exactly when both of its components are inflations.

@[simp]

theorem TauCeti.ExactStructure.curvedDuplex_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {w : R} {X Y : CurvedDuplex C w} (f : X ⟶ Y) : (E.curvedDuplex w).IsDeflation f ↔ E.IsDeflation f.f₀ ∧ E.IsDeflation f.f₁

A morphism of curved duplexes is a deflation for the componentwise exact structure exactly when both of its components are deflations.

theorem TauCeti.ExactStructure.isConflationExact_eval₀_curvedDuplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (w : R) : (E.curvedDuplex w).IsConflationExact E (CurvedDuplex.eval₀ C w)

Evaluation at the even component preserves conflations of the componentwise exact structure.

theorem TauCeti.ExactStructure.isConflationExact_eval₁_curvedDuplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (w : R) : (E.curvedDuplex w).IsConflationExact E (CurvedDuplex.eval₁ C w)

Evaluation at the odd component preserves conflations of the componentwise exact structure.