mathlib documentation

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

@[instance]
def direct_sum.module {R : Type u} [semiring R] {ι : Type v} {M : ι → Type w} [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] :
module R (⨁ (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 : ι), module R (M i)] {S : Type u_1} [semiring S] [Π (i : ι), module S (M i)] [∀ (i : ι), smul_comm_class R S (M i)] :
smul_comm_class R S (⨁ (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 : ι), module R (M i)] {S : Type u_1} [semiring S] [has_scalar R S] [Π (i : ι), module S (M i)] [∀ (i : ι), is_scalar_tower R S (M i)] :
is_scalar_tower R S (⨁ (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 : ι), module R (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 : ι), module R (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 : ι), module R (M i)] (i : ι) :
M i →ₗ[R] ⨁ (i : ι), M i

Inclusion of each component into the direct sum.

Equations
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 : ι), module R (M i)] (i : ι) (b : M i) :
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 : ι), module R (M i)] (s : finset ι) (c : R) (x : Π (i : s), M i.val) :
(direct_sum.mk M s) (c x) = c (direct_sum.mk M 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 : ι), module R (M i)] (i : ι) (c : R) (x : M i) :
(direct_sum.of M i) (c x) = c (direct_sum.of M 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 : ι), module R (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 : ι), module R (M i)] (N : Type u₁) [add_comm_monoid N] [module R N] (φ : Π (i : ι), M i →ₗ[R] N) :
(⨁ (i : ι), M i) →ₗ[R] N

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

Equations
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 : ι), module R (M i)] (N : Type u₁) [add_comm_monoid N] [module R 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 : ι), module R (M i)] {N : Type u₁} [add_comm_monoid N] [module R N] {φ : Π (i : ι), M i →ₗ[R] N} (i : ι) (x : M i) :
(direct_sum.to_module R ι N φ) ((direct_sum.lof R ι 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 : ι), module R (M i)] {N : Type u₁} [add_comm_monoid N] [module R N] (ψ : (⨁ (i : ι), M i) →ₗ[R] N) (f : ⨁ (i : ι), M i) :
ψ f = (direct_sum.to_module R ι N (λ (i : ι), ψ.comp (direct_sum.lof R ι 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_monoid (M i)] [Π (i : ι), module R (M i)] {N : Type u₁} [add_comm_monoid N] [module R N] {ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N} (H : ∀ (i : ι), ψ.comp (direct_sum.lof R ι M i) = ψ'.comp (direct_sum.lof R ι 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_monoid (M i)] [Π (i : ι), module R (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
def direct_sum.lid (R : Type u) [semiring R] (M : Type v) (ι : Type u_1 := punit) [add_comm_monoid M] [module R 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 : ι), module R (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_monoid (M i)] [Π (i : ι), module R (M i)] (f : ⨁ (i : ι), M i) (i : ι) :
f i = (direct_sum.component R ι 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 : ι), module R (M i)] {f g : ⨁ (i : ι), M i} (h : ∀ (i : ι), (direct_sum.component R ι M i) f = (direct_sum.component R ι 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 : ι), module R (M i)] {f g : ⨁ (i : ι), M i} :
f = g ∀ (i : ι), (direct_sum.component R ι M i) f = (direct_sum.component R ι 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 : ι), module R (M i)] (i : ι) (b : M i) :
((direct_sum.lof R ι 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 : ι), module R (M i)] (i : ι) (b : M i) :
(direct_sum.component R ι M i) ((direct_sum.lof R ι 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 : ι), module R (M i)] (i j : ι) (b : M j) :
(direct_sum.component R ι M i) ((direct_sum.lof R ι 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] [add_comm_monoid M] [module R M] (A : ι → submodule R 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.

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] [add_comm_monoid M] [module R M] (A : ι → submodule R 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] [add_comm_group M] [module R M] (A : ι → submodule R 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] [add_comm_monoid M] [module R M] (A : ι → submodule R M) (h : direct_sum.submodule_is_internal A) :