Copy-Discard Categories

Symmetric monoidal categories where every object has a commutative comonoid structure compatible with tensor products.

Main definitions

• CopyDiscardCategory - Category with coherent copy and delete

Notations

• Δ[X] - Copy morphism for X (from ComonObj)
• ε[X] - Delete morphism for X (from ComonObj)

Implementation notes

We use ComonObj instances to provide the comonoid structure. The key axioms ensure tensor products respect the comonoid structure.

References

• [Cho and Jacobs, Disintegration and Bayesian inversion via string diagrams][cho_jacobs_2019]
• [Fritz, A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics][fritz2020]

Tags

copy-discard, comonoid, symmetric monoidal

class CategoryTheory.CopyDiscardCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] extends CategoryTheory.SymmetricCategory C : Type (max u v)

Category where objects have compatible copy and discard operations.

• braiding (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ≅ MonoidalCategoryStruct.tensorObj Y X
• braiding_naturality_right (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) (β_ X Z).hom = CategoryStruct.comp (β_ X Y).hom (MonoidalCategoryStruct.whiskerRight f X)
• braiding_naturality_left {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (β_ Y Z).hom = CategoryStruct.comp (β_ X Z).hom (MonoidalCategoryStruct.whiskerLeft Z f)
• hexagon_forward (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (β_ X (MonoidalCategoryStruct.tensorObj Y Z)).hom (MonoidalCategoryStruct.associator Y Z X).hom) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Z).hom (MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom))
• hexagon_reverse (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (β_ (MonoidalCategoryStruct.tensorObj X Y) Z).hom (MonoidalCategoryStruct.associator Z X Y).inv) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Z Y).inv (MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y))
• symmetry (X Y : C) : CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)
• comonObj (X : C) : ComonObj X

  Every object has commutative comonoid structure.

• isCommComonObj (X : C) : IsCommComonObj X

  Every object's comonoid structure is commutative.

• copy_tensor (X Y : C) : ComonObj.comul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (MonoidalCategory.tensorμ X X Y Y)

  Tensor products of copies equal copies of tensor products.

• discard_tensor (X Y : C) : ComonObj.counit = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

  Discard distributes over tensor.

• copy_unit : ComonObj.comul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv

  Copy on the unit object.

• discard_unit : ComonObj.counit = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

  Discard on the unit object.