1.1. Usage🔗

To use Kernel-Hom, add the following to your lakefile.toml:

[[require]]
name = "kernelhom"
git = "https://github.com/gaetanserre/KernelHom.git"

or to your lakefile.lean:

require kernelhom from git "https://github.com/gaetanserre/KernelHom" @ "main"

Then, in your Lean files, you can import the library with:

import KernelHom

Tactics

The library provides several tactics for working with s-finite kernels equalities. The main tactics are:

• kernel_hom: Transforms a s-finite kernel equality into an equality in the SFinKer monoidal category.

• hom_kernel: The inverse of kernel_hom, transforms an equality in SFinKer back into a kernel equality.

• kernel_monoidal: Applies the monoidal tactic to a s-finite kernel equality.

• kernel_coherence: Applies the coherence tactic to a s-finite kernel equality.

Basically, whenever you have a equality of s-finite kernels that you want to simplify, you can apply kernel_hom to transform it into a categorical equality, try applying categorical tactics, simps, or manually manipulate it, and then apply hom_kernel to get back to a kernel equality if needed. The built-in helpers kernel_monoidal and kernel_coherence directly apply categorical tactics to kernels without needing to manually invoke the translation tactic.

Kernel diagrams

The library also provides the kernel_diagram command, which generates string diagrams for kernel expressions. This is an adaptation of the string_diagram command, where s-finite kernels are represented as morphisms using kernel_hom. This provides a visual representation of kernel compositions and transformations, aiding intuition and understanding. The use of this command is similar to string_diagram:

1.2. Examples🔗

These tactics are particularly useful when dealing with compositions and parallel compositions of kernels. The following examples are taken from the file KernelLemmas.lean and illustrate how the tactics can be used to drastically simplify the proofs of kernel equalities.

• parallelComp_id_left_comp_parallelComp

• parallelComp_id_right_comp_parallelComp

• parallelComp_comp_parallelComp

• parallelComp_comp_prod

• swap_parallelComp

  Object of the symmetric category are also handled by the tactic, such as Kernel.swap that is translated to the right braiding of SFinKer.

• deterministic_comp_copy

  The categorical counterpart of Kernel.deterministic are automatically treated as Deterministic morphisms.