Zulip Chat Archive

Stream: maths

Topic: Reusing monoid, group, etc over equivalences


view this post on Zulip Eric Wieser (Jul 24 2020 at 15:55):

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

view this post on Zulip Chris Hughes (Jul 24 2020 at 16:03):

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.

view this post on Zulip Eric Wieser (Jul 24 2020 at 16:14):

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.

view this post on Zulip Chris Hughes (Jul 24 2020 at 16:25):

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.

view this post on Zulip Adam Topaz (Jul 24 2020 at 16:56):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 17:02):

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.

view this post on Zulip Adam Topaz (Jul 24 2020 at 17:03):

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.

view this post on Zulip Adam Topaz (Jul 24 2020 at 17:10):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 18:11):

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

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 19:55):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 20:06):

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.

view this post on Zulip Adam Topaz (Jul 24 2020 at 20:08):

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)

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:14):

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.

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:21):

Yes. Lawvere theories

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:22):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:23):

@Colter MacDonald

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:25):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:25):

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

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:25):

Start PRing it. :-)

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:26):

There are still some issues were working out.

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:26):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 00:12):

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.

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:13):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 00:13):

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).

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:13):

We didn't define Lawvere theories

view this post on Zulip Reid Barton (Jul 25 2020 at 00:14):

oh, so what do you do then?

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:15):

We do thing in the classical "universal algebra way"

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:15):

I.e. n-ary operations and universal axioms

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:17):

https://github.com/adamtopaz/UnivAlg

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:18):

Ignore the readme

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:19):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:21):

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

view this post on Zulip Aaron Anderson (Jul 25 2020 at 01:18):

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

view this post on Zulip Aaron Anderson (Jul 25 2020 at 01:19):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 01:20):

Agreed

view this post on Zulip Adam Topaz (Jul 25 2020 at 01:21):

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

view this post on Zulip Aaron Anderson (Jul 25 2020 at 01:22):

They have a few examples

view this post on Zulip Aaron Anderson (Jul 25 2020 at 01:22):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 01:29):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 02:28):

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.

view this post on Zulip Aaron Anderson (Jul 25 2020 at 03:51):

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.


Last updated: May 11 2021 at 16:22 UTC