6. Kernelized monoidal composition🔗

The translation of kernels to morphisms in the SFinKer category allows to adapt the “⊗≫” monoidal composition for kernels. The MeasurableCoherence class witnesses measurable equivalences between types, enabling an instance of categorical MonoidalCoherence that makes the kernelized monoidal composition (noted “⊗≫ₖ”) possible.

6.1. Measurable Coherence🔗

The MeasurableCoherence class witnesses the existence of measurable equivalences between two measurable spaces. It acts as a kernel-level counterpart to the categorical MonoidalCoherence class:

type class

MeasurableCoherence.{u_1, u_2} (X : Type u_1) (Y : Type u_2)
  [MeasurableSpace X] [MeasurableSpace Y] : Type (max u_1 u_2)
MeasurableCoherence.{u_1, u_2}
  (X : Type u_1) (Y : Type u_2)
  [MeasurableSpace X]
  [MeasurableSpace Y] : Type (max u_1 u_2)

A class witnessing the existence of a measurable equivalence between two measurable spaces.

Instance Constructor

MeasurableCoherence.mk.{u_1, u_2}

Methods

miso : X ≃ᵐ Y

A measurable equivalence between X and Y.

This class enables an instance of MonoidalCoherence between SFinKer objects at a common universe level via the monoidalCoherence function, using measurable equivalences from the original types.

def

MeasurableCoherence.monoidalCoherence.{w, x, y} {X : Type x}
  {Y : Type y} [MeasurableSpace X] [MeasurableSpace Y]
  [mXY : MeasurableCoherence X Y] {X' Y' : Type w} [MeasurableSpace X']
  [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) :
  CategoryTheory.MonoidalCoherence { carrier := X', str := inst✝ }
    { carrier := Y', str := inst✝¹ }
MeasurableCoherence.monoidalCoherence.{w,
    x, y}
  {X : Type x} {Y : Type y}
  [MeasurableSpace X] [MeasurableSpace Y]
  [mXY : MeasurableCoherence X Y]
  {X' Y' : Type w} [MeasurableSpace X']
  [MeasurableSpace Y'] (ex : X' ≃ᵐ X)
  (ey : Y' ≃ᵐ Y) :
  CategoryTheory.MonoidalCoherence
    { carrier := X', str := inst✝ }
    { carrier := Y', str := inst✝¹ }

MeasurableCoherence gives an instance of MonoidalCoherence in the SFinKer category.

This allows to bridge the gap between the notion of measurable equivalence and the categorical notion of monoidal coherence, enabling the use of categorical machinery for kernel compositions.

6.2. Monoidal Composition of Kernels🔗

The kernelized monoidal composition “⊗≫ₖ” is defined by composing two kernels while automatically handling measurable equivalences through the categorical framework:

Transport to SFinKer: Both kernels are translated to morphisms in the SFinKer category using the hom function, which lifts carrier spaces to a common universe level.
Categorical composition: The categorical monoidal composition “⊗≫” is applied to the resulting morphisms in SFinKer, which automatically inserts the necessary associators and unitors.
Transport back to kernels: The result is translated back to a kernel using the fromHom function.