# Zulip Chat Archive

## Stream: general

### Topic: Bundled Group morphisms

#### Floris van Doorn (Apr 13 2020 at 18:40):

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 (Apr 13 2020 at 18:42):

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

#### Kevin Buzzard (Apr 13 2020 at 18:47):

Note also #2140

#### Floris van Doorn (Apr 13 2020 at 18:58):

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

#### Yury G. Kudryashov (Apr 13 2020 at 19:02):

I started with `is_ring_hom`

and `is_semiring_hom`

#### Yury G. Kudryashov (Apr 13 2020 at 19:05):

Right now the main users of `is_ring_hom`

are `polynomial`

s and `mv_polynomial`

s. 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 (Apr 13 2020 at 19:06):

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 (Apr 13 2020 at 19:08):

I guess `polynomial`

s might use theorems about `is_group_hom`

s through `is_ring_hom`

#### Yury G. Kudryashov (Apr 13 2020 at 19:09):

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

#### Yury G. Kudryashov (Apr 13 2020 at 19:09):

I also have theorems like `nat.eq_cast`

rewritten using bundled homs, not PR-ready yet.

#### Floris van Doorn (Apr 13 2020 at 19:11):

Ok, sounds good

#### Yury G. Kudryashov (Apr 13 2020 at 19:45):

BTW, we have an `is_mul_hom`

which is not an `is_monoid_hom`

. It's called `nhds`

.

#### Yury G. Kudryashov (Apr 13 2020 at 19:46):

So `is_mul_hom`

lemmas in `pointwise`

can't be migrated to `→*`

without loosing this application.

#### Kevin Buzzard (Apr 13 2020 at 19:47):

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

#### Yury G. Kudryashov (Apr 13 2020 at 19:49):

$ 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 (Apr 13 2020 at 19:50):

I recently migrated `ring_theory/algebra`

to bundled homs.

#### Yury G. Kudryashov (Apr 13 2020 at 19:51):

Most of this can easily go away once `polynomial`

s use bundled homs.

#### Yury G. Kudryashov (Apr 13 2020 at 19:52):

I don't want to touch `ring_theory/localization`

because @Amelia Livingston is going to (almost fully) rewrite it.

Last updated: May 13 2021 at 06:15 UTC