[Merged by Bors] - feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid

[eric-wieser]

The extra _s required to make this still build are unfortunate, but hopefully someone else can work out how to remove them in a later PR.

---

Continues the work in #2848, cc @sgouezel

[semorrison]

Isn't the problem here that direct_sum itself here is still all written in terms of add_comm_group, rather than add_comm_monoid?

Perhaps we should refactor that first before attempting this change.

[semorrison]

(To be honest, I'm disinclined to do this myself because I just want to rip out everything we have on direct sums and replace it with stuff using the category theory library, so we don't have to go around writing boilerplate about how the projection maps have is_add_group_hom instances, etc. Probably I'd just be replacing it with different boilerplate, but ...)

[semorrison]

Oh, I see, I'm slow, that's in #3487. Could you explain why that PR is blocked on this one? I would have guessed it was the other way round.

[eric-wieser]

It's blocked primarily because I don't want to bite off too much in a single PR, and this only had two downstream proofs that were affected. The other PR looked far harder to resolve, and conflicts with #3473 anyway.

[semorrison]

I guess I still don't understand why #3487 is blocked on this. Can't we start generalizing that file without touching anything here?

[semorrison]

(Sorry about the slow responses on these PRs. I'll try to check back sooner.)

[eric-wieser]

Blocked is a strong word. It seemed this was easier to get past the finish line, and the PRs were likely to conflict.

[semorrison]

I'm going to mark this back as WIP. My understanding is that:

1. this change is essentially a regression: we shouldn't be making this change that introduces the need for lots of new underscores, without fixing the underlying problem.
2. You have another overlapping PR open, [Merged by Bors] - feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid #3537, which is also working on a solution.

Once you've sorted out which approach is best, could you mark that one as request-review again? (And/or close other PRs as appropriate.)

[eric-wieser]

this change is essentially a regression: we shouldn't be making this change that introduces the need for lots of new underscores, without fixing the underlying problem.

My argument is that we have a pile of code that assumes add_comm_group and should assume add_comm_monoid. The only options are:

• Fix the whole pile
• Start from the bottom of the pile, and introduce temporary ugly underscores as we move up the pile

I don't see why the second option is a problem here. Can't we do this incrementally?

(I've found myself needing this specific change again, and I don't want to have to revive the other other PRs about direct_sum which I don't care about right now)

[Vierkantor]

Generalizing to add_comm_monoid is a good idea and few more underscores doesn't hurt the readability too much IMO, so I'm in favour of this PR.

[digama0]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests