Kleisli Category of PMF as a Markov Category

The Kleisli category of the PMF monad (probability mass functions), with Prod as tensor and PUnit as unit, forms a Markov category — the first non-trivial instance of MarkovCategory.

Full probability (PMF) rather than sub-probability (PMF (Option α)) is needed because discard_natural (f ≫ ε = ε) requires mass preservation. The key lemma is PMF.bind_const : (p.bind fun _ => q) = q, giving discard_natural for free.

Main results

• MonoidalCategory (KleisliCat PMF) — Prod tensor, PUnit unit
• BraidedCategory (KleisliCat PMF) — braiding swaps components via pure
• SymmetricCategory (KleisliCat PMF) — braiding is self-inverse
• CopyDiscardCategory (KleisliCat PMF) — diagonal copy, terminal discard
• MarkovCategory (KleisliCat PMF) — discard_natural via PMF.bind_const

@[simp]

theorem CategoryTheory.KleisliCat.comp_apply {α β γ : KleisliCat PMF} (f : α ⟶ β) (g : β ⟶ γ) (x : α) : CategoryStruct.comp f g x = (f x).bind g

Composition in KleisliCat PMF applies the first morphism then binds the second.

@[simp]

theorem CategoryTheory.KleisliCat.id_apply {α : KleisliCat PMF} (x : α) : CategoryStruct.id α x = PMF.pure x

The identity morphism in KleisliCat PMF is PMF.pure.

@[simp]

theorem CategoryTheory.KleisliCat.pure_eq {α : KleisliCat PMF} (a : α) : pure a = PMF.pure a

Bridge between the generic pure and PMF.pure, needed because KleisliCat.id_def rewrites 𝟙 α to the generic monad pure.

Monoidal structure

noncomputable def CategoryTheory.KleisliCat.whiskerLeftPMF (X : KleisliCat PMF) {Y₁ Y₂ : KleisliCat PMF} (f : Y₁ ⟶ Y₂) : (have this := X × Y₁; this) ⟶ have this := X × Y₂; this

Left whiskering: tensors the identity on X with a morphism f on the right.

Equations

• X.whiskerLeftPMF f (x_1, y) = (f y).bind fun (y' : Y₂) => PMF.pure (x_1, y')

noncomputable def CategoryTheory.KleisliCat.whiskerRightPMF {X₁ X₂ : KleisliCat PMF} (f : X₁ ⟶ X₂) (Y : KleisliCat PMF) : (have this := X₁ × Y; this) ⟶ have this := X₂ × Y; this

Right whiskering: tensors a morphism f on the left with the identity on Y.

Equations

• CategoryTheory.KleisliCat.whiskerRightPMF f Y (x_1, y) = (f x_1).bind fun (x' : X₂) => PMF.pure (x', y)

noncomputable def CategoryTheory.KleisliCat.assocHomPMF (X : KleisliCat PMF) (Y : KleisliCat PMF) (Z : KleisliCat PMF) : (have this := (X × Y) × Z; this) ⟶ have this := X × Y × Z; this

Forward component of the associator.

Equations

• X.assocHomPMF Y Z ((x_1, y), z) = PMF.pure (x_1, y, z)

noncomputable def CategoryTheory.KleisliCat.assocInvPMF (X : KleisliCat PMF) (Y : KleisliCat PMF) (Z : KleisliCat PMF) : (have this := X × Y × Z; this) ⟶ have this := (X × Y) × Z; this

Inverse component of the associator.

Equations

• X.assocInvPMF Y Z (x_1, y, z) = PMF.pure ((x_1, y), z)

noncomputable def CategoryTheory.KleisliCat.assocIsoPMF (X : KleisliCat PMF) (Y : KleisliCat PMF) (Z : KleisliCat PMF) : (have this := (X × Y) × Z; this) ≅ have this := X × Y × Z; this

Associator isomorphism for the tensor product.

Equations

• X.assocIsoPMF Y Z = { hom := X.assocHomPMF Y Z, inv := X.assocInvPMF Y Z, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CategoryTheory.KleisliCat.leftUnitorPMF (X : KleisliCat PMF) : (have this := PUnit.{u_2 + 1} × X; this) ≅ X

Left unitor: PUnit ⊗ X ≅ X.

Equations

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

noncomputable def CategoryTheory.KleisliCat.rightUnitorPMF (X : KleisliCat PMF) : (have this := X × PUnit.{u_2 + 1}; this) ≅ X

Right unitor: X ⊗ PUnit ≅ X.

Equations

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

noncomputable def CategoryTheory.KleisliCat.braidHomPMF (X : KleisliCat PMF) (Y : KleisliCat PMF) : (have this := X × Y; this) ⟶ have this := Y × X; this

Forward component of the braiding: swaps the two components.

Equations

• X.braidHomPMF Y (x_1, y) = PMF.pure (y, x_1)

noncomputable def CategoryTheory.KleisliCat.braidIsoPMF (X : KleisliCat PMF) (Y : KleisliCat PMF) : (have this := X × Y; this) ≅ have this := Y × X; this

Braiding isomorphism: swaps the two tensor factors.

Equations

• X.braidIsoPMF Y = { hom := X.braidHomPMF Y, inv := Y.braidHomPMF X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instMonoidalCategoryStructPMF_catCryptCore : MonoidalCategoryStruct (KleisliCat PMF)

Equations

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

Simp lemmas

@[simp]

theorem CategoryTheory.KleisliCat.whiskerLeft_def (X : KleisliCat PMF) {Y₁ Y₂ : KleisliCat PMF} (f : Y₁ ⟶ Y₂) : MonoidalCategoryStruct.whiskerLeft X f = X.whiskerLeftPMF f

@[simp]

theorem CategoryTheory.KleisliCat.whiskerRight_def {X₁ X₂ : KleisliCat PMF} (f : X₁ ⟶ X₂) (Y : KleisliCat PMF) : MonoidalCategoryStruct.whiskerRight f Y = whiskerRightPMF f Y

@[simp]

theorem CategoryTheory.KleisliCat.tensorHom_eq {X₁ Y₁ X₂ Y₂ : KleisliCat PMF} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : MonoidalCategoryStruct.tensorHom f g = CategoryStruct.comp (whiskerRightPMF f X₂) (Y₁.whiskerLeftPMF g)

@[simp]

theorem CategoryTheory.KleisliCat.associator_hom_eq (X Y Z : KleisliCat PMF) : (MonoidalCategoryStruct.associator X Y Z).hom = X.assocHomPMF Y Z

@[simp]

theorem CategoryTheory.KleisliCat.associator_inv_eq (X Y Z : KleisliCat PMF) : (MonoidalCategoryStruct.associator X Y Z).inv = X.assocInvPMF Y Z

@[simp]

theorem CategoryTheory.KleisliCat.leftUnitor_hom_eq (X : KleisliCat PMF) : (MonoidalCategoryStruct.leftUnitor X).hom = X.leftUnitorPMF.hom

@[simp]

theorem CategoryTheory.KleisliCat.leftUnitor_inv_eq (X : KleisliCat PMF) : (MonoidalCategoryStruct.leftUnitor X).inv = X.leftUnitorPMF.inv

@[simp]

theorem CategoryTheory.KleisliCat.rightUnitor_hom_eq (X : KleisliCat PMF) : (MonoidalCategoryStruct.rightUnitor X).hom = X.rightUnitorPMF.hom

@[simp]

theorem CategoryTheory.KleisliCat.rightUnitor_inv_eq (X : KleisliCat PMF) : (MonoidalCategoryStruct.rightUnitor X).inv = X.rightUnitorPMF.inv

MonoidalCategory

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instMonoidalCategoryPMF_catCryptCore : MonoidalCategory (KleisliCat PMF)

Equations

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

BraidedCategory and SymmetricCategory

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instBraidedCategoryPMF_catCryptCore : BraidedCategory (KleisliCat PMF)

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instSymmetricCategoryPMF_catCryptCore : SymmetricCategory (KleisliCat PMF)

Equations

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

ComonObj (copy = diagonal, delete = terminal)

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instComonObjPMF (X : KleisliCat PMF) : ComonObj X

Every type in KleisliCat PMF is a comonoid object: comul is the diagonal and counit is the terminal map.

Equations

• X.instComonObjPMF = { counit := fun (x : X) => PMF.pure PUnit.unit, comul := fun (x : X) => PMF.pure (x, x), counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }

@[simp]

theorem CategoryTheory.KleisliCat.braiding_hom_eq (X Y : KleisliCat PMF) : (β_ X Y).hom = X.braidHomPMF Y

@[simp]

theorem CategoryTheory.KleisliCat.braiding_inv_eq (X Y : KleisliCat PMF) : (β_ X Y).inv = Y.braidHomPMF X

instance CategoryTheory.KleisliCat.instIsCommComonObjPMF (X : KleisliCat PMF) : IsCommComonObj X

Every type in KleisliCat PMF is a commutative comonoid object.

CopyDiscardCategory

theorem CategoryTheory.KleisliCat.tensorμ_apply (X₁ X₂ Y₁ Y₂ : KleisliCat PMF) (x₁ : X₁) (x₂ : X₂) (y₁ : Y₁) (y₂ : Y₂) : MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂ ((x₁, x₂), y₁, y₂) = PMF.pure ((x₁, y₁), x₂, y₂)

The tensor strength tensorμ acts as a pure reshuffling on product types.

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instCopyDiscardCategoryPMF_catCryptCore : CopyDiscardCategory (KleisliCat PMF)

Equations

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

MarkovCategory

@[implicit_reducible]

noncomputable instance CategoryTheory.KleisliCat.instMarkovCategoryPMF_catCryptCore : MarkovCategory (KleisliCat PMF)

KleisliCat PMF is a Markov category: discarding after any stochastic map equals discarding directly.

Equations

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