Direct sum of modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 (direct_sum.coe_linear_map), 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 more generally
elsewhere as direct_sum.is_internal, but its basic consequences on submodules are established
in this file.
@[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 (direct_sum ι (λ (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 (direct_sum ι (λ (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_smul R S]
[Π (i : ι), module S (M i)]
[∀ (i : ι), is_scalar_tower R S (M i)] :
is_scalar_tower R S (direct_sum ι (λ (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 (direct_sum ι (λ (i : ι), M 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 : ι) :
M i →ₗ[R] direct_sum ι (λ (i : ι), M i)
Inclusion of each component into the direct sum.
Equations
- direct_sum.lof R ι M = dfinsupp.lsingle
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) :
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 : direct_sum ι (λ (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) :
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 φ = ⇑(dfinsupp.lsum ℕ) φ
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) :
⇑(direct_sum.to_module R ι N φ) = ⇑(direct_sum.to_add_monoid (λ (i : ι), (φ i).to_add_monoid_hom))
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]
(ψ : 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.
@[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]
⦃ψ ψ' : direct_sum ι (λ (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.
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) :
direct_sum ↥S (λ (i : ↥S), M ↑i) →ₗ[R] direct_sum ↥T (λ (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
- 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 (λ (i : subtype T), M ↑i) ⟨↑i, _⟩)
@[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 : direct_sum ι (λ (i : ι), M i))
(i : ι) :
⇑(direct_sum.linear_equiv_fun_on_fintype R ι M) x i = ⇑x 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 ι] :
direct_sum ι (λ (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
- direct_sum.linear_equiv_fun_on_fintype R ι M = {to_fun := coe_fn (direct_sum.has_coe_to_fun ι (λ (i : ι), M i)), map_add' := _, map_smul' := _, inv_fun := dfinsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}
@[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) :
⇑(direct_sum.linear_equiv_fun_on_fintype R ι M) (⇑(direct_sum.lof R ι M i) m) = pi.single i m
@[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) :
⇑((direct_sum.linear_equiv_fun_on_fintype R ι M).symm) (pi.single i m) = ⇑(direct_sum.lof R ι M i) m
@[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 : direct_sum ι (λ (i : ι), M i)) :
⇑((direct_sum.linear_equiv_fun_on_fintype R ι M).symm) ⇑f = f
@[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 ι] :
direct_sum ι (λ (_x : ι), M) ≃ₗ[R] M
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 : ι) :
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 = 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 : direct_sum ι (λ (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 : direct_sum ι (λ (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 : direct_sum ι (λ (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.lequiv_congr_left
(R : Type u)
[semiring R]
{ι : Type v}
{M : ι → Type w}
[Π (i : ι), add_comm_monoid (M i)]
[Π (i : ι), module R (M i)]
{κ : Type u_1}
(h : ι ≃ κ) :
direct_sum ι (λ (i : ι), M i) ≃ₗ[R] direct_sum κ (λ (k : κ), M (⇑(h.symm) k))
Reindexing terms of a direct sum is linear.
Equations
- direct_sum.lequiv_congr_left R h = {to_fun := (direct_sum.equiv_congr_left h).to_fun, map_add' := _, map_smul' := _, inv_fun := (direct_sum.equiv_congr_left h).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
direct_sum.lequiv_congr_left_apply
(R : Type u)
[semiring R]
{ι : Type v}
{M : ι → Type w}
[Π (i : ι), add_comm_monoid (M i)]
[Π (i : ι), module R (M i)]
{κ : Type u_1}
(h : ι ≃ κ)
(f : direct_sum ι (λ (i : ι), M i))
(k : κ) :
noncomputable
def
direct_sum.sigma_lcurry
(R : Type u)
[semiring R]
{ι : Type v}
{α : ι → Type u_1}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
[Π (i : ι) (j : α i), module R (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) →ₗ[R] direct_sum ι (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))
curry as a linear map.
Equations
- direct_sum.sigma_lcurry R = {to_fun := direct_sum.sigma_curry.to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
direct_sum.sigma_lcurry_apply
(R : Type u)
[semiring R]
{ι : Type v}
{α : ι → Type u_1}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
[Π (i : ι) (j : α i), module R (δ i j)]
(f : direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd))
(i : ι)
(j : α i) :
def
direct_sum.sigma_luncurry
(R : Type u)
[semiring R]
{ι : Type v}
{α : ι → Type u_1}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
[Π (i : ι) (j : α i), module R (δ i j)]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι) (j : α i), decidable_eq (δ i j)] :
direct_sum ι (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j)) →ₗ[R] direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd)
uncurry as a linear map.
Equations
- direct_sum.sigma_luncurry R = {to_fun := direct_sum.sigma_uncurry.to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
direct_sum.sigma_luncurry_apply
(R : Type u)
[semiring R]
{ι : Type v}
{α : ι → Type u_1}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
[Π (i : ι) (j : α i), module R (δ i j)]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι) (j : α i), decidable_eq (δ i j)]
(f : direct_sum ι (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j)))
(i : ι)
(j : α i) :
noncomputable
def
direct_sum.sigma_lcurry_equiv
(R : Type u)
[semiring R]
{ι : Type v}
{α : ι → Type u_1}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
[Π (i : ι) (j : α i), module R (δ i j)]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι) (j : α i), decidable_eq (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) ≃ₗ[R] direct_sum ι (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))
curry_equiv as a linear equiv.
Equations
- direct_sum.sigma_lcurry_equiv R = {to_fun := direct_sum.sigma_curry_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := direct_sum.sigma_curry_equiv.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
direct_sum.lequiv_prod_direct_sum_symm_apply
(R : Type u)
[semiring R]
{ι : Type v}
[dec_ι : decidable_eq ι]
{α : option ι → Type w}
[Π (i : option ι), add_comm_monoid (α i)]
[Π (i : option ι), module R (α i)]
(ᾰ : α option.none × direct_sum ι (λ (i : ι), α (option.some i))) :
noncomputable
def
direct_sum.lequiv_prod_direct_sum
(R : Type u)
[semiring R]
{ι : Type v}
[dec_ι : decidable_eq ι]
{α : option ι → Type w}
[Π (i : option ι), add_comm_monoid (α i)]
[Π (i : option ι), module R (α i)] :
direct_sum (option ι) (λ (i : option ι), α i) ≃ₗ[R] α option.none × direct_sum ι (λ (i : ι), α (option.some i))
Linear isomorphism obtained by separating the term of index none of a direct sum over
option ι.
Equations
- direct_sum.lequiv_prod_direct_sum R = {to_fun := direct_sum.add_equiv_prod_direct_sum.to_fun, map_add' := _, map_smul' := _, inv_fun := direct_sum.add_equiv_prod_direct_sum.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
direct_sum.lequiv_prod_direct_sum_apply
(R : Type u)
[semiring R]
{ι : Type v}
[dec_ι : decidable_eq ι]
{α : option ι → Type w}
[Π (i : option ι), add_comm_monoid (α i)]
[Π (i : option ι), module R (α i)]
(ᾰ : direct_sum (option ι) (λ (i : option ι), α i)) :
def
direct_sum.coe_linear_map
{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) :
direct_sum ι (λ (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 ι. This is direct_sum.coe_add_monoid_hom as a linear_map.
Equations
- direct_sum.coe_linear_map A = direct_sum.to_module R ι M (λ (i : ι), (A i).subtype)
@[simp]
theorem
direct_sum.coe_linear_map_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.coe_linear_map A) (⇑(direct_sum.of (λ (i : ι), ↥(A i)) i) x) = ↑x
theorem
direct_sum.is_internal.submodule_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.is_internal A) :
If a direct sum of submodules is internal then the submodules span the module.
theorem
direct_sum.is_internal.submodule_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.is_internal A) :
If a direct sum of submodules is internal then the submodules are independent.
noncomputable
def
direct_sum.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.is_internal A)
{α : ι → Type u_2}
(v : Π (i : ι), basis (α i) R ↥(A i)) :
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
- h.collected_basis v = {repr := ((linear_equiv.of_bijective (direct_sum.coe_linear_map A) h).symm.trans (dfinsupp.map_range.linear_equiv (λ (i : ι), (v i).repr))).trans (sigma_finsupp_lequiv_dfinsupp R).symm}
@[simp]
theorem
direct_sum.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.is_internal A)
{α : ι → Type u_2}
(v : Π (i : ι), basis (α i) R ↥(A i)) :
theorem
direct_sum.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.is_internal A)
{α : ι → Type u_2}
(v : Π (i : ι), basis (α i) R ↥(A i))
(a : Σ (i : ι), α i) :
⇑(h.collected_basis v) a ∈ A a.fst
theorem
direct_sum.is_internal.is_compl
{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 : ι}
(hij : i ≠ j)
(h : set.univ = {i, j})
(hi : direct_sum.is_internal A) :
is_compl (A i) (A j)
When indexed by only two distinct elements, direct_sum.is_internal implies
the two submodules are complementary. Over a ring R, this is true as an iff, as
direct_sum.is_internal_iff_is_compl.
theorem
direct_sum.is_internal_submodule_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.
theorem
direct_sum.is_internal_submodule_iff_independent_and_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) :
iff version of direct_sum.is_internal_submodule_of_independent_of_supr_eq_top,
direct_sum.is_internal.independent, and direct_sum.is_internal.supr_eq_top.
theorem
direct_sum.is_internal_submodule_iff_is_compl
{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)
{i j : ι}
(hij : i ≠ j)
(h : set.univ = {i, j}) :
direct_sum.is_internal A ↔ is_compl (A i) (A j)
If a collection of submodules has just two indices, i and j, then
direct_sum.is_internal is equivalent to is_compl.
Now copy the lemmas for subgroup and submonoids.
theorem
direct_sum.is_internal.add_submonoid_independent
{ι : Type v}
[dec_ι : decidable_eq ι]
{M : Type u_1}
[add_comm_monoid M]
{A : ι → add_submonoid M}
(h : direct_sum.is_internal A) :
theorem
direct_sum.is_internal.add_subgroup_independent
{ι : Type v}
[dec_ι : decidable_eq ι]
{M : Type u_1}
[add_comm_group M]
{A : ι → add_subgroup M}
(h : direct_sum.is_internal A) :