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
Rsemimodules indexed over
Create the direct sum given a family
R semimodules indexed over
Inclusion of each component into the direct sum.
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.
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