Kernel-Hom: Tactics for Kernel Categorical Reasoning🔗

Overview

Kernel-Hom is a Lean 4 library that provides tactics to simplify kernel equalities by leveraging categorical reasoning. It automatically translates s-finite kernel equalities into equalities in a monoidal category, where tactics like monoidal or coherence can be applied, and then translates the result back to a kernel equality if needed. The translation from kernels to categorical expressions also allows to use any tool from category theory within the context of kernels, such as string diagram visualization or monoidal composition.

Documentation

The complete documentation for the library is available in the API reference.

Core of the project

The library introduces two main tactics:

• kernel_hom : transforms a kernel equality into an equality in the monoidal category.

• kernel_hom : performs the inverse transformation, bringing the categorical equality back to a kernel equality.

These tactics allow users to transform complex kernel equalities into categorical equalities, where powerful categorical tactics can be applied to simplify or prove them. To this end, the library provides built-in helpers like kernel_monoidal and kernel_coherence to apply categorical tactics directly to kernels without needing to manually invoke the translation tactics.

The library rests on SFinKer, the category of measurable spaces with s-finite kernels as morphisms, equipped with monoidal and symmetric structures. This category is also used to define Stoch, the category of measurable spaces with Markov kernels as morphisms, which is a wide subcategory of SFinKer (see  (Fritz, 2020)Tobias Fritz, 2020. “A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics”. In Advances in Mathematics.). Both categories have been merged into Mathlib (PR #36779).

Universe handling

A key aspect of the library is automatic universe management: expressions are lifted to a common universe level during translation, ensuring categorical expressions are well-typed. This allows users to work with kernels of varying universe levels without needing to manually manage universe annotations.

Kernel diagrams

The library 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 visualization of such diagrams in this documentation is made possible by the Verso code block expander made by @Yuma Mizuno.

Kernelized monoidal composition

An additional consequence of the translation to SFinKer is that one can adapt the categorical monoidal composition “⊗≫” to kernels, resulting in a kernelized monoidal composition “⊗≫ₖ”. This composition automatically handles measurable equivalences, allowing for seamless composition of kernels while maintaining s-finiteness.

About

This library is under active development and is under the GNU GPL 3.0 license. Contributions and feedback are welcome!