5. hom_kernel tactic🔗

The hom_kernel tactic is the inverse of kernel_hom. It transforms categorical equalities in the SFinKer category back into equivalent kernel equalities. For example, given morphisms κ.toHom ≫ η.toHom = ξ.toHom in the SFinKer category, the tactic transforms it back to the kernel equality η ∘ₖ κ = ξ.

def

HomKernel.homKernel : Lean.ParserDescr
HomKernel.homKernel : Lean.ParserDescr

The hom_kernel tactic is the inverse of kernel_hom: it transforms an equality written in the monoidal category back to an equivalent equality of s-finite kernels.

The tactic supports location specifiers like rw or simp:

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

It is useful to switch back to kernel equations once categorical rewrites are done.

The tactic can be described in 4 steps:

First, it recursively traverses the categorical equality and creates a new expression where each morphism is replaced by its kernel counterpart: the categorical operations (composition, tensor product, whiskers, identity, unitors, associators, braiding, copy and discard) are translated to the corresponding kernel operations, and κ.toHom to κ. As for kernel_hom, each translated subexpression comes with a proof given by the same congruence lemmas. This is done using the homToKernel function.
🔗opaque
```
HomKernel.homToKernel (u : Lean.Level) (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
HomKernel.homToKernel (u : Lean.Level)
  (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
```
Recursive translation of a morphism e of SFinKer.{u} into a kernel e'. 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 objCarrier. 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, ...).
Then, the resulting equality of lifted kernels is un-lifted to the original universe levels of the carrier spaces with the machinery of unlift_eq.
The products ×ₖ and composition-products ⊗ₖ, which kernel_hom unfolds into copies, parallel compositions and structural kernels, are folded back by the function foldKernelOp. As the compositions of kernels associate to the left, a product preceded by a kernel ξ reads ξ ∘ₖ (κ ∥ₖ η) ∘ₖ copy X, which does not contain the unfolding (κ ∥ₖ η) ∘ₖ copy X of κ ×ₖ η as a subterm. Each operation is therefore folded by two lemmas, with and without such a prefix, such as comp_parallelComp_comp_copy_eq_comp_prod and parallelComp_comp_copy for ×ₖ. A product written unfolded in the original equality is folded as well.
🔗def
```
foldKernelOp (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)
foldKernelOp (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
```
Fold back Kernel.compProd and Kernel.prod in an expression, in the form produced by unfoldKernelOp and possibly reassociated. Returns the folded expression e' together with a proof of e = e'. As the compositions associate to the left, an operation preceded by a kernel ξ is not a subterm of its unfolding, ξ ∘ₖ (κ ∥ₖ η) ∘ₖ copy α for a product: each operation is folded by two lemmas, with and without such a prefix. Kernel.compProd is folded first, since its unfolding contains the unfolding (Kernel.id ∥ₖ κ) ∘ₖ copy α of a product.
Finally, the proofs are combined, with toHom_congr_of_eq, into a proof that the categorical equality is equivalent to the kernel equality, which replaces the goal or the hypothesis.

Note that when PUnit is encountered during the un-lifting process, it un-lifts to Unit, no matter the universe level of the original PUnit carrier. This is because PUnit is used as the unit object of the monoidal structure, which makes it hard to recover the original universe level.