Stoch

The category of measurable spaces with Markov kernels is a positive Markov category.

Main definition

Stoch is defined as the wide subcategory WideSubcategory StochHom of SFinKer, where StochHom selects Markov kernels, and this construction provides in particular the instance PositiveCategory Stoch.

Implementation notes

Among categories of measurable spaces and probability kernels, Stoch stands out as the unique positive Markov category. In contrast, SFinKer and the category of finite kernels (not implemented) do not satisfy positivity. To see why, consider the counterexample with $X = Y = \{\varnothing\}$, kernels $\kappa(\cdot | \varnothing) = 2\delta_{\varnothing}$ and $\eta(\cdot | \varnothing) = (1/2)\delta_{\varnothing}$: although their composition is deterministic, the positivity equation fails.

References

• A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics

@[reducible, inline]

abbrev StochHom : CategoryTheory.MorphismProperty SFinKer

Morphism property selecting Markov kernels in SFinKer.

Equations

• StochHom κ = ProbabilityTheory.IsMarkovKernel κ.hom

instance instIsStableUnderBraidingSFinKerStochHom : StochHom.IsStableUnderBraiding

instance instIsStableUnderComonoidSFinKerStochHom {X : SFinKer} : StochHom.IsStableUnderComonoid X

@[reducible, inline]

abbrev Stoch : Type (u_1 + 1)

Stoch is the wide subcategory of SFinKer with Markov-kernel morphisms.

Equations

• Stoch = CategoryTheory.WideSubcategory StochHom

instance instDeterministicStochOfSFinKerHomWideSubcategoryStochHom {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ.hom] : CategoryTheory.Deterministic κ

instance instDeterministicStochComul {X : Stoch} : CategoryTheory.Deterministic CategoryTheory.ComonObj.comul

instance instDeterministicStochCounit {X : Stoch} : CategoryTheory.Deterministic CategoryTheory.ComonObj.counit

instance instDeterministicStochMkWideSubcategorySFinKerStochHomMkOfIsDeterministicCarrierObj (X Y : Stoch) (κ : ProbabilityTheory.Kernel X.obj.carrier Y.obj.carrier) [ProbabilityTheory.IsDeterministic κ] [ProbabilityTheory.IsMarkovKernel κ] : CategoryTheory.Deterministic { hom := { hom := κ, property := ⋯ }, property := ⋯ }

instance instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory {X Y : Stoch} (κ : X ⟶ Y) : ProbabilityTheory.IsMarkovKernel κ.hom.hom

instance instDeterministicSFinKerHomWideSubcategoryStochHomOfStoch {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ] : CategoryTheory.Deterministic κ.hom

instance instIsDeterministicCarrierObjSFinKerStochHomHomHomWideSubcategoryOfDeterministicStoch {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ] : ProbabilityTheory.IsDeterministic κ.hom.hom

@[implicit_reducible]

noncomputable instance instPositiveCategoryStoch : CategoryTheory.PositiveCategory Stoch

Equations

• instPositiveCategoryStoch = { toCopyDiscardCategory := StochHom.instCopyDiscardCategoryWideSubcategoryOfIsStableUnderComonoid, discard_natural := ⋯, copy_comp_natural := ⋯ }