# Zulip Chat Archive

## Stream: maths

### Topic: Reusing monoid, group, etc over equivalences

#### 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

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

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

#### 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`

.

#### Adam Topaz (Jul 24 2020 at 16:56):

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

#### 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 `mul`

such that `one`

and `mul`

induce a monoid structure.

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

#### 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
```

#### 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

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

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

#### Adam Topaz (Jul 24 2020 at 20:08):

But I understand what you're saying. The `rel`

from 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 (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.

#### Adam Topaz (Jul 24 2020 at 23:21):

Yes. Lawvere theories

#### 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

#### Adam Topaz (Jul 24 2020 at 23:23):

@Colter MacDonald

#### 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? :-)

#### Adam Topaz (Jul 24 2020 at 23:25):

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

#### Scott Morrison (Jul 24 2020 at 23:25):

Start PRing it. :-)

#### Adam Topaz (Jul 24 2020 at 23:26):

There are still some issues were working out.

#### Scott Morrison (Jul 24 2020 at 23:26):

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

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

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

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

#### Adam Topaz (Jul 25 2020 at 00:13):

We didn't define Lawvere theories

#### Reid Barton (Jul 25 2020 at 00:14):

oh, so what do you do then?

#### Adam Topaz (Jul 25 2020 at 00:15):

We do thing in the classical "universal algebra way"

#### Adam Topaz (Jul 25 2020 at 00:15):

I.e. n-ary operations and universal axioms

#### Adam Topaz (Jul 25 2020 at 00:17):

https://github.com/adamtopaz/UnivAlg

#### Adam Topaz (Jul 25 2020 at 00:18):

Ignore the readme

#### 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

#### 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

#### Aaron Anderson (Jul 25 2020 at 01:18):

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

#### 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

#### Adam Topaz (Jul 25 2020 at 01:20):

Agreed

#### Adam Topaz (Jul 25 2020 at 01:21):

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

#### Aaron Anderson (Jul 25 2020 at 01:22):

They have a few examples

#### 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`

#### Adam Topaz (Jul 25 2020 at 01:29):

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

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

#### 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