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

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 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 (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 polynomials might use theorems about is_group_homs 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.

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/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/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 polynomials 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