Lean 4 project focused on tactics that translate kernel equalities into categorical equalities, and back. This work is still in early stages, but the core tactics are already implemented and can be used to simplify kernel equalities by leveraging categorical reasoning.
For more information, see the project homepage and the full documentation.
This repository is mainly about the tactics kernel_hom and hom_kernel.
They are built on top of SFinKer, the category of measurable spaces with s-finite kernels as morphisms. This categorical layer is the key reason the tactic workflow works.
Very briefly, the tactics:
- translate an equality of s-finite kernels into an equality in categorical/monoidal form,
- let you run category-theory tactics such as
coherenceormonoidal, - translate the result back to a kernel equality.
Universe handling is part of this translation: expressions are lifted to a common universe level, so rewrites stay well-typed across universe levels.
In addition, SFinKer also gives a direct route to Stoch, the Markov category of measurable spaces and Markov kernels, defined as the wide subcategory of SFinKer with Markov kernels as morphisms. The definitions/results for SFinKer and Stoch are now in Mathlib (PR #36779).
The translation from kernels to categorical expressions allows to use any tool from category theory within the context of kernels, such as string diagram visualization or monoidal composition.
The library provides the kernel_diagram command that generates a string diagram for a given kernel expression. This can be useful for visualizing complex kernel compositions and understanding the structure of kernel equalities.
#kernel_diagram ProbabilityTheory.Kernel.deterministic_comp_copy
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.
Add this in your lakefile.toml:
[[require]]
name = "kernelhom"
git = "https://github.com/gaetanserre/KernelHom"If you're using a lakefile.lean, add:
require verso from git "https://github.com/gaetanserre/KernelHom"@"latest"See Examples for examples of how to use the tactics.
- Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Adv. Math. 370 (2020), 107239. arXiv:1908.07021.
GNU GPL 3.0. See LICENSE.