mathlib documentation

algebra.direct_sum.module

Direct sum of modules #

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, 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 as direct_sum.submodule_is_internal, and its basic consequences are established.

@[protected, 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
@[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 : ι), 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)
@[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 : ι), 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)
@[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 : ι), module R (M i)] [Π (i : ι), module Rᵐᵒᵖ (M i)] [∀ (i : ι), is_central_scalar R (M i)] :
is_central_scalar R (⨁ (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.lof_eq_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 : ι) (b : M i) :
(direct_sum.lof R ι M i) b = (direct_sum.of M 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 : ι), 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.

@[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 : ι), 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)) :
ψ = ψ'

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

See note [partially-applied ext lemmas].

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
@[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 : ι), module R (M i)] [fintype ι] (x : ⨁ (i : ι), M i) (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 : ι), module R (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 : ι), module R (M i)] [fintype ι] [decidable_eq ι] (i : ι) (m : M i) :
@[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 : ι), module R (M i)] [fintype ι] [decidable_eq ι] (i : ι) (m : M i) :
@[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 : ι), module R (M i)] [fintype ι] (f : ⨁ (i : ι), M i) :
@[protected]
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_coe {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] (A : ι → submodule R 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 ι

Equations
@[simp]
theorem direct_sum.submodule_coe_of {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] (A : ι → submodule R M) (i : ι) (x : (A i)) :
(direct_sum.submodule_coe A) ((direct_sum.of (λ (i : ι), (A i)) i) x) = x
theorem direct_sum.coe_of_submodule_apply {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] (A : ι → submodule R M) (i j : ι) (x : (A i)) :
(((direct_sum.of (λ (i : ι), (A i)) i) x) j) = ite (i = j) x 0
def direct_sum.submodule_is_internal {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [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.

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 {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] (A : ι → submodule R M) :
theorem direct_sum.submodule_is_internal.supr_eq_top {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] {A : ι → submodule R M} (h : direct_sum.submodule_is_internal A) :

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

theorem direct_sum.submodule_is_internal.independent {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] {A : ι → submodule R M} (h : direct_sum.submodule_is_internal A) :

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

noncomputable def direct_sum.submodule_is_internal.collected_basis {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] {A : ι → submodule R M} (h : direct_sum.submodule_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.submodule_is_internal.collected_basis_coe {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] {A : ι → submodule R M} (h : direct_sum.submodule_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.submodule_is_internal.collected_basis_mem {R : Type u} [semiring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_monoid M] [module R M] {A : ι → submodule R M} (h : direct_sum.submodule_is_internal A) {α : ι → Type u_2} (v : Π (i : ι), basis (α i) R (A i)) (a : Σ (i : ι), α i) :
theorem direct_sum.submodule_is_internal.to_add_subgroup {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_group M] [module R M] (A : ι → submodule R M) :
theorem direct_sum.submodule_is_internal_of_independent_of_supr_eq_top {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] {M : Type u_1} [add_comm_group M] [module R M] {A : ι → submodule R 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.

Now copy the lemmas for subgroup and submonoids.