Bundled Group morphisms

Stream: general

[Floris van Doorn]

I noticed that is_group_hom and variants are deprecated, but still used all over group_theory.
I'm happy to try to make a PR updating these to monoid_hom/→*.
Is someone already working on this (or did in the past)?

[Johan Commelin]

See recent PRs by @Yury G. Kudryashov (who is now very busy grading exams :pen: :paper:)

[Kevin Buzzard]

Note also #2140

[Floris van Doorn]

Thanks, those are indeed all related, but I don't think they interfere much with this project.

[Yury G. Kudryashov]

I started with is_ring_hom and is_semiring_hom

[Yury G. Kudryashov]

Right now the main users of is_ring_hom are polynomials and mv_polynomials. I have a rewrite of eval that uses bundled homs but I won't be able to make it PR-ready until I'm done with grading.

[Floris van Doorn]

Do you think this will interfere a lot with factoring out is_group_hom? My guess is that there shouldn't be that much interference.

[Yury G. Kudryashov]

I guess polynomials might use theorems about is_group_homs through is_ring_hom

[Yury G. Kudryashov]

So I'd suggest to wait for about a week till I PR my changes.

[Yury G. Kudryashov]

I also have theorems like nat.eq_cast rewritten using bundled homs, not PR-ready yet.

[Floris van Doorn]

Ok, sounds good

[Yury G. Kudryashov]

BTW, we have an is_mul_hom which is not an is_monoid_hom. It's called nhds.

[Yury G. Kudryashov]

So is_mul_hom lemmas in pointwise can't be migrated to →* without loosing this application.

[Kevin Buzzard]

I think a lot of the ideal and algebra stuff uses is_ring_hom?

[Yury G. Kudryashov]

$ git grep -l 'is_\(semi_\)\?ring_hom'
src/algebra/direct_limit.lean
src/algebra/field.lean
src/algebra/field_power.lean
src/algebra/pi_instances.lean
src/algebra/punit_instances.lean
src/algebra/ring.lean
src/data/complex/basic.lean
src/data/equiv/ring.lean
src/data/mv_polynomial.lean
src/data/padics/padic_integers.lean
src/data/polynomial.lean
src/data/zsqrtd/gaussian_int.lean
src/field_theory/minimal_polynomial.lean
src/field_theory/mv_polynomial.lean
src/field_theory/subfield.lean
src/ring_theory/adjoin_root.lean
src/ring_theory/free_comm_ring.lean
src/ring_theory/free_ring.lean
src/ring_theory/localization.lean
src/ring_theory/maps.lean
src/topology/algebra/module.lean
src/topology/algebra/uniform_ring.lean

[Yury G. Kudryashov]

I recently migrated ring_theory/algebra to bundled homs.

[Yury G. Kudryashov]

Most of this can easily go away once polynomials use bundled homs.

[Yury G. Kudryashov]

I don't want to touch ring_theory/localization because @Amelia Livingston is going to (almost fully) rewrite it.