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
Ris a commutative ring,ιis a discrete type,Sis a finite set inι,Mis a family ofRmodules indexed overι.
@[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)
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 : ι) :
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 ι) :
Create the direct sum given a family M of R modules indexed over ι.
Equations
- direct_sum.lmk R ι M = dfinsupp.lmk
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 : ι) :
Inclusion of each component into the direct sum.
Equations
- direct_sum.lof R ι M = dfinsupp.lsingle
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) :
dfinsupp.single i b = ⇑(direct_sum.lof R ι 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 : ι), 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) :
dfinsupp.support (c • v) ⊆ dfinsupp.support v
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) :
The linear map constructed using the universal property of the coproduct.
Equations
- direct_sum.to_module R ι N φ = ⇑(dfinsupp.lsum ℕ) φ
@[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) :
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) :
The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.
Equations
- direct_sum.lset_to_set R S T H = direct_sum.to_module R ↥S (⨁ (i : ↥T), M ↑i) (λ (i : ↥S), direct_sum.lof R ↥T (λ (i : subtype T), M ↑i) ⟨↑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 ι] :
The natural linear equivalence between ⨁ _ : ι, M and M when unique ι.
Equations
- direct_sum.lid R M ι = {to_fun := (direct_sum.id M ι).to_fun, map_add' := _, map_smul' := _, inv_fun := (direct_sum.id M ι).inv_fun, left_inv := _, right_inv := _}
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 : ι) :
The projection map onto one component, as a linear map.
Equations
- direct_sum.component R ι M i = dfinsupp.lapply i
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
- direct_sum.submodule_is_internal A = function.bijective ⇑(direct_sum.to_module R ι M (λ (i : ι), (A i).subtype))
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) :
direct_sum.submodule_is_internal A ↔ direct_sum.add_submonoid_is_internal (λ (i : ι), (A i).to_add_submonoid)
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) :
direct_sum.submodule_is_internal A ↔ direct_sum.add_subgroup_is_internal (λ (i : ι), (A i).to_add_subgroup)