Direct sum of modules #
The first part of the file provides constructors for direct sums of modules. It provides a
construction of the direct sum using the universal property and proves its uniqueness
The second part of the file covers the special case of direct sums of submodules of a fixed module
M. There is a canonical linear map from this direct sum to
the construction is of particular importance when this linear map is an equivalence; that is, when
the submodules provide an internal decomposition of
M. The property is defined more generally
DirectSum.IsInternal, but its basic consequences on
Submodules are established
in this file.
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.
LinearMaps out of a direct sum are equal if they agree on the generators.
See note [partially-applied ext lemmas].
The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.
curry as a linear map.
uncurry as a linear map.
curryEquiv as a linear equiv.
Linear isomorphism obtained by separating the term of index
none of a direct sum over
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.
Given an internal direct sum decomposition of a module
M, and a basis for each of the
components of the direct sum, the disjoint union of these bases is a basis for
Note that this is not generally true for
[Semiring R]; see
CompleteLattice.Independent.dfinsupp_lsum_injective for details.
Now copy the lemmas for subgroup and submonoids.