Positive Categories

Markov categories where deletion is natural for all morphisms.

Main definitions

• PositiveCategory: Markov category where copy is natural given deterministic composition of morphisms.

Main results

• copy_comp_natural - Given morphisms f : X ⟶ Y and g : Y ⟶ Z, if their composition is deterministic, then process f, copy and then process g equals copy and process f and g independently.

• All isomorphisms in a positive Markov category are deterministic.

Implementation notes

The key property copy_comp_natural : f ≫ Δ ≫ (g ⊗ₘ 𝟙 Y) = Δ ≫ (f ≫ g ⊗ₘ f), given Deterministic (f ≫ g), means that after processing f, copying and then processing g is the same as copying and processing f and g independently. The probabilistic interpretation is that given a deterministic process that has a stochastic intermediate result, the same distribution over both results can be obtained by computing the intermediate result independently of the deterministic process.

References

• Fritz, A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, Def. 11.22
• Moss and Perrone, A category-theoretic proof of the ergodic decomposition theorem

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

Markov category where copy is natural given deterministic composition of morphisms.

• 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
• isCommComonObj (X : C) : IsCommComonObj X
• copy_tensor (X Y : C) : ComonObj.comul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (MonoidalCategory.tensorμ X X Y Y)
• discard_tensor (X Y : C) : ComonObj.counit = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom
• copy_unit : ComonObj.comul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv
• discard_unit : ComonObj.counit = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
• discard_natural {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f ComonObj.counit = ComonObj.counit
• copy_comp_natural {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : Deterministic (CategoryStruct.comp f g)] : CategoryStruct.comp f (CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom g (CategoryStruct.id Y))) = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp f g) f)

  Given morphisms f : X ⟶ Y and g : Y ⟶ Z, if their composition is deterministic, then process f, copy and then process g equals copy and process f and g independently.

instance CategoryTheory.PositiveCategory.instDeterministicOfIsIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [PositiveCategory C] {X Y : C} (f : X ⟶ Y) [IsIso f] : Deterministic f