Commit 2025-03-05 02:59 6cd25d22

feat(Algebra/DirectSum): getting a map between directsums by giving the map on components (#22354) This PR defines the map obtained between DirectSums by giving the component-wise mapping. More specifically, it creates a homomorphism DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i from the component-wise map f : ∀(i : ι), α i →+ β i. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings. The linear version of this map was added already in #20265.