Reusing monoid, group, etc over equivalences

Stream: maths

[Eric Wieser]

Would it be sensible and/or possible to change monoid M etc to be defined with an additional {eqv : M → M → Prop := eq} [equivalence eqv] argument, so that they can be reused for equivalences other than eq?

Asking in the context of #3531, where it seems we end up rebuilding a lot of the algebra hierarchy

[Chris Hughes]

Equality is the only relation which allows you to make substitutions, so proving all of monoid theory for relations other than equality would be a pain. If you had a relation other than eq you would usually just take the quotient by that relation, and prove that this quotient is a monoid. I don't understand how this is related to #3531.

[Eric Wieser]

The relevance is inductive types like

| mul_assoc {a b c : pre R M} : rel (a * b * c) (a * (b * c))
| one_mul {a : pre R M} : rel (1 * a) a
| mul_one {a : pre R M} : rel (a * 1) a

which might be nicer to write as

| monoid : monoid.of rel

rather than having to repeat the definition of a monoid again.

I suppose that would require some clever elaboration of mutually inductive types that probably isn't supported.

[Chris Hughes]

I think inductive types like that are not used often enough to make it worth generalizing monoid. What may well be worth doing is writing meta code that generates that inductive relation given the definition of a monoid.

One issue to consider is the fact that the inductive relation idea does not work for all type classes. For example there is no corresponding way to inductively define the analogue of your relation rel for fields. There has to be a mechanism to check that the intersection of relations satisfying monoid.of also satisfies monoid.of. This would not be the case for field.of.

[Adam Topaz]

Yeah, just like Chris said, this trick only works for anything coming from universal algebra.

[Adam Topaz]

What you can do (and I've experimented with this in the past), is to have a "monoid builder", even without introducing any new automation.
Just take any type T endowed with a constant called one and a binary operation mul and construct the maximal quotient of T compatible with mulsuch that oneand mul induce a monoid structure.

[Adam Topaz]

Then, if you want to construct the free monoid, say, you could apply this monoid builder construction to an inductive type like this:

inductive pre (S : Type)
| of : S \to pre
| one : pre
| mul : pre \to pre \to pre

where one and mul are the two constants you feed into the monoid builder machine.

[Adam Topaz]

Here's a sketch:

import algebra

class raw_monoid (M : Type*) extends has_one M, has_mul M

namespace monoid_builder

inductive rel (M : Type*) [raw_monoid M] : M → M → Prop
| mul_assoc {a b c} : rel (a * b * c) (a * (b * c))
| mul_one {a} : rel (a * 1) a
| one_mul {a} : rel (1 * a) a
| compatl {a b c} : rel a b → rel (a * c) (b * c)
| compatr {a b c} : rel a b → rel (c * a) (c * b)

instance {M : Type*} [raw_monoid M] : monoid (quot (rel M)) := sorry

end monoid_builder

[Adam Topaz]

BTW: this could be useful here too: https://github.com/leanprover-community/mathlib/blob/47efcf3c7f7dadd98f47372c8bdcc1d220773201/src/algebra/category/Mon/colimits.lean#L66

[Yury G. Kudryashov]

We also have src#con for relations such that the quotient type has a monoid structure.

[Adam Topaz]

Oh nice. But this (and things like src#con_gen.rel ) ensure that multiplication descends to the quotient, but not necessarily that it satisfies the other axioms of a monoid.

[Adam Topaz]

But I understand what you're saying. The relfrom above could have been easily replaced with

inductive prerel (M : Type*) [raw_monoid M] : M → M → Prop
| mul_assoc {a b c} : rel (a * b * c) (a * (b * c))
| mul_one {a} : rel (a * 1) a
| one_mul {a} : rel (1 * a) a

rel := con_gen.rel (prerel M)

[Scott Morrison]

Looking at this PR, I realise we have some cases of duplication involving these universal-algebra-constructions-via-inductive-types. It doesn't apply directly to the tensor algebras PR, but for example when we build colimits in Group, or when we build free groups, we're doing very similar things. Is there some single construction out of which both of these things fall out? I feel like this should be some elementary category theory magic, but I'm blanking on it.

[Adam Topaz]

Yes. Lawvere theories

[Adam Topaz]

Forgetful functors between categories of algebras associated to morphisms of lawvere theories always have left adjoints, and they can all be constructed like this

[Adam Topaz]

@Colter MacDonald

[Scott Morrison]

So that gives the free constructions. And mumble-mumble-mumble gives the construction of colimits for some value of mumble-mumble-mumble? :-)

[Adam Topaz]

Yeah! @Colter MacDonald and I have a repo where we're doing this exact thing

[Scott Morrison]

Start PRing it. :-)

[Adam Topaz]

There are still some issues were working out.

[Scott Morrison]

(My general advice would be: work in branches of mathlib, not other repos. :-)

[Reid Barton]

With these general categorical frameworks the problem generally gets pushed backed to proving that the framework's version of the category is equivalent to the normal direct definition. For example, proving that the category of models of the theory of rings is equivalent to the category of rings.

[Adam Topaz]

Yeah I agree. The main thing we're trying to solve is to make this usable in practice.

[Reid Barton]

If the goal is only to prove that rings (say) have colimits, then I'm pretty sure it's considerably less work to do it directly than to go through Lawvere theories (or monads etc).

[Adam Topaz]

We didn't define Lawvere theories

[Reid Barton]

oh, so what do you do then?

[Adam Topaz]

We do thing in the classical "universal algebra way"

[Adam Topaz]

I.e. n-ary operations and universal axioms

[Adam Topaz]

https://github.com/adamtopaz/UnivAlg

[Adam Topaz]

Ignore the readme

[Adam Topaz]

And we were a bit careless about the finite tuple stuff -- it needs to be integrated better with mathlib

[Adam Topaz]

But the mathematical idea is that this lang.gen construction is essentially a monad whose algebras are exactly Lawvere theories

[Aaron Anderson]

I feel like this kinda has to merge with flypitch’s first-order-structures eventually...

[Aaron Anderson]

As most of universal algebra uses the same basic definitions as model theory, but with languages with no relations

[Adam Topaz]

Agreed

[Adam Topaz]

Does flypitch actually provide interpretations of first order theories in types?

[Aaron Anderson]

They have a few examples

[Aaron Anderson]

I’m not 100% sure what you mean, but if the answer is “yes”, some of it is in their file abel.lean

[Adam Topaz]

I guess my question is if/how they define models of a first order theory.

[Adam Topaz]

Ok I think I understand. They can define an interpretation of a language on a type, and then define the associated complete theory, so you can speak about models.

[Aaron Anderson]

They also have a notion of whether a structure realizes a particular sentence or set thereof (see lines starting around 1200 in fol.lean), but perhaps it'd be better to move most of this discussion back to the existing model theory thread.