The free modules of a finite biproduct as retracts

A finite biproduct in the ambient category presents each of its summands as a retract, and taking free modules preserves both the retraction identities and the totality of the projectors. This is how a mixed sum of copies of the unit and the odd line is fed to an additivity argument without ever forming a biproduct in the category of module objects.

theorem RS.freeModMap_biproduct_total {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Limits.HasFiniteBiproducts D] {ι : Type} [Fintype ι] (f : ι → D) : ∑ i : ι, CategoryTheory.CategoryStruct.comp (freeModMap A (CategoryTheory.Limits.biproduct.π f i)).hom (freeModMap A (CategoryTheory.Limits.biproduct.ι f i)).hom = CategoryTheory.CategoryStruct.id (freeMod A (⨁ f)).X

The free-module retracts of a finite biproduct are total.