Direct sum of modules over commutative rings, indexed by a discrete type. #
This file provides constructors for finite direct sums of modules. It provides a construction of the direct sum using the universal property and proves its uniqueness.
Implementation notes #
All of this file assumes that
Ris a commutative ring,
ιis a discrete type,
Sis a finite set in
Mis a family of
Rmodules indexed over
Create the direct sum given a family
R modules indexed over
Scalar multiplication commutes with direct sums.
Scalar multiplication commutes with the inclusion of each component into the direct sum.
The linear map constructed using the universal property of the coproduct.
Coproducts in the categories of modules and additive monoids commute with the forgetful functor from modules to additive monoids.
The map constructed using the universal property gives back the original maps when restricted to each component.
Every linear map from a direct sum agrees with the one obtained by applying the universal property to each of its components.
The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.
The natural linear equivalence between
⨁ _ : ι, M and