# mathlibdocumentation

algebra.direct_sum.module

# 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

• R is a commutative ring,
• ι is a discrete type,
• S is a finite set in ι,
• M is a family of R modules indexed over ι.
@[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
@[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)
@[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)
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) :
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.submodule_is_internal {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [semiring R] [ M] (A : ι → M) :
Prop

The direct_sum formed by a collection of submodules of M is said to be internal if the canonical map (⨁ i, A i) →ₗ[R] M is bijective.

For the alternate statement in terms of independence and spanning, see direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top.

Equations
theorem direct_sum.submodule_is_internal.to_add_submonoid {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [semiring R] [ M] (A : ι → M) :
theorem direct_sum.submodule_is_internal.to_add_subgroup {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [ring R] [ M] (A : ι → M) :
theorem direct_sum.submodule_is_internal.supr_eq_top {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [semiring R] [ M] {A : ι → M}  :

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

theorem direct_sum.submodule_is_internal.independent {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [semiring R] [ M] {A : ι → M}  :

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

theorem direct_sum.submodule_is_internal_of_independent_of_supr_eq_top {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [ring R] [ 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.submodule_is_internal_iff_independent_and_supr_eq_top {ι : Type v} [dec_ι : decidable_eq ι] {R : Type u_1} {M : Type u_2} [ring R] [ M] (A : ι → M) :

iff version of direct_sum.submodule_is_internal_of_independent_of_supr_eq_top, direct_sum.submodule_is_internal.independent, and direct_sum.submodule_is_internal.supr_eq_top.