# mathlib3documentation

algebra.direct_sum.module

# 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 submodules are established in this file.

@[protected, instance]
def direct_sum.module {R : Type u} [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] :
(λ (i : ι), M i))
Equations
@[protected, instance]
def direct_sum.smul_comm_class {R : Type u} [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {S : Type u_1} [semiring S] [Π (i : ι), (M i)] [ (i : ι), (M i)] :
(λ (i : ι), M i))
@[protected, instance]
def direct_sum.is_scalar_tower {R : Type u} [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {S : Type u_1} [semiring S] [ S] [Π (i : ι), (M i)] [ (i : ι), (M i)] :
(λ (i : ι), M i))
@[protected, instance]
def direct_sum.is_central_scalar {R : Type u} [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [Π (i : ι), (M i)] [ (i : ι), (M i)] :
(λ (i : ι), M i))
theorem direct_sum.smul_apply {R : Type u} [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (b : R) (v : (λ (i : ι), M i)) (i : ι) :
(b v) i = b v i
def direct_sum.lmk (R : Type u) [semiring R] (ι : Type v) [dec_ι : decidable_eq ι] (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (s : finset ι) :
(Π (i : s), M i.val) →ₗ[R] (λ (i : ι), M i)

Create the direct sum given a family M of R modules indexed over ι.

Equations
def direct_sum.lof (R : Type u) [semiring R] (ι : Type v) [dec_ι : decidable_eq ι] (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) :
M i →ₗ[R] (λ (i : ι), M i)

Inclusion of each component into the direct sum.

Equations
theorem direct_sum.lof_eq_of (R : Type u) [semiring R] (ι : Type v) [dec_ι : decidable_eq ι] (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) (b : M i) :
ι M i) b = i) b
theorem direct_sum.single_eq_lof (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) (b : M i) :
= ι M i) b
theorem direct_sum.mk_smul (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (s : finset ι) (c : R) (x : Π (i : s), M i.val) :
s) (c x) = c s) x

Scalar multiplication commutes with direct sums.

theorem direct_sum.of_smul (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) (c : R) (x : M i) :
i) (c x) = c i) x

Scalar multiplication commutes with the inclusion of each component into the direct sum.

theorem direct_sum.support_smul {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [Π (i : ι) (x : M i), decidable (x 0)] (c : R) (v : (λ (i : ι), M i)) :
def direct_sum.to_module (R : Type u) [semiring R] (ι : Type v) [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (N : Type u₁) [ N] (φ : Π (i : ι), M i →ₗ[R] N) :
(λ (i : ι), M i) →ₗ[R] N

The linear map constructed using the universal property of the coproduct.

Equations
• N φ = φ
theorem direct_sum.coe_to_module_eq_coe_to_add_monoid (R : Type u) [semiring R] (ι : Type v) [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (N : Type u₁) [ N] (φ : Π (i : ι), M i →ₗ[R] N) :

Coproducts in the categories of modules and additive monoids commute with the forgetful functor from modules to additive monoids.

@[simp]
theorem direct_sum.to_module_lof (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {N : Type u₁} [ N] {φ : Π (i : ι), M i →ₗ[R] N} (i : ι) (x : M i) :
N φ) ( ι M i) x) = (φ i) x

The map constructed using the universal property gives back the original maps when restricted to each component.

theorem direct_sum.to_module.unique (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {N : Type u₁} [ N] (ψ : (λ (i : ι), M i) →ₗ[R] N) (f : (λ (i : ι), M i)) :
ψ f = N (λ (i : ι), ψ.comp ι M i))) f

Every linear map from a direct sum agrees with the one obtained by applying the universal property to each of its components.

@[ext]
theorem direct_sum.linear_map_ext (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {N : Type u₁} [ N] ⦃ψ ψ' : (λ (i : ι), M i) →ₗ[R] N⦄ (H : (i : ι), ψ.comp ι M i) = ψ'.comp ι M i)) :
ψ = ψ'

Two linear_maps out of a direct sum are equal if they agree on the generators.

def direct_sum.lset_to_set (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (S T : set ι) (H : S T) :
(λ (i : S), M i) →ₗ[R] (λ (i : T), M i)

The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.

Equations
@[simp]
theorem direct_sum.linear_equiv_fun_on_fintype_apply (R : Type u) [semiring R] (ι : Type v) (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [fintype ι] (x : (λ (i : ι), M i)) (i : ι) :
i = x i
def direct_sum.linear_equiv_fun_on_fintype (R : Type u) [semiring R] (ι : Type v) (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [fintype ι] :
(λ (i : ι), M i) ≃ₗ[R] Π (i : ι), M i

Given fintype α, linear_equiv_fun_on_fintype R is the natural R-linear equivalence between ⨁ i, M i and Π i, M i.

Equations
@[simp]
theorem direct_sum.linear_equiv_fun_on_fintype_lof (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [fintype ι] [decidable_eq ι] (i : ι) (m : M i) :
( ι M i) m) = m
@[simp]
theorem direct_sum.linear_equiv_fun_on_fintype_symm_single (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [fintype ι] [decidable_eq ι] (i : ι) (m : M i) :
.symm) m) = ι M i) m
@[simp]
theorem direct_sum.linear_equiv_fun_on_fintype_symm_coe (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [fintype ι] (f : (λ (i : ι), M i)) :
@[protected]
def direct_sum.lid (R : Type u) [semiring R] (M : Type v) (ι : Type u_1 := punit) [ M] [unique ι] :
(λ (_x : ι), M) ≃ₗ[R] M

The natural linear equivalence between ⨁ _ : ι, M and M when unique ι.

Equations
def direct_sum.component (R : Type u) [semiring R] (ι : Type v) (M : ι Type w) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) :
(λ (i : ι), M i) →ₗ[R] M i

The projection map onto one component, as a linear map.

Equations
• M i =
theorem direct_sum.apply_eq_component (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (f : (λ (i : ι), M i)) (i : ι) :
f i = M i) f
@[ext]
theorem direct_sum.ext (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {f g : (λ (i : ι), M i)} (h : (i : ι), M i) f = M i) g) :
f = g
theorem direct_sum.ext_iff (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {f g : (λ (i : ι), M i)} :
f = g (i : ι), M i) f = M i) g
@[simp]
theorem direct_sum.lof_apply (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) (b : M i) :
( ι M i) b) i = b
@[simp]
theorem direct_sum.component.lof_self (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i : ι) (b : M i) :
M i) ( ι M i) b) = b
theorem direct_sum.component.of (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] (i j : ι) (b : M j) :
M i) ( ι M j) b) = dite (j = i) (λ (h : j = i), h.rec_on b) (λ (h : ¬j = i), 0)
def direct_sum.lequiv_congr_left (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {κ : Type u_1} (h : ι κ) :
(λ (i : ι), M i) ≃ₗ[R] (λ (k : κ), M ((h.symm) k))

Reindexing terms of a direct sum is linear.

Equations
@[simp]
theorem direct_sum.lequiv_congr_left_apply (R : Type u) [semiring R] {ι : Type v} {M : ι Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {κ : Type u_1} (h : ι κ) (f : (λ (i : ι), M i)) (k : κ) :
f) k = f ((h.symm) k)
noncomputable def direct_sum.sigma_lcurry (R : Type u) [semiring R] {ι : Type v} {α : ι Type u_1} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι) (j : α i), (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) →ₗ[R] (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))

curry as a linear map.

Equations
@[simp]
theorem direct_sum.sigma_lcurry_apply (R : Type u) [semiring R] {ι : Type v} {α : ι Type u_1} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι) (j : α i), (δ i j)] (f : direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd)) (i : ι) (j : α i) :
( f) i) j = f i, j⟩
def direct_sum.sigma_luncurry (R : Type u) [semiring R] {ι : Type v} {α : ι Type u_1} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι) (j : α i), (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] :
(λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j)) →ₗ[R] direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd)

uncurry as a linear map.

Equations
@[simp]
theorem direct_sum.sigma_luncurry_apply (R : Type u) [semiring R] {ι : Type v} {α : ι Type u_1} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι) (j : α i), (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] (f : (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))) (i : ι) (j : α i) :
f) i, j⟩ = (f i) j
noncomputable def direct_sum.sigma_lcurry_equiv (R : Type u) [semiring R] {ι : Type v} {α : ι Type u_1} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι) (j : α i), (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) ≃ₗ[R] (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))

curry_equiv as a linear equiv.

Equations
@[simp]
theorem direct_sum.lequiv_prod_direct_sum_symm_apply (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] [Π (i : option ι), (α i)] (ᾰ : × (λ (i : ι), α (option.some i))) :
noncomputable def direct_sum.lequiv_prod_direct_sum (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] [Π (i : option ι), (α i)] :
direct_sum (option ι) (λ (i : option ι), α i) ≃ₗ[R] × (λ (i : ι), α (option.some i))

Linear isomorphism obtained by separating the term of index none of a direct sum over option ι.

Equations
@[simp]
theorem direct_sum.lequiv_prod_direct_sum_apply (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] [Π (i : option ι), (α i)] (ᾰ : direct_sum (option ι) (λ (i : option ι), α i)) :
def direct_sum.coe_linear_map {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] (A : ι M) :
(λ (i : ι), (A i)) →ₗ[R] M

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
@[simp]
theorem direct_sum.coe_linear_map_of {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] (A : ι M) (i : ι) (x : (A i)) :
((direct_sum.of (λ (i : ι), (A i)) i) x) = x
theorem direct_sum.is_internal.submodule_supr_eq_top {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (h : direct_sum.is_internal A) :

If a direct sum of submodules is internal then the submodules span the module.

theorem direct_sum.is_internal.submodule_independent {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (h : direct_sum.is_internal A) :

If a direct sum of submodules is internal then the submodules are independent.

noncomputable def direct_sum.is_internal.collected_basis {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (h : direct_sum.is_internal A) {α : ι Type u_2} (v : Π (i : ι), basis (α i) R (A i)) :
basis (Σ (i : ι), α i) R M

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
@[simp]
theorem direct_sum.is_internal.collected_basis_coe {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (h : direct_sum.is_internal A) {α : ι Type u_2} (v : Π (i : ι), basis (α i) R (A i)) :
(h.collected_basis v) = λ (a : Σ (i : ι), α i), ((v a.fst) a.snd)
theorem direct_sum.is_internal.collected_basis_mem {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (h : direct_sum.is_internal A) {α : ι Type u_2} (v : Π (i : ι), basis (α i) R (A i)) (a : Σ (i : ι), α i) :
theorem direct_sum.is_internal.is_compl {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} {i j : ι} (hij : i j) (h : set.univ = {i, j}) (hi : direct_sum.is_internal A) :
is_compl (A i) (A j)

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.

theorem direct_sum.is_internal_submodule_of_independent_of_supr_eq_top {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] {A : ι M} (hi : complete_lattice.independent A) (hs : supr A = ) :

Note that this is not generally true for [semiring R]; see complete_lattice.independent.dfinsupp_lsum_injective for details.

theorem direct_sum.is_internal_submodule_iff_independent_and_supr_eq_top {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] (A : ι M) :

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.

theorem direct_sum.is_internal_submodule_iff_is_compl {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [ M] (A : ι M) {i j : ι} (hij : i j) (h : set.univ = {i, j}) :
is_compl (A i) (A j)

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.

theorem direct_sum.is_internal.add_submonoid_independent {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} {A : ι } (h : direct_sum.is_internal A) :
theorem direct_sum.is_internal.add_subgroup_independent {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} {A : ι } (h : direct_sum.is_internal A) :