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][fritz2020]

@[reducible, inline]

abbrev StochHom : CategoryTheory.MorphismProperty SFinKer

Morphism property selecting Markov kernels in SFinKer.

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.

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

@[implicit_reducible]

noncomputable instance instMarkovCategoryStoch : CategoryTheory.MarkovCategory Stoch