## Stream: maths

### Topic: is_mul_hom and is_group_hom

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

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

#### Yury G. Kudryashov (Jul 01 2019 at 07:25):

@Johan Commelin Thank you for the explanation.

#### 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}, ...?

#### Mario Carneiro (Jul 05 2019 at 17:17):

∀ x y, ...

#### Chris Hughes (Jul 05 2019 at 17:17):

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

#### Chris Hughes (Jul 05 2019 at 17:18):

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

#### Mario Carneiro (Jul 05 2019 at 17:18):

It seems similar to vector_space vs module

#### Mario Carneiro (Jul 05 2019 at 17:19):

the definition isn't different, just the constraints

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

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

#### Mario Carneiro (Jul 05 2019 at 17:25):

it could be a notation

#### Mario Carneiro (Jul 05 2019 at 17:26):

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

#### Mario Carneiro (Jul 05 2019 at 17:26):

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

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

yes

#### Yury G. Kudryashov (Jul 05 2019 at 17:30):

Then we have a reason for is_group_hom to exist.

fair point

#### Johan Commelin (Jul 05 2019 at 17:57):

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

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

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

#### Johan Commelin (Jul 05 2019 at 18:53):

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

Thanks!

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

#### Yury G. Kudryashov (Jul 13 2019 at 19:27):

@Johan Commelin Which approach would you prefer?

#### Johan Commelin (Jul 13 2019 at 19:40):

The conflicts in (1) are unfortunate.

#### Johan Commelin (Jul 13 2019 at 19:40):

Otherwise I would have very much preferred that one.

#### Johan Commelin (Jul 13 2019 at 19:41):

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

#### Johan Commelin (Jul 13 2019 at 19:41):

So we could make is_field_hom.map_inv protected.

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

#### Johan Commelin (Jul 13 2019 at 19:43):

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

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

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

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

#### Yury G. Kudryashov (Jul 13 2019 at 19:48):

@Johan Commelin I'll try (1)

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


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

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

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

#### Johan Commelin (Jul 13 2019 at 19:52):

Ok, I understand.

#### Johan Commelin (Jul 13 2019 at 19:52):

Need to go now. See you later!

#### Yury G. Kudryashov (Jul 13 2019 at 19:52):

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

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

#### Yury G. Kudryashov (Jul 13 2019 at 20:19):

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

#### Yury G. Kudryashov (Jul 13 2019 at 20:20):

And linear_map is used in at least 21 files.

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

#### Mario Carneiro (Jul 13 2019 at 20:30):

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

#### Yury G. Kudryashov (Jul 13 2019 at 20:40):

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

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

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

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

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

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

#### Johan Commelin (Jul 15 2019 at 09:39):

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

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

#### Yury G. Kudryashov (Jul 15 2019 at 10:01):

Thanks, I somehow missed it

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

#### Yury G. Kudryashov (Jul 15 2019 at 13:26):

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

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

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