4. 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 translation as a kernel expression, uniformly un-lifting carrier spaces from the common universe level to their original universe levels using measurable equivalences. During this process, it recognizes patterns of categorical composition and identities, and translates them to the corresponding kernel operations (composition, identity, parallel composition, etc...). This is done using the transformHomToKernel function.
🔗opaque
```
transformHomToKernel (eLevel : Lean.Level) (e : Lean.Expr)
  (op_data : List CategoryOP) : Lean.MetaM (Lean.Expr × List CategoryOP)
transformHomToKernel (eLevel : Lean.Level)
  (e : Lean.Expr)
  (op_data : List CategoryOP) :
  Lean.MetaM (Lean.Expr × List CategoryOP)
```
Recursive transformation from morphism expression in SFinKer to kernel expression.
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.

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.