Zulip Chat Archive

Stream: general

Topic: Bundled Group morphisms


view this post on Zulip 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)?

view this post on Zulip Johan Commelin (Apr 13 2020 at 18:42):

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

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 18:47):

Note also #2140

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:02):

I started with is_ring_hom and is_semiring_hom

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:08):

I guess polynomials might use theorems about is_group_homs through is_ring_hom

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:09):

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

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Apr 13 2020 at 19:11):

Ok, sounds good

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 19:47):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:50):

I recently migrated ring_theory/algebra to bundled homs.

view this post on Zulip Yury G. Kudryashov (Apr 13 2020 at 19:51):

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

view this post on Zulip 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