Kernel Categorical Reasoning

6. Kernel reassociation🔗

The translation of kernels to morphisms in the SFinKer category allows to adapt the @[reassoc] attribute to equalities of s-finite kernels.

To this end, the library provides the @[kernel_reassoc] attribute, which is a variant of @[reassoc] that, given a lemma named F of shape ∀ .., f = g, where f g : Kernel X Y are s-finite kernels, will create a new lemma named F_assoc of shape ∀ .. {Z : Type u} [MeasurableSpace Z] (ξ : Kernel Y Z) [IsSFiniteKernel], ξ ∘ₖ f = ξ ∘ₖ g. As a new measurable space Z is introduced, the new declaration has a new universe level, which prevents the use of the @[reassoc] pipeline. Instead, @[kernel_reassoc] mirrors the structure of @[reassoc] but uses the kernelReassocHandler function to generate the proof of the new declaration. It first transforms the kernel equality into a categorical equality in SFinKer, then applies the @[reassoc] pipeline to generate the reassociated equality, and finally transforms the result back into a kernel equality.

🔗def
kernelReassocHandler (h_eq : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Array Lean.LMVarId)
kernelReassocHandler (h_eq : Lean.Expr) :
  Lean.MetaM
    (Lean.Expr × Array Lean.LMVarId)

Core handler for @[kernel_reassoc].

Given an equality between s-finite kernels, this constructs the corresponding reassociated equality in SFinKer category, under the extra Z measurable space and instance binders needed to state the result. The returned array contains the fresh level metavariables that still need to be added to the declaration's universe levels.

6.1. Example🔗

The @[kernel_reassoc] attribute works the exact same way as @[reassoc], but for equalities of s-finite kernels:

@[kernel_reassoc] lemma parallelComp_self_comp_copy' [IsMarkovKernel κ] [IsDeterministic κ] : (κ ∥ₖ κ) ∘ₖ copy (X × Y) = copy Z ∘ₖ κ := X:Type u_1Y:Type u_2Z:Type u_3inst✝⁴:MeasurableSpace Xinst✝³:MeasurableSpace Yinst✝²:MeasurableSpace Zκ:Kernel (X × Y) Zinst✝¹:IsMarkovKernel κinst✝:IsDeterministic κ⊢ κ ∥ₖ κ ∘ₖ copy (X × Y) = copy Z ∘ₖ κ All goals completed! 🐙variable {W : Type*} [MeasurableSpace W] (ξ : Kernel (Z × Z) W) [IsSFiniteKernel ξ] parallelComp_self_comp_copy'_assoc κ ξ : ξ ∘ₖ (κ ∥ₖ κ) ∘ₖ copy (X × Y) = ξ ∘ₖ copy Z ∘ₖ κ#check parallelComp_self_comp_copy'_assoc κ ξ 
parallelComp_self_comp_copy'_assoc κ ξ : ξ ∘ₖ (κ ∥ₖ κ) ∘ₖ copy (X × Y) = ξ ∘ₖ copy Z ∘ₖ κ