Bundled functions: separate hierarchies?

Stream: mathlib4

[Yury G. Kudryashov]

@Anne Baanen What do you think about deleting all the *HomClasses that mix hierarchies? I mean, since we have separate FunLike instances anyway, we can use [FunLike F A B] [MonoidHomClass A B] [OrderHomClass A B] whenever we need instead of creating all the cross-insances.

[Yury G. Kudryashov]

This way we can have:

• order-related hierarchy;
• algebraic hierarchy;
• topological/metrical/smooth hierarchy;

[Yury G. Kudryashov]

#xy: some class searches in #10472 fail, probably because I make more *HomClasses available.

[Yaël Dillies]

It was not possible until the FunLike unbundling, but now that that's done it sounds reasonable to at least try

[Anne Baanen]

I agree we should try this. From my experience during the refactor I'd probably start with definitions that mix sets of variables, like splitting docs#StarAlgHomClass into the Star part and the Alg part that has an extra algebra parameter.

[Yury G. Kudryashov]

I'm going to start with algebraic and ordered hierarchies.

[Yury G. Kudryashov]

Mathlib.Algebra.Order.Hom.Monoid is used by surprisingly few files now.

[Yaël Dillies]

Is that surprising? I defined it pretty late in the history of mathlib, and by that point we already had docs#AbsoluteValue

[Jireh Loreaux]

How few is "surprisingly few"?

[Yury G. Kudryashov]

Less than 10

[Jireh Loreaux]

transitively or directly?

[Yury G. Kudryashov]

Transitively, see #10544

[Yury G. Kudryashov]

mon.pdf

[Yury G. Kudryashov]

I also merged it into #10472 to see if it helps there.

[Yury G. Kudryashov]

How should I name what's now called OrderMonoidHomClass.toOrderMonoidHom etc?

[Yaël Dillies]

Half-awake guess: OrderMonoidHom.ofClass

[Yury G. Kudryashov]

I suggest that I don't change names for now, then I change them for all bundled homs at once.