Stoch

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

Main declarations

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

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 instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory {X Y : Stoch} (κ : X ⟶ Y) : ProbabilityTheory.IsMarkovKernel κ.hom.hom

@[implicit_reducible]

noncomputable instance instMarkovCategoryStoch : CategoryTheory.MarkovCategory Stoch

Equations

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