Universal Algebra

Stream: Is there code for X?

[Marcus Rossel]

Is there a notion of an algebra in mathlib that matches this?:

Algebra

More specifically I'm actually looking for this notion of an algebra being freely generated:

Freely Generated

[Eric Wieser]

Do you have a reference for this? Searching for "sigma algebra" finds σ not Σ

[Marcus Rossel]

@Eric Wieser https://arxiv.org/abs/2212.05529

[Eric Wieser]

I think you probably need 2.6.1 in your screenshot too

[Marcus Rossel]

I've updated it accordingly.

[Eric Wieser]

this looks to me like the model_theory stuff, perhaps starting with docs#first_order.language

[Adam Topaz]

We have had many MANY discussions about universal algebra

[Adam Topaz]

And yes one way to model this is using model theory

[Adam Topaz]

We don't have any free stuff in mathlib, but take a look at www.github.com/adamtopaz/univalg

[Martin Dvořák]

If we do more computer science in Lean, universal algebra will come really handy!
(apart from wanting to have the math for its own sake)

[Kevin Buzzard]

I'll advertise my former MSc student @Joseph Hua whose masters thesis was a lean 3 formalisation of the model theory proof of the Ax-Grothendieck theorem.

[Pedro Sánchez Terraf]

Just for reference: Trendy stuff in universal algebra includes the Constraint Satisfaction Problem (related to P vs NP, one important paper here settling a conjecture) and tame congruence theory (leading to this JAMS paper). Another nice piece of math is commutator theory, which provides vast generalizations of results that were only known for groups and rings (see here, for example).

[David Wärn]

I think much of the value in formalising universal algebra would come from proving relatively basic results about varieties (e.g. existence of (co)limits and creation of filtered colimits) and making sure they can be transferred to classes in mathlib's algebraic hierarchy. This would save us from having to reprove each result for each class