Markov Categories

Copy-discard categories where deletion is natural for all morphisms.

Main definitions

• MarkovCategory - Copy-discard category with natural deletion

Main results

• eq_discard - Any morphism to the unit equals discard
• isTerminalUnit - The monoidal unit is terminal

Implementation notes

Natural discard forces probabilistic interpretation: morphisms preserve normalization. The unit being terminal follows from naturality of discard.

The key property discard_natural : f ≫ ε[Y] = ε[X] means discard "erases" any preceding morphism, a distinguishing feature of Markov categories in categorical probability.

References

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

Tags

Markov category, probability, categorical probability

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

Copy-discard category where discard is natural.

• 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

  Process then discard equals discard directly.

@[simp]

theorem CategoryTheory.MarkovCategory.discard_natural_assoc {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : MonoidalCategory C} [self : MarkovCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp ComonObj.counit h) = CategoryStruct.comp ComonObj.counit h

Process then discard equals discard directly.

theorem CategoryTheory.MarkovCategory.eq_discard {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MarkovCategory C] (X : C) (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) : f = ComonObj.counit

Any morphism to the unit equals discard.

def CategoryTheory.MarkovCategory.isTerminalUnit {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MarkovCategory C] : Limits.IsTerminal (MonoidalCategoryStruct.tensorUnit C)

The monoidal unit is a terminal object.

Equations

• CategoryTheory.MarkovCategory.isTerminalUnit = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (Y : C) => CategoryTheory.ComonObj.counit) ⋯

instance CategoryTheory.MarkovCategory.instSubsingletonHomTensorUnit {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MarkovCategory C] (X : C) : Subsingleton (X ⟶ MonoidalCategoryStruct.tensorUnit C)

There is a unique morphism to the unit (it is terminal).