3. kernel_hom tactic🔗

The kernel_hom tactic transforms a s-finite kernel equality into an equality in the SFinKer category, where any categorical reasoning can be applied to simplify it. For example, given kernels κ : Kernel X Y, η : Kernel Y Z and ξ : Kernel X Z, the following kernel equality: η ∘ₖ κ = ξ is transformed to κ.hom ≫ η.hom = ξ.hom in the SFinKer category, where hom is the translation of kernels to morphisms in SFinKer.

def

kernelHom : Lean.ParserDescr
kernelHom : Lean.ParserDescr

The kernel_hom tactic transforms a kernel equality to an equivalent equality in the category of measurable spaces and s-finite kernels.

The tactic supports location specifiers like rw or simp:

kernel_hom — applies to the goal
kernel_hom at h — applies to hypothesis h
kernel_hom at h₁ h₂ — applies to multiple hypotheses
kernel_hom at h ⊢ — applies to hypothesis h and the goal
kernel_hom at * — applies to all hypotheses and the goal

Example:

example {W X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
    [MeasurableSpace W] (κ : Kernel X Y) (η : Kernel Y Z) (ξ : Kernel Z W)
    [IsFiniteKernel ξ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ := by
  kernel_hom
  exact Category.assoc _ _ _

The tactic can be described in 4 steps:

First, it finds the minimum common universe level for which all carrier spaces of the kernels involved in the equality can be lifted to.
Then, it recursively traverses the kernel equality and creates a new expression where each kernel is replaced by its translation in the SFinKer category, uniformly lifting carrier spaces to the common universe level determined in the first step. During this process, it recognizes patterns of kernel composition and identities, and translates them to the corresponding categorical operations (composition, identity, unitors, whiskers, monoidal composition, braiding, comul, etc...). This is done using the transformKernelToHom function.
🔗opaque
```
transformKernelToHom (maxLvl : Lean.Level) (e : Lean.Expr)
  (op_data : List CategoryOP) : Lean.MetaM (Lean.Expr × List CategoryOP)
transformKernelToHom (maxLvl : Lean.Level)
  (e : Lean.Expr)
  (op_data : List CategoryOP) :
  Lean.MetaM (Lean.Expr × List CategoryOP)
```
Recursive transformation from kernel expressions to morphism expressions in the SFinKer category.
Next, it constructs the proof of equivalence between the original kernel equality and the transformed categorical equality. This proof relies on the properties of the translation (e.g., that it preserves composition and identities) and on the fact that all kernels can be uniformly lifted to the common universe level using measurable equivalences.
Finally, it replaces the original goal or hypothesis with the transformed one.