Zulip Chat Archive

Stream: general

Topic: minimalist assumptions

Johan Commelin (May 08 2020 at 07:13):

We have probably discussed this before, but I'm not sure if there is a consensus. What are the pros and cons of changing the definition of monoid_hom to only assume has_one M, has_mul M, has_one N, and has_mul N (in other words, a lawless monoid), instead of assuming lawful monoids?

Would it even be feasible to refactor the library to use such a definition? Or are the headaches simply to big to bother?

Yury G. Kudryashov (May 08 2020 at 07:17):

Lean won't be able to fine [monoid M] [monoid N] by unification.
This will break concrete categories.

Johan Commelin (May 08 2020 at 07:17):

But Lean can find has_one and has_mul by unification, right?

Johan Commelin (May 08 2020 at 07:18):

(2) is a serious problem

Yury G. Kudryashov (May 08 2020 at 07:18):

Probably we can adjust concrete categories but now we just label monoid_hom as a bundled hom.

Yury G. Kudryashov (May 08 2020 at 07:21):

instance bundled_hom : bundled_hom @monoid_hom :=
⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩

Yury G. Kudryashov (May 08 2020 at 07:23):

I don't know whether this will work well with λ M N mM mN, @monoid_hom M N mM.to_has_one ...

Yury G. Kudryashov (May 08 2020 at 07:23):

You can try

Johan Commelin (May 08 2020 at 07:23):

See lawless-homs for my first attempt at this. I'm running into more problems than I expected.

Yury G. Kudryashov (May 08 2020 at 07:24):

I wanted this (UPD: in free_monoid_product.normalized) to define a monoid_hom before I can define a monoid but decided not to try.

Johan Commelin (May 08 2020 at 07:24):

You get multiplicative nat at some point, and it infers the wrong has_one and has_mul. As in... they are correct, but it expects a different path.

Johan Commelin (May 08 2020 at 07:24):

Yury G. Kudryashov said:

I wanted this to define a monoid_hom before I can define a monoid but decided not to try.

Same here.

Last updated: Dec 20 2023 at 11:08 UTC