Zulip Chat Archive

Stream: maths

Topic: is_mul_hom and is_group_hom


view this post on Zulip Yury G. Kudryashov (Jun 30 2019 at 23:03):

Hi, is there any reason why is_group_hom does not extend is_mul_hom?
BTW, they use slightly different map_mul types (explicit vs implicit arguments).

view this post on Zulip Johan Commelin (Jul 01 2019 at 01:22):

@Yury G. Kudryashov The reason is history. is_mul_hom was added only very recently. And there was no big refactor, as maybe there should have been.

view this post on Zulip Yury G. Kudryashov (Jul 01 2019 at 07:25):

@Johan Commelin Thank you for the explanation.

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 17:16):

@Johan Commelin Probably I'll try to merge is_mul_hom with is_group_hom (I mean, make is_group_hom extend is_mul_hom). Which version of map_mul do you prefer: ∀ x y, ... or ∀ {x y}, ...?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:17):

∀ x y, ...

view this post on Zulip Chris Hughes (Jul 05 2019 at 17:17):

Personally I don't think they should be different things.

view this post on Zulip Chris Hughes (Jul 05 2019 at 17:18):

It just means you have to duplicate a lot of proofs.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:18):

It seems similar to vector_space vs module

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:19):

the definition isn't different, just the constraints

view this post on Zulip Chris Hughes (Jul 05 2019 at 17:19):

But why add constraints?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:19):

I'm not saying what is better, and actually I forget what we did for vector_space

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 17:24):

@Chris Hughes I guess, it improves readability. If you see [group α] [group β] (f : α → β) (h : is_mul_hom f), you have to know that any is_mul_hom plays nice with 1 and inv to understand the text. However, (h : is_group_hom f) makes is much easier to read.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:25):

it could be a notation

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:26):

I am not a big fan of when "readability" makes my proofs harder

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:26):

or I have to do a bunch of boilerplate to support what is effectively notation

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 17:29):

Given instances is_monoid_hom.to_is_mul_hom and is_mul_hom.to_is_monoid_hom [group β], will Lean enter a loop?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:30):

yes

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 17:30):

Then we have a reason for is_group_hom to exist.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:31):

fair point

view this post on Zulip Johan Commelin (Jul 05 2019 at 17:57):

Right... the fact that is_group_hom is just an is_mul_hom is a coincidence.

view this post on Zulip Johan Commelin (Jul 05 2019 at 17:57):

But in case of vector_space I can't think of such a reason. I would be happy to see it go away.

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 18:48):

@Johan Commelin , could you please have another look at #1164? It's a step towards making is_group_hom extend is_mul_hom.

view this post on Zulip Johan Commelin (Jul 05 2019 at 18:53):

Thanks for reminding me @Yury G. Kudryashov
It's on the merge queue now.

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 18:54):

Thanks!

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 17:47):

Hi, I'm making is_semiring_hom and is_ring_hom extend is_add_monoid_hom etc.
I have a few choices:
1. Add map_mul and friends to the root namespace as @Johan Commelin suggested here. This way map_add conflicts with multiset.map_add (so I have to explicitly add _root_.map_add or multiset.map_add) and map_inv conflicts with its version for fields.
2. Use is_mul_hom.map_mul, is_monoid_hom.map_one, is_group_hom.map_inv. This way users have to know which class defines map_mul etc.
3. Use export (is_mul_hom) map_mul etc. This way it should be possible to use is_ring_hom.map_add etc unless you want to provide [is_ring_hom f] argument explicitly; then you find out that you need [is_add_hom f], not [is_ring_hom f].
4. Manually export substituting arguments. I'd prefer to have a tactic for this but I never tried to write a Lean tactic and failed to find any docs on the meta-specific API (e.g., implemented monads).

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:27):

@Johan Commelin Which approach would you prefer?

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:40):

The conflicts in (1) are unfortunate.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:40):

Otherwise I would have very much preferred that one.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:41):

But I would be happy to write is_field_hom.map_inv to avoid the conflict.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:41):

So we could make is_field_hom.map_inv protected.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:42):

(Btw, maybe that should be is_division_ring_hom?? But I don't know if that one exists :smiley:)

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:43):

I don't really like (2). It's quite unfriendly to users and to refactors.

view this post on Zulip Chris Hughes (Jul 13 2019 at 19:44):

There is a plan to bundle all of them at some point by the way. Someone just has to get around to doing it.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:47):

@Yury G. Kudryashov If we choose (1), this probably means that all the simp-lemmas multiset.map_add and foobar.map_add, etc..., should be made protected. I don't think that's a bad idea anyway.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:48):

@Chris Hughes What exactly do you want to have? Could you post some code, e.g, for the simplest case of semigroups?

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:48):

@Johan Commelin I'll try (1)

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:50):

I would just want something like

-- root namespace
lemma map_add {X Y} (f : X  Y) [is_add_hom f] (x y) : f (x + y) = f x + f y := is_add_hom.map_add f x y

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:51):

@Johan Commelin Yes, this is what I have now (with α and β instead of X and Y)

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:51):

And similar for map_mul, map_zero, map_one, map_sub, map_neg, map_inv, map_div, and any others that I forgot...

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:51):

My question to @Chris Hughes is about bundling. What should be bundled and how should it look like.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:52):

Ok, I understand.

view this post on Zulip Johan Commelin (Jul 13 2019 at 19:52):

Need to go now. See you later!

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 19:52):

@Johan Commelin Now I have just (in root namespace) export is_mul_hom (map_mul)

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 20:10):

Module homomorphisms are bundled and this worked, so the plan is to bundle group homs, ring homs etc, but people seem to be of the opinion that it all needs to be done in one go which makes it a daunting task

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:19):

I see that is_linear_map is used in at least 7 files.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:20):

And linear_map is used in at least 21 files.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:29):

How should people use these bundled versions for specific maps? E.g., now we have instance : is_semiring_hom (coe : nat -> α). What should be the bundled version of this?

view this post on Zulip Mario Carneiro (Jul 13 2019 at 20:30):

of_nat : semiring_hom nat A, of_nat_apply : of_nat a = \u a

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:40):

So, we need add_monoid.of_nat and semiring.of_nat.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:41):

Another question: I have a theorem about add_group_hom. How should I apply it to a ring_hom? Explicit conversion? Some implicit coercion?

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 20:47):

If this is going to be rewritten, I think that I'll switch from making is_ring_hom extend is_monoid_hom and is_add_group_hom to something more useful.

view this post on Zulip Johan Commelin (Jul 14 2019 at 04:36):

Another question: I have a theorem about add_group_hom. How should I apply it to a ring_hom? Explicit conversion? Some implicit coercion?

This is a hard question. If I recall correctly, experiments so far have not really been satisfactory.

view this post on Zulip Johan Commelin (Jul 14 2019 at 04:37):

I think that your "export stuff in the root namespace" PR would hopefully not be too much work. So you could still just do that. I'm not sure if bundling of morphisms will happen in the near future...

view this post on Zulip Yury G. Kudryashov (Jul 15 2019 at 09:32):

@Johan Commelin It takes more time&effort than I expected. There are a few reasons:
1. Many namespaces have map_mul, map_add etc. I have to make all of them protected, then figure out where I need to add namespace.
2. Sometimes class instance resolution fails to find is_add_monoid_hom f a few lines after instance : is_ring_hom f, and I don't know how to fix this but supplying the conversion explicitly (and this looks ugly).
So, I'm going to do the following:
1. Push current state to a branch (compile fails).
2. Submit PRs on various small fixes I made while trying to do this move.
3. Try to make is_ring_hom extend is_add_group_hom by "manually exporting" map_add etc into is_ring_hom namespace.
3b. Try to turn the "manual export" in (3) into a tactic, if I find some docs on writing tactics.

view this post on Zulip Johan Commelin (Jul 15 2019 at 09:39):

Hmmm, I'm sorry that it is so painful.

view this post on Zulip Johan Commelin (Jul 15 2019 at 09:39):

@Yury G. Kudryashov Concerning writing tactics. Are you aware of https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md?

view this post on Zulip Yury G. Kudryashov (Jul 15 2019 at 10:01):

Thanks, I somehow missed it

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 10:10):

There will be general "mathlib-style" principles about how to do this sort of stuff and it would probably best to hear from a maintainer or expert who understands e.g. the details of typeclass inference and how it works in mathlib, before doing too much more on this.

view this post on Zulip Yury G. Kudryashov (Jul 15 2019 at 13:26):

@Kevin Buzzard Then I'll just do (1) and (2)

view this post on Zulip Chris Hughes (Jul 15 2019 at 13:29):

I did make a start on bundling homs https://github.com/leanprover-community/mathlib/tree/bundled-homs. My plan was to make group hom be the same as monoid hom (reducible def or something), on the grounds that nobody really cares about semigroups, so this is more useful than it extending mul hom (the downside is one unnecessary axiom, but this isn't much of a downside, and you can just write a new constructor). I also wanted to get rid of is_field_hom.

view this post on Zulip Yury G. Kudryashov (Jul 15 2019 at 18:46):

@Chris Hughes I'll have a look at this, but I want to formalize something non-trivial before coming back to cleanup.


Last updated: May 11 2021 at 15:12 UTC