Direct sum of modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
(direct_sum.to_module.unique
).
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 M
(direct_sum.coe_linear_map
), and
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
elsewhere as direct_sum.is_internal
, but its basic consequences on submodule
s are established
in this file.
Equations
Create the direct sum given a family M
of R
modules indexed over ι
.
Equations
- direct_sum.lmk R ι M = dfinsupp.lmk
Inclusion of each component into the direct sum.
Equations
- direct_sum.lof R ι M = dfinsupp.lsingle
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.
Equations
- direct_sum.to_module R ι N φ = ⇑(dfinsupp.lsum ℕ) φ
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.
Two linear_map
s 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.
Equations
- direct_sum.lset_to_set R S T H = direct_sum.to_module R ↥S (direct_sum ↥T (λ (i : ↥T), M ↑i)) (λ (i : ↥S), direct_sum.lof R ↥T (λ (i : subtype T), M ↑i) ⟨↑i, _⟩)
Given fintype α
, linear_equiv_fun_on_fintype R
is the natural R
-linear equivalence
between ⨁ i, M i
and Π i, M i
.
Equations
- direct_sum.linear_equiv_fun_on_fintype R ι M = {to_fun := coe_fn (direct_sum.has_coe_to_fun ι (λ (i : ι), M i)), map_add' := _, map_smul' := _, inv_fun := dfinsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}
The natural linear equivalence between ⨁ _ : ι, M
and M
when unique ι
.
Equations
- direct_sum.lid R M ι = {to_fun := (direct_sum.id M ι).to_fun, map_add' := _, map_smul' := _, inv_fun := (direct_sum.id M ι).inv_fun, left_inv := _, right_inv := _}
The projection map onto one component, as a linear map.
Equations
- direct_sum.component R ι M i = dfinsupp.lapply i
Reindexing terms of a direct sum is linear.
Equations
- direct_sum.lequiv_congr_left R h = {to_fun := (direct_sum.equiv_congr_left h).to_fun, map_add' := _, map_smul' := _, inv_fun := (direct_sum.equiv_congr_left h).inv_fun, left_inv := _, right_inv := _}
curry
as a linear map.
Equations
- direct_sum.sigma_lcurry R = {to_fun := direct_sum.sigma_curry.to_fun, map_add' := _, map_smul' := _}
uncurry
as a linear map.
Equations
- direct_sum.sigma_luncurry R = {to_fun := direct_sum.sigma_uncurry.to_fun, map_add' := _, map_smul' := _}
curry_equiv
as a linear equiv.
Equations
- direct_sum.sigma_lcurry_equiv R = {to_fun := direct_sum.sigma_curry_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := direct_sum.sigma_curry_equiv.inv_fun, left_inv := _, right_inv := _}
Linear isomorphism obtained by separating the term of index none
of a direct sum over
option ι
.
Equations
- direct_sum.lequiv_prod_direct_sum R = {to_fun := direct_sum.add_equiv_prod_direct_sum.to_fun, map_add' := _, map_smul' := _, inv_fun := direct_sum.add_equiv_prod_direct_sum.inv_fun, left_inv := _, right_inv := _}
The canonical embedding from ⨁ i, A i
to M
where A
is a collection of submodule R M
indexed by ι
. This is direct_sum.coe_add_monoid_hom
as a linear_map
.
Equations
- direct_sum.coe_linear_map A = direct_sum.to_module R ι M (λ (i : ι), (A i).subtype)
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 M
.
Equations
- h.collected_basis v = {repr := ((linear_equiv.of_bijective (direct_sum.coe_linear_map A) h).symm.trans (dfinsupp.map_range.linear_equiv (λ (i : ι), (v i).repr))).trans (sigma_finsupp_lequiv_dfinsupp R).symm}
When indexed by only two distinct elements, direct_sum.is_internal
implies
the two submodules are complementary. Over a ring R
, this is true as an iff, as
direct_sum.is_internal_iff_is_compl
.
Note that this is not generally true for [semiring R]
; see
complete_lattice.independent.dfinsupp_lsum_injective
for details.
iff
version of direct_sum.is_internal_submodule_of_independent_of_supr_eq_top
,
direct_sum.is_internal.independent
, and direct_sum.is_internal.supr_eq_top
.
If a collection of submodules has just two indices, i
and j
, then
direct_sum.is_internal
is equivalent to is_compl
.
Now copy the lemmas for subgroup and submonoids.