# mathlibdocumentation

linear_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 semimodules indexed over ι.
@[instance]
def direct_sum.semimodule {R : Type u} [semiring R] {ι : Type v} {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] :
(⨁ (i : ι), M i)

Equations
@[simp]
theorem direct_sum.smul_apply {R : Type u} [semiring R] {ι : Type v} {M : ι → Type w} [Π (i : ι), add_comm_group (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_group (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 semimodules indexed over ι.

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

Inclusion of each component into the direct sum.

Equations
• M =
theorem direct_sum.single_eq_lof (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι → Type w} [Π (i : ι), add_comm_group (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_group (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_group (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_group (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_group (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
@[simp]
theorem direct_sum.to_module_lof (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι → Type w} [Π (i : ι), add_comm_group (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_group (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.

theorem direct_sum.to_module.ext (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] {N : Type u₁} [ N] {ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N} (H : ∀ (i : ι), ψ.comp ι M i) = ψ'.comp ι M i)) (f : ⨁ (i : ι), M i) :
ψ f = ψ' f

def direct_sum.lset_to_set (R : Type u) [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] (S T : set ι) :
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
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_group (M i)] [Π (i : ι), (M i)] (i : ι) :
(⨁ (i : ι), M i) →ₗ[R] M i

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

Equations
theorem direct_sum.apply_eq_component (R : Type u) [semiring R] {ι : Type v} {M : ι → Type w} [Π (i : ι), add_comm_group (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_group (M i)] [Π (i : ι), (M i)] {f g : ⨁ (i : ι), M i} :
(∀ (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_group (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_group (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_group (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_group (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)