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 κ.hom ≫ η.hom = ξ.hom in the SFinKer category, the tactic transforms it back to the kernel equality η ∘ₖ κ = ξ.

def

homKernel : Lean.ParserDescr
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 3 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 κ.hom to κ. As for kernel_hom, each translated subexpression comes with a proof built by congruence. This is done using the transformHomToKernel function.
🔗opaque
```
transformHomToKernel (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
transformHomToKernel (e : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
```
Recursive transformation from morphism expression in SFinKer to kernel expression. Returns the kernel expression e' together with a proof of e = e'.hom, built by congruence from the translation lemmas (comp_hom, parallelComp_hom, ...).
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.
Finally, the proofs are combined, with hom_congr, 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.