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 ofRsemimodules indexed overι.
@[instance]
def
direct_sum.semimodule
{R : Type u}
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)] :
semimodule R (direct_sum ι (λ (i : ι), M i))
Equations
def
direct_sum.lmk
(R : Type u)
[semiring R]
(ι : Type v)
[decidable_eq ι]
(M : ι → Type w)
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(s : finset ι) :
Create the direct sum given a family M of R semimodules indexed over ι.
Equations
- direct_sum.lmk R ι M = dfinsupp.lmk M R
def
direct_sum.lof
(R : Type u)
[semiring R]
(ι : Type v)
[decidable_eq ι]
(M : ι → Type w)
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(i : ι) :
M i →ₗ[R] direct_sum ι (λ (i : ι), M i)
Inclusion of each component into the direct sum.
Equations
- direct_sum.lof R ι M = dfinsupp.lsingle M R
theorem
direct_sum.single_eq_lof
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule 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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule 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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule 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.
def
direct_sum.to_module
(R : Type u)
[semiring R]
(ι : Type v)
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(N : Type u₁)
[add_comm_group N]
[semimodule R N] :
(Π (i : ι), M i →ₗ[R] N) → (direct_sum ι (λ (i : ι), M i) →ₗ[R] N)
The linear map constructed using the universal property of the coproduct.
Equations
- direct_sum.to_module R ι N φ = {to_fun := direct_sum.to_group (λ (i : ι), ⇑(φ i)) _, map_add' := _, map_smul' := _}
@[simp]
theorem
direct_sum.to_module_lof
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
{N : Type u₁}
[add_comm_group N]
[semimodule 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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
{N : Type u₁}
[add_comm_group N]
[semimodule R N]
(ψ : direct_sum ι (λ (i : ι), M i) →ₗ[R] N)
(f : direct_sum ι (λ (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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
{N : Type u₁}
[add_comm_group N]
[semimodule R N]
{ψ ψ' : direct_sum ι (λ (i : ι), M i) →ₗ[R] N}
(H : ∀ (i : ι), ψ.comp (direct_sum.lof R ι M i) = ψ'.comp (direct_sum.lof R ι M i))
(f : direct_sum ι (λ (i : ι), M i)) :
def
direct_sum.lset_to_set
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(S T : set ι) :
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 (direct_sum ↥T (λ (i : ↥T), M ↑i)) (λ (i : ↥S), direct_sum.lof R ↥T (M ∘ subtype.val) ⟨i.val, _⟩)
def
direct_sum.lid
(R : Type u)
[semiring R]
(M : Type v)
[add_comm_group M]
[semimodule R M] :
direct_sum punit (λ (_x : punit), M) ≃ₗ[R] M
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)
[decidable_eq ι]
(M : ι → Type w)
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(i : ι) :
direct_sum ι (λ (i : ι), M i) →ₗ[R] M i
The projection map onto one component, as a linear map.
Equations
- direct_sum.component R ι M i = {to_fun := λ (f : direct_sum ι (λ (i : ι), M i)), ⇑f i, map_add' := _, map_smul' := _}
@[simp]
theorem
direct_sum.lof_apply
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(i : ι)
(b : M i) :
⇑(⇑(direct_sum.lof R ι M i) b) i = b
theorem
direct_sum.apply_eq_component
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
(f : direct_sum ι (λ (i : ι), M i))
(i : ι) :
⇑f i = ⇑(direct_sum.component R ι M i) f
@[simp]
theorem
direct_sum.component.lof_self
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule 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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule 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)
@[ext]
theorem
direct_sum.ext
(R : Type u)
[semiring R]
{ι : Type v}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
{f g : direct_sum ι (λ (i : ι), M i)} :
(∀ (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}
[decidable_eq ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), semimodule R (M i)]
{f g : direct_sum ι (λ (i : ι), M i)} :
f = g ↔ ∀ (i : ι), ⇑(direct_sum.component R ι M i) f = ⇑(direct_sum.component R ι M i) g