This PR/issue depends on:

• [Merged by Bors] - feat(Algebra/DirectSum): getting a map between directsums by giving the map on components #22354
  By Dependent Issues (🤖). Happy coding!

Hello @ocfnash. On behalf of the reviewer auto-assignment algorithm, I'm assigning this PR to you.

I like this PR and I'd like to get it resolved. Thank you all for the work so far!

Before we go further I think we need to settle some design decisions.

First, I have some remarks about existing definitions as follows:

• TwoSidedIdeal Two-sided ideals, very general (in particular no commutativity / unitality assumed)
• RingCon An implementation detail en route to TwoSidedIdeal
• HomogenousIdeal Homogenous left ideals, expect only useful in commutative (unital) world
• RingQuot A legacy adhoc construction, which we should phase out in favour of working with TwoSidedIdeal

Assuming I've got the above correct (ping @eric-wieser in case he has bandwidth to add some remarks) I believe two weaknesses of the current design are:

• it uses the language of relations rather than ideals
• it uses the legacy RingQuot

Bearing all of the above in mind, I have the following questions:

1. Do we really want to have a notion of a homogeneous relation, that does not necessarily come from an ideal (or at least a submodule)?
2. If the answer to 1 is "no", is there any reason why we should not work on top of TwoSidedIdeal rather than using relations and RingQuot? If so, it seems that HomogenousIdeal would provide some design inspiration, in particular using Submodule.IsHomogeneous. (In an ideal world we would not have both HomogenousIdeal and the hypothetical HomogenousTwoSidedIdeal, but this is part of a separate concern.)

This PR has been migrated to a fork-based workflow: #27307