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

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
• )

@[implicit_reducible]

instance instCoeSortSFinKerType : CoeSort SFinKer (Type u_1)

Equations

• instCoeSortSFinKerType = { coe := SFinKer.carrier }

structure SFinKer.Hom (X Y : SFinKer) : Type u

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.

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

Equations

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

@[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

Equations

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

@[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

Equations

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

@[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

Equations

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

@[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

Equations

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