Commit 2022-06-16 19:20 ae10dced

feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626) This is a constructive version of direct_sum.is_internal, and generalizes the existing graded_algebra. The main user-facing changes are:

• graded_algebra.decompose is now spelt direct_sum.decompose_alg_hom
• The simp normal form of decomposition is now direct_sum.decompose.
• graded_algebra.support 𝒜 x is now spelt (decompose 𝒜 x).support
• left_inv and right_inv has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left graded_algebra.proj alone for a future refactor.