Reorganizing `Mathlib.Algebra.Hom`

Stream: mathlib4

[Anne Baanen]

I don't like the current setup of the folder Mathlib.Algebra.Hom that holds definitions of morphism types for all kinds of algebraic structures. I believe the file defining a type of morphisms belongs alongside the file defining the structure this morphism works on. So I would like to reorganize these files so that e.g. Mathlib.Algebra.Hom.Ring becomes Mathlib.Algebra.Ring.Hom and Mathlib.Algebra.Hom.NonUnitalAlg becomes Mathlib.Algebra.Algebra.NonUnitalHom. Before I do so, any objections?

[Filippo A. E. Nuccio]

Seems a great idea!

[Jireh Loreaux]

Sounds good to me

[Riccardo Brasca]

I also agree.

[Eric Wieser]

Can you do the same for Algebra/Hom/Equiv?

[Yaël Dillies]

Hmm, in fact I did the reverse refactor a while ago. Not claiming it was a good idea, just letting you know.

[Anne Baanen]

Yaël Dillies said:

Hmm, in fact I did the reverse refactor a while ago. Not claiming it was a good idea, just letting you know.

That was mathlib3#12647, looks like.

[Anne Baanen]

I recall commenting on a PR a long time ago that I didn't like going down the Algebra.Hom path, but apparently that wasn't on that specific PR.

[Anne Baanen]

#8095