is_mul_hom and is_group_hom

Stream: maths

[Yury G. Kudryashov]

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]

@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]

@Johan Commelin Thank you for the explanation.

[Yury G. Kudryashov]

@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]

∀ x y, ...

[Chris Hughes]

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

[Chris Hughes]

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

[Mario Carneiro]

It seems similar to vector_space vs module

[Mario Carneiro]

the definition isn't different, just the constraints

[Chris Hughes]

But why add constraints?

[Mario Carneiro]

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

[Yury G. Kudryashov]

@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]

it could be a notation

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

yes

[Yury G. Kudryashov]

Then we have a reason for is_group_hom to exist.

[Mario Carneiro]

fair point

[Johan Commelin]

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

[Johan Commelin]

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]

@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]

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

[Yury G. Kudryashov]

Thanks!

[Yury G. Kudryashov]

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]

@Johan Commelin Which approach would you prefer?

[Johan Commelin]

The conflicts in (1) are unfortunate.

[Johan Commelin]

Otherwise I would have very much preferred that one.

[Johan Commelin]

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

[Johan Commelin]

So we could make is_field_hom.map_inv protected.

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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]

@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]

@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]

@Johan Commelin I'll try (1)

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Ok, I understand.

[Johan Commelin]

Need to go now. See you later!

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

And linear_map is used in at least 21 files.

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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]

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]

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]

@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]

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

[Johan Commelin]

@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]

Thanks, I somehow missed it

[Kevin Buzzard]

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]

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

[Chris Hughes]

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]

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