Exact structures with a biexact tensor product

An exact structure E on a monoidal additive category C is monoidal when the tensor product is biexact: for every object X, tensoring on the left with X and tensoring on the right with X carry E-conflations to E-conflations. This is the hypothesis under which the tensor product descends to a multiplication on the exact Grothendieck group, as split short exact sequences always do on split K₀.

The motivating instance is the canonical exact structure on the abelian category of finite-dimensional representations of a monoid over a field: the tensor product over a field is exact in each variable, while short exact sequences of representations need not split.

Main definitions

• TauCeti.ExactStructure.IsMonoidal: the tensor product of C is biexact for E.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, Section 5, for exact functors between exact categories.

class TauCeti.ExactStructure.IsMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (E : ExactStructure C) : Prop

An exact structure on a monoidal additive category is monoidal when its tensor product is biexact: tensoring on either side with a fixed object is a conflation-exact functor.

• isConflationExact_tensorLeft (X : C) : E.IsConflationExact E (CategoryTheory.MonoidalCategory.tensorLeft X)

  Tensoring on the left with a fixed object carries conflations to conflations.

• isConflationExact_tensorRight (X : C) : E.IsConflationExact E (CategoryTheory.MonoidalCategory.tensorRight X)

  Tensoring on the right with a fixed object carries conflations to conflations.