Kleisli Category of SPComp as a Symmetric Monoidal Category

This file shows that the Kleisli category of SPComp (stateful probabilistic computations) forms a symmetric monoidal category with Sum as tensor and Empty as unit.

Main results

• Category KlSPComp — Kleisli category of SPComp
• MonoidalCategory KlSPComp — Sum tensor, Empty unit
• BraidedCategory KlSPComp — braiding swaps summands via pure
• SymmetricCategory KlSPComp — braiding is self-inverse

def CatCrypt.Core.KlSPComp : Type 1

Objects of the Kleisli category of SPComp. Opaque wrapper around Type to avoid conflicting with Mathlib's CategoryTheory.types : Category Type.

Equations

• CatCrypt.Core.KlSPComp = Type

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instCategoryStruct : CategoryTheory.CategoryStruct.{0, 1} KlSPComp

Equations

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

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instCategory : CategoryTheory.Category.{0, 1} KlSPComp

Equations

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

@[simp]

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

@[simp]

theorem CatCrypt.Core.KlSPComp.id_apply {α : KlSPComp} (x : α) : CategoryTheory.CategoryStruct.id α x = SPComp.pure x

Monoidal definitions

All structural morphisms use explicit pattern matching on Sum constructors so their equations are directly available to simp.

noncomputable def CatCrypt.Core.KlSPComp.wkL (X : KlSPComp) {Y₁ Y₂ : KlSPComp} (f : Y₁ ⟶ Y₂) : (have this := X ⊕ Y₁; this) ⟶ have this := X ⊕ Y₂; this

Equations

• X.wkL f (Sum.inl a) = CatCrypt.Core.SPComp.pure (Sum.inl a)
• X.wkL f (Sum.inr c) = CatCrypt.Core.SPComp.map Sum.inr (f c)

noncomputable def CatCrypt.Core.KlSPComp.wkR {X₁ X₂ : KlSPComp} (f : X₁ ⟶ X₂) (Y : KlSPComp) : (have this := X₁ ⊕ Y; this) ⟶ have this := X₂ ⊕ Y; this

Equations

• CatCrypt.Core.KlSPComp.wkR f Y (Sum.inl a) = CatCrypt.Core.SPComp.map Sum.inl (f a)
• CatCrypt.Core.KlSPComp.wkR f Y (Sum.inr c) = CatCrypt.Core.SPComp.pure (Sum.inr c)

noncomputable def CatCrypt.Core.KlSPComp.assocHom (X Y Z : KlSPComp) : (have this := (X ⊕ Y) ⊕ Z; this) ⟶ have this := X ⊕ Y ⊕ Z; this

Equations

• X.assocHom Y Z (Sum.inl (Sum.inl a)) = CatCrypt.Core.SPComp.pure (Sum.inl a)
• X.assocHom Y Z (Sum.inl (Sum.inr b)) = CatCrypt.Core.SPComp.pure (Sum.inr (Sum.inl b))
• X.assocHom Y Z (Sum.inr c) = CatCrypt.Core.SPComp.pure (Sum.inr (Sum.inr c))

noncomputable def CatCrypt.Core.KlSPComp.assocInv (X Y Z : KlSPComp) : (have this := X ⊕ Y ⊕ Z; this) ⟶ have this := (X ⊕ Y) ⊕ Z; this

Equations

• X.assocInv Y Z (Sum.inl a) = CatCrypt.Core.SPComp.pure (Sum.inl (Sum.inl a))
• X.assocInv Y Z (Sum.inr (Sum.inl b)) = CatCrypt.Core.SPComp.pure (Sum.inl (Sum.inr b))
• X.assocInv Y Z (Sum.inr (Sum.inr c)) = CatCrypt.Core.SPComp.pure (Sum.inr c)

noncomputable def CatCrypt.Core.KlSPComp.assocIso (X Y Z : KlSPComp) : (have this := (X ⊕ Y) ⊕ Z; this) ≅ have this := X ⊕ Y ⊕ Z; this

Equations

• X.assocIso Y Z = { hom := X.assocHom Y Z, inv := X.assocInv Y Z, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CatCrypt.Core.KlSPComp.lUnit (X : KlSPComp) : (have this := Empty ⊕ X; this) ≅ X

Equations

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

noncomputable def CatCrypt.Core.KlSPComp.rUnit (X : KlSPComp) : (have this := X ⊕ Empty; this) ≅ X

Equations

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

noncomputable def CatCrypt.Core.KlSPComp.braidHom (X Y : KlSPComp) : (have this := X ⊕ Y; this) ⟶ have this := Y ⊕ X; this

Equations

• X.braidHom Y (Sum.inl a) = CatCrypt.Core.SPComp.pure (Sum.inr a)
• X.braidHom Y (Sum.inr c) = CatCrypt.Core.SPComp.pure (Sum.inl c)

noncomputable def CatCrypt.Core.KlSPComp.braidIso (X Y : KlSPComp) : (have this := X ⊕ Y; this) ≅ have this := Y ⊕ X; this

Equations

• X.braidIso Y = { hom := X.braidHom Y, inv := Y.braidHom X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct KlSPComp

Equations

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

Simp lemmas for class projections

These bridge from Mathlib notation (◁, ▷, ⊗ₘ, α_, λ_, ρ_) to our concrete definitions (wkL, wkR, assocIso, lUnit, rUnit).

@[simp]

theorem CatCrypt.Core.KlSPComp.whiskerLeft_def (X : KlSPComp) {Y₁ Y₂ : KlSPComp} (f : Y₁ ⟶ Y₂) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = X.wkL f

@[simp]

theorem CatCrypt.Core.KlSPComp.whiskerRight_def {X₁ X₂ : KlSPComp} (f : X₁ ⟶ X₂) (Y : KlSPComp) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = wkR f Y

@[simp]

theorem CatCrypt.Core.KlSPComp.tensorHom_eq {X₁ Y₁ X₂ Y₂ : KlSPComp} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.CategoryStruct.comp (wkR f X₂) (Y₁.wkL g)

@[simp]

theorem CatCrypt.Core.KlSPComp.associator_hom_eq (X Y Z : KlSPComp) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = X.assocHom Y Z

@[simp]

theorem CatCrypt.Core.KlSPComp.associator_inv_eq (X Y Z : KlSPComp) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = X.assocInv Y Z

@[simp]

theorem CatCrypt.Core.KlSPComp.leftUnitor_hom_eq (X : KlSPComp) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = X.lUnit.hom

@[simp]

theorem CatCrypt.Core.KlSPComp.rightUnitor_hom_eq (X : KlSPComp) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = X.rUnit.hom

MonoidalCategory

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instMonoidalCategory : CategoryTheory.MonoidalCategory KlSPComp

Equations

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

BraidedCategory and SymmetricCategory

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instBraidedCategory : CategoryTheory.BraidedCategory KlSPComp

Equations

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

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instSymmetricCategory : CategoryTheory.SymmetricCategory KlSPComp

Equations

• CatCrypt.Core.KlSPComp.instSymmetricCategory = { toBraidedCategory := CatCrypt.Core.KlSPComp.instBraidedCategory, symmetry := CatCrypt.Core.KlSPComp.instSymmetricCategory._proof_1 }