The realization of a biproduct

Morphisms into a finite biproduct are families of morphisms into the summands, ℂ-linearly. With the distribution of a tensor over a biproduct this computes ρ on a mixed sum.

noncomputable def RS.homBiproductEquiv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] {J : Type} [Finite J] (P : D) (f : J → D) : (P ⟶ ⨁ f) ≃ₗ[ℂ] (j : J) → P ⟶ f j

Morphisms into a biproduct are families of morphisms, as ℂ-modules.

Equations

• One or more equations did not get rendered due to their size.