Components of the free module on a biproduct

The free module on a binary biproduct is the biproduct of the two free modules; that isomorphism is freeModBiprodIso, assembled from the carrier-level distributor tensorBiprodIso. Recorded here are its four components: the distributor followed by a projection of the module biproduct is the free module on the corresponding projection of the underlying biproduct, and an injection of the module biproduct followed by the inverse distributor is the free module on the corresponding injection. Since each side is a module map, the identifications are those of the carriers, and the carrier-level identifications are the defining equations of biprod.lift and biprod.desc.

The vanishing of the free module on a zero object completes the bookkeeping of the empty mixed sum.

theorem RS.freeModZeroIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] {V : D} (h : CategoryTheory.Limits.IsZero V) : CategoryTheory.Limits.IsZero (freeMod R V).X

The free module on a zero object is zero: the vanishing of a tensor product, retyped at the carrier of the free module.