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 gives access to the tools of category theory for kernels, which has three main benefits:

• Proving API lemmas easily. Equalities of kernels built from compositions, parallel compositions, products, copies, discards and swaps are proved by a single call to kernel_disch, without any knowledge of the lemmas about kernels (see the examples).

• Visualizing kernels. The kernel_diagram command and the string diagram widget draw complex kernel expressions as string diagrams, which makes their structure easier to understand.

• Reasoning by calculation. A proof can be written as a calc whose lines are the mathematically meaningful rewrites, while the structural steps between them are proved automatically by the categorical tactics. Each step can moreover be visualized. In Mathlib, proofs by calculation whose steps are equalities of kernels are rare, and in calculations on measures built from kernels, each structural step is a chain of rewritings with lemmas about kernels and measures (see the calculational proof of Basu's theorem).

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_disch, kernel_monoidal, kernel_coherence and aesop_kernel to apply categorical tactics directly to kernels without needing to manually invoke the translation tactics. kernel_disch is the tactic to use by default, as it tries both cat_disch and monoidal.

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)Marginal noteShow marginal noteTobias 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. When several hypotheses and the goal are translated together (kernel_hom at h ⊢), they are all lifted to the same universe level, so that the translated equalities can be used to rewrite each other. This part is handled by the lift_eq tactic, which can also be used independently (see the GitHub repository).

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.

Kernel reassociation

The library also provides the @[kernel_reassoc] attribute, which is a variant of @[reassoc] that, given a lemma named F of shape ∀ .., f = g, where f g : Kernel X Y are s-finite kernels, will create a new lemma named F_assoc of shape ∀ .. {Z : Type u} [MeasurableSpace Z] (ξ : Kernel Y Z) [IsSFiniteKernel ξ], ξ ∘ₖ f = ξ ∘ₖ g. It first transforms the kernel equality into a categorical equality in SFinKer, then applies the @[reassoc] pipeline to generate the reassociated equality, and finally transforms the result back into a kernel equality. It comes with the term elaborator kernel_reassoc_of%, the variant of reassoc_of%, which applies the same construction to any proof of an equality of s-finite kernels, such as a local hypothesis.

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.

Implementation

The translation builds its terms and proofs directly rather than through mkAppM and rewriting: the equivalence between the original and the translated equalities is proved by congruence from the translation lemmas, and the instances, inferred types and recursively built objects (measurable equivalences, objects of SFinKer) are memoized in a cache that is reset at each call. See the Implementation of the translation page for the underlying structures.

About

This library is under active development and is under the Apache 2.0 license. Contributions and feedback are welcome!