Zulip Chat Archive

Stream: maths

Topic: universal algebra and filtered colimits


David Wärn (Sep 17 2021 at 18:57):

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 XXnX \mapsto X^n preserves filtered colimits. If you then consider some notion of structure (like "ring") defined by functions n-ary functions XnXX^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 (Sep 17 2021 at 19:14):

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 (Sep 17 2021 at 19:22):

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 (Sep 17 2021 at 19:27):

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 (Sep 17 2021 at 19:35):

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

Adam Topaz (Sep 17 2021 at 19:35):

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

Adam Topaz (Sep 17 2021 at 20:13):

Another approach to all this stuff is through Lawvere theories.

Reid Barton (Sep 18 2021 at 03:01):

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 (Sep 18 2021 at 08:53):

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 (Sep 18 2021 at 10:29):

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.


Last updated: Dec 20 2023 at 11:08 UTC