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.
linear_maps out of a direct sum are equal if they agree on the generators.
The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.
linear_equiv_fun_on_fintype R is the natural
⨁ i, M i and
Π i, M i.
The natural linear equivalence between
⨁ _ : ι, M and
For the alternate statement in terms of independence and spanning, see
If a direct sum of submodules is internal then the submodules span the module.
If a direct sum of submodules is internal then the submodules are independent.
Note that this is not generally true for
[semiring R]; see
complete_lattice.independent.dfinsupp_lsum_injective for details.