Kernel-Hom: Tactics for Categorical Kernel Reasoning🔗

Overview

Kernel Hom is a Lean 4 library that provides tactics to simplify kernel equalities by leveraging categorical reasoning. It automatically translates kernel equalities into equalities in a monoidal category, where tactics like coherence or monoidal can be applied, and then translates the result back to a kernel equality.

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.

• hom_kernel : 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_coherence and kernel_monoidal 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.

Kernelized monoidal composition

One consequence of the translation to SFinKer is that we 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!