lawvere theories

Stream: maths

[Chris Grossack (they/them)]

Hey all! I'm new to LEAN, but I have a student who wants to formalize something and this seems like a great excuse for me to learn.

He's interested in category theory, and I noticed that there's no lawvere theories (confirmed by @Johan Commelin). Do you know roughly how hard it would be to formalize some of the definitions and prove a few theorems (for instance, categories of models always have limits/colimits, etc)? Does that sound like a good first topic (for both me and the student)?

[Adam Topaz]

Implementing Lawvere theories involves a lot of important design decisions at the very beginning (and we can certainly help with all that here on zulip). Once the basic definitions are set up, proving things like existence of (co)limits sounds like a nice project.

[Chris Grossack (they/them)]

Fantastic! What kinds of design decisions are you forseeing? Or maybe it makes more sense to ask that after I've read more of MIL?

[Adam Topaz]

Well, you need to decide whether to define your type of objects to be $\mathbb{N}$ or something less evil. Also, the mathlib philosophy is to define things in the appropriate level of generality, and presumably this means that one should define multi-sorted Lawvere theories and specialize to the case of a single sort if needed

[Adam Topaz]

Finally, there is the issue of relating the abstract categorical situation to concrete categories like docs#Group and to theories as defined in model theory (which we have in mathlib)

[Chris Grossack (they/them)]

Aaaah, gotcha. Yeah, I see that we already have bicategories implemented. So my (very rough) plan was to define the bicategory of finite product categories/finite product functors/natural transformations, and define a (Set)-model to be a fp-functor into Set. That's the right level of generality, imo, since it's the level that lets us prove lawvere duality (the 2-equivalence between canonical theories and models).

[Chris Grossack (they/them)]

And yeah, I wouldn't even know how to start relating these things to concrete categories like Group... I would need a ton of advice on doing that, haha

[Adam Topaz]

Sorry, what is a "finite product category" in this context?

[Chris Grossack (they/them)]

Categories which admit finite products, and functors which preserve them. The "classical" case is where there's a single generator X and every object is a finite product of copies of X. The "multisorted" case is where there's some family of generators, {X_i}, and every object is a finite product of the X_i, but the theory goes through in any category with finite products

[Adam Topaz]

Ok I see. So what is a "canonical theory"?

[Adam Topaz]

I'm just trying to tease out the relevant parts of the definition :)

[Chris Grossack (they/them)]

No worries at all! I'm very literally here to ask about making all this stuff precise, haha. I'm sure your questions are nothing next to the detail I'll have to give LEAN :P

[Chris Grossack (they/them)]

It turns out you can have two inequivalent fp-categories A and B with equivalent categories of models (fp functors into Set). So we have no hope of recovering the theory from the category of models in this level of generality. Buuuut, any two such A and B have equivalent "cauchy completions", and we _can_ recover a cauchy complete theory from the category of models. With this in mind, we call a cauchy complete finite product category a "canonical theory". Then we get a 2-equivalence

{canonical theories, fp functors, natural transformations} <--> {algebraic categories, algebraic functors, natural transformations}

[Adam Topaz]

sorry (again)... what does "cauchy complete" mean here?

[Chris Grossack (they/them)]

We can avoid this by working with finite limit (lex) theories instead. So our theories are categories with all finite limits, and our models are finite limit functors into Set. Then since every finite limit category is already cauchy complete, we don't have this issue. So we get a nice clean 2-equivalence

{finite limit categories, finite limit functors, natural transformations} <--> {locally presentable categories, functors preserving limits and filtered colimits, natural transformations}

This is "Gabriel-Ulmer Duality", and we still get something of independent interest. Where finite product theories agree with classical equational theories in algebra, the finite limit theories agree with "essentially algebraic" theories (algebraic theories where we allow operations to be partially defined).

[Chris Grossack (they/them)]

So Gabriel-Ulmer duality is slightly easier in that we don't have to restrict to canonical theories, but it feels a bit odd to start there instead of lawvere theories (at least imo)

[Chris Grossack (they/them)]

And no worries (again) :P. "Cauchy Complete" has two (equivalent) definitions:

1. C is cauchy complete if it has all absolute colimits
2. C is cauchy complete if every idempotent splits (an idempotent is an arrow e with ee = e, see here https://ncatlab.org/nlab/show/idempotent)

[Adam Topaz]

And does "algebraic category" mean a category with limits and filtered colimits which is concrete and the forgetful functor reflects isos, preserves limits and filtered colimits, or something else?

[Adam Topaz]

anyway, if I understand correctly, there is some 2-categorical adjunction between what you call "finite product categories" and "algebraic categories" which is "cauchy completion" when you go from fpcat to alg-cats back to fpcats and which is isomorphic to the identity when you go from alg-cat to fpcats and back. This would be a nice way to formulate things.

[Chris Grossack (they/them)]

In case your theory has a single sort, then yes. In case you have S many sorts, you want the forgetful functor to be valued in Set^S. For a general finite product theory, the definition is slightly more involved and I don't remember it off the top of my head. It's something like "cocomplete with a set G of objects so that every object is a sifted colimit of objects in G". I can look it up in Adamek et al's "Algebraic Theories".

[Adam Topaz]

oh yeah I had in mind the single-sorted case

[Chris Grossack (they/them)]

I usually do too, haha

[Chris Grossack (they/them)]

Adam Topaz said:

anyway, if I understand correctly, there is some 2-categorical adjunction between what you call "finite product categories" and "algebraic categories" which is "cauchy completion" when you go from fpcat to alg-cats back to fpcats and which is isomorphic to the identity when you go from alg-cat to fpcats and back. This would be a nice way to formulate things.

Yeah, this is morally right.

To a finite product category T you associate an algebraic category [T,Set] of finite product functors T --> Set.

To an algebraic category A you associate a finite product category "the opposite of the category of 'perfectly presentable' (read: generalized free) objects"

Then you can show that
A --> A_pp^op --> [A_pp^op, Set]
is an equivalence of categories, and moreover
T --> [T,Set] --> [T,Set]_pp^op
is the cauchy completion of T

So if we restrict attention to theories which are cauchy complete, this gives us a 2-equivalence.