Documentation

Mathlib.Probability.Kernel.Category.SFinKer

SFinKer #

The category of measurable spaces with s-finite kernels is a copy-discard category.

Main declarations #

LargeCategory SFinKer: the categorical structure on SFinKer.
MonoidalCategory SFinKer: SFinKer is a monoidal category using the Cartesian product.
SymmetricCategory SFinKer: SFinKer is a symmetric monoidal category.
CopyDiscardCategory SFinKer: SFinKer is a copy-discard category.

References #

[A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics][fritz2020]

structure SFinKer :

Type (u + 1)

The category of measurable spaces and s-finite kernels.

of :: (

carrier : Type u
The underlying measurable space.
str : MeasurableSpace self.carrier

)

Instances For

@[implicit_reducible]

instance instCoeSortSFinKerType :

CoeSort SFinKer (Type u_1)

structure SFinKer.Hom (X Y : SFinKer) :

The morphisms in SFinKer from X to Y are the s-finite kernels from X to Y.

hom : ProbabilityTheory.Kernel X.carrier Y.carrier
The underlying morphism.
property : ProbabilityTheory.IsSFiniteKernel self.hom
The property that the morphism satisfies.

Instances For

theorem SFinKer.Hom.ext {X Y : SFinKer} {x y : X.Hom Y} (hom : x.hom = y.hom) :

x = y

theorem SFinKer.Hom.ext_iff {X Y : SFinKer} {x y : X.Hom Y} :

x = y ↔ x.hom = y.hom

instance SFinKer.instIsSFiniteKernelCarrierHom {X Y : SFinKer} {κ : X.Hom Y} :

ProbabilityTheory.IsSFiniteKernel κ.hom

@[implicit_reducible]

noncomputable instance SFinKer.instLargeCategory :

CategoryTheory.LargeCategory SFinKer

@[simp]

theorem SFinKer.comp_hom {X✝ Y✝ Z✝ : SFinKer} (κ : X✝.Hom Y✝) (η : Y✝.Hom Z✝) :

(CategoryTheory.CategoryStruct.comp κ η).hom = η.hom.comp κ.hom

@[simp]

theorem SFinKer.id_hom (X : SFinKer) :

(CategoryTheory.CategoryStruct.id X).hom = ProbabilityTheory.Kernel.id

theorem SFinKer.hom_ext {X Y : SFinKer} {κ η : X ⟶ Y} (h : κ.hom = η.hom) :

κ = η

theorem SFinKer.hom_ext_iff {X Y : SFinKer} {κ η : X ⟶ Y} :

κ = η ↔ κ.hom = η.hom

@[implicit_reducible]

noncomputable instance instMonoidalCategorySFinKer :

CategoryTheory.MonoidalCategory SFinKer

@[simp]

theorem leftUnitor_hom_hom (X : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = ProbabilityTheory.Kernel.id.map Prod.snd

@[simp]

theorem tensorUnit_carrier :

(CategoryTheory.MonoidalCategoryStruct.tensorUnit SFinKer).carrier = PUnit.{u + 1}

@[simp]

theorem rightUnitor_hom_hom (X : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = ProbabilityTheory.Kernel.id.map Prod.fst

@[simp]

theorem tensorObj_carrier (X Y : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).carrier = (X.carrier × Y.carrier)

@[simp]

theorem whiskerLeft_hom (X Y₁ Y₂ : SFinKer) (κ : Y₁ ⟶ Y₂) :

(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X κ).hom = ProbabilityTheory.Kernel.id.parallelComp κ.hom

@[simp]

theorem whiskerRight_hom {X₁✝ X₂✝ : SFinKer} (κ : X₁✝ ⟶ X₂✝) (Y : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.whiskerRight κ Y).hom = κ.hom.parallelComp ProbabilityTheory.Kernel.id

@[simp]

theorem rightUnitor_inv_hom (X : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = ProbabilityTheory.Kernel.id.map fun (x : X.carrier) => (x, PUnit.unit)

@[simp]

theorem tensorHom_def {X₁ Y₁ X₂ Y₂ : SFinKer} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :

CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.CategoryStruct.comp ((fun {X₁ X₂ : SFinKer} (κ : X₁ ⟶ X₂) (Y : SFinKer) => { hom := κ.hom.parallelComp ProbabilityTheory.Kernel.id, property := ⋯ }) f X₂) ((fun (X Y₁ Y₂ : SFinKer) (κ : Y₁ ⟶ Y₂) => { hom := ProbabilityTheory.Kernel.id.parallelComp κ.hom, property := ⋯ }) Y₁ X₂ Y₂ g)

@[simp]

theorem leftUnitor_inv_hom (X : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = ProbabilityTheory.Kernel.id.map fun (x : X.carrier) => (PUnit.unit, x)

@[simp]

theorem associator_inv_hom (X Y Z : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = ProbabilityTheory.Kernel.id.map fun (x : X.carrier × Y.carrier × Z.carrier) => ((x.1, x.2.1), x.2.2)

@[simp]

theorem associator_hom_hom (X Y Z : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = ProbabilityTheory.Kernel.id.map fun (x : (X.carrier × Y.carrier) × Z.carrier) => (x.1.1, x.1.2, x.2)

@[simp]

theorem tensorObj_str (X Y : SFinKer) :

(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).str = Prod.instMeasurableSpace

@[simp]

theorem tensorUnit_str :

(CategoryTheory.MonoidalCategoryStruct.tensorUnit SFinKer).str = PUnit.instMeasurableSpace

@[implicit_reducible]

noncomputable instance instSymmetricCategorySFinKer :

CategoryTheory.SymmetricCategory SFinKer

@[simp]

theorem braiding_inv_hom (X Y : SFinKer) :

(β_ X Y).inv.hom = ProbabilityTheory.Kernel.swap Y.carrier X.carrier

@[simp]

theorem braiding_hom_hom (X Y : SFinKer) :

(β_ X Y).hom.hom = ProbabilityTheory.Kernel.swap X.carrier Y.carrier

@[implicit_reducible]

noncomputable instance instComonObjSFinKer {X : SFinKer} :

CategoryTheory.ComonObj X

@[simp]

theorem counit_hom {X : SFinKer} :

CategoryTheory.ComonObj.counit.hom = ProbabilityTheory.Kernel.discard X.carrier

@[simp]

theorem comul_hom {X : SFinKer} :

CategoryTheory.ComonObj.comul.hom = ProbabilityTheory.Kernel.copy X.carrier

@[implicit_reducible]

noncomputable instance instCopyDiscardCategorySFinKer :

CategoryTheory.CopyDiscardCategory SFinKer