universal algebra and filtered colimits

Stream: maths

[David Wärn]

I read about @Justus Springer's work on filtered colimits and got curious about how the universal algebra version would look, so I had a go at writing it up on branch#unialg. The idea was to use docs#category_theory.limits.colimit_limit_to_limit_colimit_is_iso to prove that the functor $X \mapsto X^n$ preserves filtered colimits. If you then consider some notion of structure (like "ring") defined by functions n-ary functions $X^n \to X$, you can define corresponding operations on the colimit type, as well as showing that they are "lawful". I didn't go so far as proving that the resulting structure is a colimit (or that the forgetful functor to Type preserves / reflects / creates filtered colimits), but there shouldn't be any obstacle to this. So far it's not too much code, but you would need some more work to connect this perspective with mathlib's notion of group / ring / etc.

[Chris Hughes]

I think the main challenge with this sort of generalisation is that translating mathlib's group, ring etc into the language of category theory and varieties isn't so complicated as to make it easier to prove theorems directly on group than apply the general theorem. I feel like this universal algebra could be unified with the first order logic stuff we already have. flypitch did a bunch of work on that, and some of it is in https://leanprover-community.github.io/mathlib_docs/model_theory/basic.html

[Chris Hughes]

Another change I would make is to introduce a characteristic predicate for a category coming from an equational theory. We should still be using the usual category Grp and then some type class on a category saying what its signature is etc.

[Justus Springer]

Wow, interesting to see this perspective being developed! I don't know much about universal algebra. Do you think the existence of limits and colimits could also be proved at this abstract level? Because for limits, you'd need pi instances for arbitrary structs right? E.g. the limit cone of F : J ⥤ Mon is defined as a submonoid of Π j, F.obj j.

[David Wärn]

Yes, limits and colimits are easy to construct. I only defined binary products but the general pi instance looks the same.

[Adam Topaz]

Whatever happens with universal algebra, it should be integrated with the model theory part of mathlib.

[Adam Topaz]

Another approach to all this stuff is through Lawvere theories.

[Reid Barton]

Chris Hughes said:

I think the main challenge with this sort of generalisation is that translating mathlib's group, ring etc into the language of category theory and varieties isn't so complicated as to make it easier to prove theorems directly on group than apply the general theorem.

Ideally we would have some meta code for this (e.g. to calculate from the definition of group a certain algebraic theory, and build an equivalence between its category of models and the category of groups)

[David Wärn]

Yes. One approach would be

1. define a typeclass is_algebraic C for concrete categories C, to say that C is equivalent to the category of algebras of some algebraic theory (and that this equivalence commutes with the forgetful functor)
2. inhabit this typeclass for categories like Mon, Group, Ring (by hand or using metaprogramming)
3. for any is_algebraic C, prove that C has limits and colimits and that the forgetful functor is monadic / creates limits / preserves filtered colimits.

In the end you'd get theorems about Group instead of group, but I guess that's fine.

[Chris Hughes]

The other problem which needs quite a lot of thought is that a lot of the time stronger versions of the theorems exist in particular equational theories. E.g. if the equational theory has no functions of arity 2 or greater then I think the forgetful functor preserves all colimits not just directed ones.

Depending how far this goes, you probably want some typeclass for an equational theory that extends groups so that you can state theorems in terms of kernels in those categories instead of congruence relations.

You probably want a slightly different version of the theory for each category.