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 κ.toHom ≫ η.toHom = ξ.toHom in the SFinKer category, where toHom is the translation of kernels to morphisms in SFinKer.

def

KernelHom.kernelHom : Lean.ParserDescr
KernelHom.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 κ.toHom. Each translated subexpression comes with a proof that it is the translation of the original one, obtained from the proofs of its subterms by a congruence lemma such as comp_toHom_of_eq. This is done using the kernelToHom function.
🔗opaque
```
KernelHom.kernelToHom (u : Lean.Level) (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
KernelHom.kernelToHom (u : Lean.Level)
  (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
```
Recursive translation of a lifted kernel e into a morphism e' of SFinKer.{u}. Returns e' together with a proof of e' = e.toHom, where the carriers of the source and of the target of e are given by homCarrier. Each step is a single application of a translation lemma, given the translations of the subterms (Kernel.comp_toHom_of_eq, Kernel.parallelComp_toHom_of_eq, ...).
Finally, the proofs of the two sides give, with toHom_congr_of_eq, a proof that the lifted equality is equivalent to the categorical one, which replaces the goal or the hypothesis.