4. 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

All the equalities are lifted to a common universe level, so that the resulting categorical equalities live in the same category and can be used to rewrite each other.

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, the derived operations κ ×ₖ η and κ ⊗ₖ η are unfolded into compositions, parallel compositions and copies (unfoldKernelOp).
Then, the equality is lifted to a common universe level with the machinery of lift_eq, together with a proof of equivalence. When the tactic is applied at several locations, all the equalities are lifted to the same universe level, so that the translated equalities live in the same category and can be used to rewrite each other.
Next, it recursively traverses the lifted equality and creates a new expression where each kernel is replaced by its translation in the SFinKer category. The kernel operations are translated to the corresponding categorical operations (composition, tensor product, whiskers, identity, unitors, associators, braiding, copy and discard), and the other kernels κ to κ.hom. Each translated subexpression comes with a proof that it is the translation of the original one, built by congruence from the translation lemmas. This is done using the transformKernelToHom function.
🔗opaque
```
transformKernelToHom (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
transformKernelToHom (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
```
Recursive transformation from kernel expressions to morphism expressions in the SFinKer category. Returns the morphism expression e' together with a proof of e' = e.hom, built by congruence from the translation lemmas (comp_hom, parallelComp_hom, ...).
Finally, the proofs of the two sides give, with hom_congr, a proof that the lifted equality is equivalent to the categorical one, which replaces the goal or the hypothesis.