bundling morphisms about mathlib HOT 8 CLOSED

The reason this came to my attention is that the current version of card_nth_roots in src/data/polynomial.lean takes 12 seconds to elaborate, and @ChrisHughes24 suggested that it the unbundled is_ring_hom was perhaps to blame.

from mathlib.

I like this idea. Algebra-morphisms are already bundled, and have no unbundled analogue:
https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/algebra.lean#L147
I have used algebra morphisms in formalabstracts already (also for some proofs), and they seem to work nicely.

My main concern is that of @ChrisHughes24:

My main concern with this is that we end up having to do type class inference by hand, if we want a field hom to be a group hom or whatever.

But thinking more about it, I think it will be manageable. Given f : field_hom F F' then writing f.to_group_hom doesn't seem too bad. Also, you would have to write expressions like f' ∘ᶠ f for composition of field homomorphisms (note: unicode has more of the Latin alphabet in superscript than in subscript - there is no subscript f), but that should be fine.

As another case, the Lean 2 HoTT library used bundled morphisms in a significant algebra library, and that seemed to work well: https://github.com/cmu-phil/Spectral/tree/master/algebra

from mathlib.

How about has_comp.comp? We can pick some notation.... unfortunately \circ is locked away. And then all bundled homs can share the same notation.
I don't really like the f.to_group_hom though... Maybe we can use coercions?

from mathlib.

Let me mention related PRs (all merged):

• (additive) monoids and groups : #1271
• (semi)rings : #1305
• concrete categories (Mon, Group etc): #1380
• mul_equiv, add_equiv: #1287
• ring_equiv: #1482

Clearly, we have a TODO “migrate all code to the new API”. What else?

from mathlib.

For reference the code is no longer in the file the top comment says, and is at:

from mathlib.

OK so the transition to bundled morphisms is almost complete. Unbundled morphisms still exist, in a deprecated directory. In src and not in src/deprecated we only have the following deprecated imports:

src/control/fold.lean:import deprecated.group
src/group_theory/free_abelian_group.lean:import deprecated.group -- someone who understands `seq` can remove this
src/ring_theory/free_comm_ring.lean:import deprecated.ring
src/topology/algebra/uniform_group.lean:import deprecated.group

The hard-core algebra and topology stuff is, I think, pretty near the outskirts of mathlib in terms of imports, so hopefully it will be possible to remove these imports without too much disruption.

from mathlib.

For the record: Kevin is talking about #8178 which has now been merged into master.

from mathlib.

There's an alternative approach to unbundled bundled maps in this Zulip thread

from mathlib.