Kernel morphisms

This file defines the transformation between categorical morphisms in SFinKer and kernel objects.

Main declarations

• fromHom: transforms a categorical morphism in SFinKer to a Kernel.
• hom: transforms a Kernel to a categorical morphism in SFinKer.

noncomputable def ProbabilityTheory.Kernel.fromHom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} (κ : SX ⟶ SY) : Kernel X Y

Transform a morphism in SFinKer into a kernel.

Equations

• ProbabilityTheory.Kernel.fromHom κ = (κ.hom.comap ⇑ex.symm ⋯).map ⇑ey

instance ProbabilityTheory.Kernel.instIsSFiniteKernelFromHom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} {κ : SX ⟶ SY} : IsSFiniteKernel (fromHom κ)

noncomputable def ProbabilityTheory.Kernel.hom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} (κ : Kernel X Y) [IsSFiniteKernel κ] : SX ⟶ SY

Transform a kernel into a morphism in SFinKer.

Equations

• κ.hom = { hom := (κ.map ⇑ey.symm).comap ⇑ex ⋯, property := ⋯ }

theorem ProbabilityTheory.Kernel.hom_apply {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} (κ : Kernel X Y) [IsSFiniteKernel κ] (a : SX.carrier) : κ.hom.hom a = (κ.map ⇑ey.symm) (ex a)

theorem ProbabilityTheory.Kernel.hom_apply' {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} (κ : Kernel X Y) [IsSFiniteKernel κ] (a : SX.carrier) {s : Set SY.carrier} (hs : MeasurableSet s) : (κ.hom.hom a) s = (κ (ex a)) (⇑ey '' s)

instance ProbabilityTheory.Kernel.instDeterministicSFinKerHomOfIsMarkovKernel {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y} {κ : Kernel X Y} [IsDeterministic κ] [IsMarkovKernel κ] : CategoryTheory.Deterministic κ.hom

theorem ProbabilityTheory.Kernel.hom_congr {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (SX SY : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (κ η : Kernel X Y) [IsSFiniteKernel κ] [IsSFiniteKernel η] : κ = η ↔ κ.hom = η.hom

theorem ProbabilityTheory.Kernel.comp_hom {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (SX SY SZ : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) (η : Kernel X Y) (κ : Kernel Z X) [IsSFiniteKernel η] [IsSFiniteKernel κ] : CategoryTheory.CategoryStruct.comp κ.hom η.hom = (η.comp κ).hom

theorem ProbabilityTheory.Kernel.parallelComp_hom {X : Type u_1} {Y : Type u_2} {T : Type u_3} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace T] [MeasurableSpace Z] (SX SY SZ ST : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) (et : ST.carrier ≃ᵐ T) (κ : Kernel X Y) (η : Kernel Z T) [IsSFiniteKernel η] [IsSFiniteKernel κ] : CategoryTheory.MonoidalCategoryStruct.tensorHom κ.hom η.hom = (κ.parallelComp η).hom

theorem ProbabilityTheory.Kernel.id_hom {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) : CategoryTheory.CategoryStruct.id SX = Kernel.id.hom

theorem ProbabilityTheory.Kernel.whiskerLeft {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (SX SY SZ : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) (κ : Kernel X Y) [IsSFiniteKernel κ] : CategoryTheory.MonoidalCategoryStruct.whiskerLeft SZ κ.hom = (Kernel.id.parallelComp κ).hom

theorem ProbabilityTheory.Kernel.whiskerRight {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (SX SY SZ : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) (κ : Kernel X Y) [IsSFiniteKernel κ] : CategoryTheory.MonoidalCategoryStruct.whiskerRight κ.hom SZ = (κ.parallelComp Kernel.id).hom

theorem ProbabilityTheory.Kernel.counit {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) : CategoryTheory.ComonObj.counit = (discard X).hom

theorem ProbabilityTheory.Kernel.comul {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) : CategoryTheory.ComonObj.comul = (copy X).hom

theorem ProbabilityTheory.Kernel.braiding_hom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (SX SY : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) : (β_ SX SY).hom = (swap X Y).hom

theorem ProbabilityTheory.Kernel.leftUnitor_hom {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) {X₀ : Type u_5} [MeasurableSpace X₀] (ex₀ : X ≃ᵐ X₀) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor SX).hom = (Kernel.id.map Prod.snd).lift.hom

theorem ProbabilityTheory.Kernel.leftUnitor_inv {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) {X₀ : Type u_5} [MeasurableSpace X₀] (ex₀ : X ≃ᵐ X₀) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor SX).inv = (Kernel.id.map fun (x : X₀) => (PUnit.unit, x)).lift.hom

theorem ProbabilityTheory.Kernel.rightUnitor_hom {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) {X₀ : Type u_5} [MeasurableSpace X₀] (ex₀ : X ≃ᵐ X₀) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor SX).hom = (Kernel.id.map Prod.fst).lift.hom

theorem ProbabilityTheory.Kernel.rightUnitor_inv {X : Type u_1} [MeasurableSpace X] (SX : SFinKer) (ex : SX.carrier ≃ᵐ X) {X₀ : Type u_5} [MeasurableSpace X₀] (ex₀ : X ≃ᵐ X₀) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor SX).inv = (Kernel.id.map fun (x : X₀) => (x, PUnit.unit)).lift.hom

theorem ProbabilityTheory.Kernel.associator_hom {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (SX SY SZ : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) {X₀ : Type u_5} {Y₀ : Type u_6} {Z₀ : Type u_7} [MeasurableSpace X₀] [MeasurableSpace Y₀] [MeasurableSpace Z₀] (ex₀ : X ≃ᵐ X₀) (ey₀ : Y ≃ᵐ Y₀) (ez₀ : Z ≃ᵐ Z₀) : (CategoryTheory.MonoidalCategoryStruct.associator SX SY SZ).hom = (deterministic ⇑MeasurableEquiv.prodAssoc ⋯).lift.hom

theorem ProbabilityTheory.Kernel.associator_inv {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (SX SY SZ : SFinKer) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) {X₀ : Type u_5} {Y₀ : Type u_6} {Z₀ : Type u_7} [MeasurableSpace X₀] [MeasurableSpace Y₀] [MeasurableSpace Z₀] (ex₀ : X ≃ᵐ X₀) (ey₀ : Y ≃ᵐ Y₀) (ez₀ : Z ≃ᵐ Z₀) : (CategoryTheory.MonoidalCategoryStruct.associator SX SY SZ).inv = (deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯).lift.hom