feat(linear_algebra/decomposition): Define module decompositions and prove basic facts

[winston-h-zhang]

We define a new structure decomposition ι R M as the type of ι-indexed decompositions of M. We provide a correspondence between internal direct sums and decompositions. Some helpful auxiliary lemmas have been added as well.

---

Suggestions or criticisms about how I could do this better is certainly welcome!

• [x] depends on: #8274
• [x] depends on: #8475

[winston-h-zhang]

I'm confused, what is Merge branch 'master' into eric-wieser/direct_sum.is_internal.supr_eq_top doing? Is it modifying #8274 or #8246? My Github knowledge is too basic for this but I'm curious to understand how it works

[eric-wieser]

That commit is a commit that I made in #8274 (hence it showing me as the author), it was me pulling in the latest changes from bors

[eric-wieser]

I've pushed an update to this to resolve the merge conflicts and remove the obviously duplicate lemmas. There's still some less trivial duplication between the mem_supr and dfinsupp lemmas which I've added a TODO comment about.

[eric-wieser]

@acxxa, I think #9202 contains most of the interesting proofs from this PR; all that's left is the decomposition API.

Did you have a motivation for bundling factors rather than leaving it unbundled? Was there something you planned to build on top of this?

[eric-wieser]

Note that graded_algebra is now merged. I think probably to make it play well with this PR, we want to change it's definition from

class graded_algebra extends set_like.graded_monoid 𝒜 :=
(decompose' : A → ⨁ i, 𝒜 i)
(left_inv : function.left_inverse decompose' (direct_sum.submodule_coe 𝒜))
(right_inv : function.right_inverse decompose' (direct_sum.submodule_coe 𝒜))

to

-- this is essentially your `decomposition`
class graded_module :=
(decompose' : A → ⨁ i, 𝒜 i)
(left_inv : function.left_inverse decompose' (direct_sum.submodule_coe 𝒜))
(right_inv : function.right_inverse decompose' (direct_sum.submodule_coe 𝒜))

class graded_algebra extends set_like.graded_monoid 𝒜, graded_module 𝒜

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#8274~~
• ~~leanprover-community/mathlib#8475~~ By Dependent Issues (🤖). Happy coding!

[YaelDillies]

@eric-wieser, what's your opinion on this PR nowadays?