Monoidal category tools for non category theory objects

Stream: mathlib4

[Rémy Degenne]

I am working with objects that are not implemented as a category in Mathlib, but I want to use some cool operations and tactics from the category theory part of Mathlib, and I am not sure on how to proceed.

In the probability theory part of the library, I am working with measurable spaces (docs#MeasurableSpace) and probability transition kernels (docs#ProbabilityTheory.Kernel) that map one measurable space to another. When composing kernels, issues can arise: you can't compose κ : Kernel α' (α × (β × γ)) and η : Kernel ((α × β) × γ) δ because the two products of three spaces are not the same type because the parentheses are not at the same place. To compose them, you have to insert a measurable equivalence between the measurable spaces and in more complex cases the code can get long and hard to read. On paper, you would just compose them and not even mention the associativity issue.

Now if we take a category theory point of view, measurable spaces and kernels are a symmetric monoidal category (under some restriction on the kernels we consider). If you restrict the kernels enough, they are even a Markov category as discussed here recently .
That means that if the κ and η discussed above were implemented as morphisms in such a category, I could write κ ⊗≫ η to use docs#CategoryTheory.monoidalComp, which automatically finds and inserts the associator needed, and I could also use the coherence tactics Yuma Mizuno is PRing to mathlib these days. If possible, I'd also like to use string diagrams for kernels.

The main question is: how do I get to use the category theory definitions and tactics for kernels?

I see an ugly solution, which is to copy the definitions and tactics but specialize them to the case of measurable spaces and kernels instead of objects and morphisms in a monoidal category. I would defined a specialized MonoidalCoherence class which uses measurable equivalences and a monoidalComp for kernels. That's a lot of duplication and not very appealing.

Is there a better solution? Was a similar thing done somewhere else in the library?

[Yaël Dillies]

Do you know about prod_assoc%, the elaborator that automatically reassociates products?

[Rémy Degenne]

I don't! Do you have a link to some doc? Will it allow me to write compositions as easily as κ ⊗≫ η?

[Rémy Degenne]

(found the doc by myself)

[Yaël Dillies]

I don't know how ⊗≫ works exactly in category theory but I believe the heavy lifting is done by prod_assoc%

[Rémy Degenne]

prod_assoc% produces equivalences between products, but I would need measurable equivalences. Also I would really like to not have any equivalences at all (as in, not see them in the code).

[Adam Topaz]

Yaël Dillies said:

I don't know how ⊗≫ works exactly in category theory but I believe the heavy lifting is done by prod_assoc%

No, these are two completely different things. The monoidal one adds in isomorphisms on the fly, assuming the isomorphism is something that holds true in the free monoidal category. prod_associs indeed just for (type-level) products.

[Adam Topaz]

the benefit of prod_assoc% over the monoidal category one is that you can let the components of the product live in arbitrary universes.

[Adam Topaz]

if you want to use the monoidal category infrastructure, then you would need to introduce a monoidal category at some point. IIRC the Kleisli category of the Giry monad is supposed to be the category whose morphisms are Markov kernels, is that right?

[Adam Topaz]

BTW, the equivalences produced by prod_assoc% are extremely simple and exactly what you expect, so a measurability tactic should be able to discharge measurability proof obligations for such maps. But again, this elaborator is weaker than what the monoidal coherence tactic does since it only accounts for associativity, and not commutativity or units.

[Adam Topaz]

I think the nice way to accomplish this using existing category theory infrastructure is to prove that the Kleisli category of a monoidal monad is monoidal ( :sunglasses: ), then specialize to whatever variant of the Giry monad you want.

[Rémy Degenne]

I agree that at some point I have to introduce a monoidal category, and I have partial code to prove that the Kleisli category of a monoidal monad is monoidal and I could apply that to some variant of the Giry monad. At some point it's clear I have to prove that those monoidal results apply to my objects.

But I have no Idea how that would help me work with the type Kernel. I could prove a bunch of results for Markov categories, sure, or for copy-discard categories or whatever, but then I want to use them with the non-category types MeasurableSpace and Kernel. And I have no idea how to do that transfer.

[Adam Topaz]

A kernel is a morphism in the Kleisli category, isn’t it?

[Adam Topaz]

If you’re opposed to using the category theory API, then you will probably have to do some duplication

[Rémy Degenne]

Yes they are morphisms in that category, but I also don't understand why you ask. I have actually written several paragraphs to answer and then deleted them repeatedly because I kept thinking that there is something perhaps simple that I am missing, related to that question.

I clearly have not enough experience with categories in Lean that are not "some generic category" but actually a category with objects and morphisms given by some types. I'll build a category of measurable spaces and Markov kernels, play with it, and come back with questions supported by actual code. That will be better than vague questions like the one above.

[Johan Commelin]

@Rémy Degenne do I understand correctly that you are asking what the most ergonomic way is to move back and forth between the unbundled language of Kernel and the "bundle everything into objects and morphisms of a category" language that is needed to apply the cool tactics?

[Rémy Degenne]

That's definitely something I'd like to know more about. If you have an example of code where such back-and-forth is done, I'd like to look at that.

[Johan Commelin]

For categories of groups, rings, modules, etc, we typically have definitions like CommRingCat.of R that search for a [CommRing R] instance and then bundle that up together with R into an object of CommRingCat

[Johan Commelin]

It's not as transparent as I would like it to be.

[Sébastien Gouëzel]

Doesn't category theory force you to consider objects in the same universe?

[Adam Topaz]

Sorry for the confusion @Rémy Degenne -- Here are some further details: First, for a specific monad $M$ on a monoidal category which satisfies some assumptions, you can construct the category CategoryTheory.Kleisli . As you can see, this is just a type alias, but it has a different category structure where a morphism $X \to Y$ in there is, by definition a morphism $X \to M Y$ in the original category. So, if you take $C$ to be the category of (bundled) measurable spaces with morphisms being measurable morphisms, and take $G$ to be some Giry monad, if you use this construction you get an alias for the type of measure spaces which has a different category structure where morphisms are "kernels", except that these kernels are defined in terms of docs#Quiver.Hom . You can easily define an equivalence between such types of morphisms and the type of kernels that already exist in the measure theory library, but they won't be defeq. And yes, as @Sébastien Gouëzel mentions, this approach will force you to put some artificial universe restrictions.

[Adam Topaz]

Unfortunately this is the only way to use the monoidal coherence automation. If you want to stick to the unbundled approach, and avoid these universe restrictions, then you would have to develop some custom automation (e.g. similar to prod_assoc%)

[Rémy Degenne]

Thanks for the explanation, I get better now how the morphisms of the category and the other kernels would be related. I'll definitely implement that category and the equivalence you mention, play with it and try to get a better idea of what results about Kernel I can or cant get from it.

[Adam Topaz]

I hope you don't have to work too hard:

import Mathlib

noncomputable section
open CategoryTheory

def KernelCat := Kleisli MeasCat.Giry


namespace KernelCat
instance : Category KernelCat := inferInstanceAs (Category <| Kleisli _)

instance : CoeSort KernelCat (Type _) where
  coe X := show MeasCat from X

example (X : KernelCat) : MeasurableSpace X := inferInstance

example {X Y : KernelCat} (f : X ⟶ Y) : ProbabilityTheory.Kernel X Y where
  toFun := f.val
  measurable' := f.property

example {X Y : KernelCat} (f : ProbabilityTheory.Kernel X Y) : X ⟶ Y := ⟨f, f.measurable⟩

[Adam Topaz]

In fact, if we have a class ProbabilityTheory.KernelLike (should we?) then you could put such an instance on homs in KernelCat and call it a day!

[Rémy Degenne]

Thanks for the example! I'll experiment with the KernelLike approach you mention.

That particular category won't have a particularly nice structure because our Giry monad is not the same as the Giry monad in most papers (ours does not restrict to probability measures) but defining the other monad will be easy. Proving that the category is monoidal will require more work, but I have started doing that some time ago.