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 (DirectSum.toModule.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 (DirectSum.coeLinearMap), 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 DirectSum.IsInternal, but its basic consequences on Submodules are established in this file.

instance DirectSum.instModule {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : Module R (DirectSum ι fun (i : ι) => M i)

Equations

• DirectSum.instModule = DFinsupp.module

instance DirectSum.instSMulCommClass {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {S : Type u_1} [Semiring S] [(i : ι) → Module S (M i)] [∀ (i : ι), SMulCommClass R S (M i)] : SMulCommClass R S (DirectSum ι fun (i : ι) => M i)

Equations

• ⋯ = ⋯

instance DirectSum.instIsScalarTower {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {S : Type u_1} [Semiring S] [SMul R S] [(i : ι) → Module S (M i)] [∀ (i : ι), IsScalarTower R S (M i)] : IsScalarTower R S (DirectSum ι fun (i : ι) => M i)

Equations

• ⋯ = ⋯

instance DirectSum.instIsCentralScalar {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module Rᵐᵒᵖ (M i)] [∀ (i : ι), IsCentralScalar R (M i)] : IsCentralScalar R (DirectSum ι fun (i : ι) => M i)

Equations

• ⋯ = ⋯

theorem DirectSum.smul_apply {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (b : R) (v : DirectSum ι fun (i : ι) => M i) (i : ι) : (b • v) i = b • v i

def DirectSum.lmk (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (s : Finset ι) : ((i : ↑↑s) → M ↑i) →ₗ[R] DirectSum ι fun (i : ι) => M i

Create the direct sum given a family M of R modules indexed over ι.

Equations

• DirectSum.lmk R ι M = DFinsupp.lmk

def DirectSum.lof (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) : M i →ₗ[R] DirectSum ι fun (i : ι) => M i

Inclusion of each component into the direct sum.

Equations

• DirectSum.lof R ι M = DFinsupp.lsingle

theorem DirectSum.lof_eq_of (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (b : M i) : (DirectSum.lof R ι M i) b = (DirectSum.of M i) b

theorem DirectSum.single_eq_lof (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (b : M i) : DFinsupp.single i b = (DirectSum.lof R ι M i) b

theorem DirectSum.mk_smul (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (s : Finset ι) (c : R) (x : (i : ↑↑s) → M ↑i) : (DirectSum.mk M s) (c • x) = c • (DirectSum.mk M s) x

Scalar multiplication commutes with direct sums.

theorem DirectSum.of_smul (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (c : R) (x : M i) : (DirectSum.of M i) (c • x) = c • (DirectSum.of M i) x

Scalar multiplication commutes with the inclusion of each component into the direct sum.

theorem DirectSum.support_smul {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [(i : ι) → (x : M i) → Decidable (x ≠ 0)] (c : R) (v : DirectSum ι fun (i : ι) => M i) : DFinsupp.support (c • v) ⊆ DFinsupp.support v

def DirectSum.toModule (R : Type u) [Semiring R] (ι : Type v) {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (N : Type u₁) [AddCommMonoid N] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) : (DirectSum ι fun (i : ι) => M i) →ₗ[R] N

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

Equations

• DirectSum.toModule R ι N φ = (DFinsupp.lsum ℕ) φ

theorem DirectSum.coe_toModule_eq_coe_toAddMonoid (R : Type u) [Semiring R] (ι : Type v) {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (N : Type u₁) [AddCommMonoid N] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) : ⇑(DirectSum.toModule R ι N φ) = ⇑(DirectSum.toAddMonoid fun (i : ι) => (φ i).toAddMonoidHom)

Coproducts in the categories of modules and additive monoids commute with the forgetful functor from modules to additive monoids.

@[simp]

theorem DirectSum.toModule_lof (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] {N : Type u₁} [AddCommMonoid N] [Module R N] {φ : (i : ι) → M i →ₗ[R] N} (i : ι) (x : M i) : (DirectSum.toModule R ι N φ) ((DirectSum.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 DirectSum.toModule.unique (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] {N : Type u₁} [AddCommMonoid N] [Module R N] (ψ : (DirectSum ι fun (i : ι) => M i) →ₗ[R] N) (f : DirectSum ι fun (i : ι) => M i) : ψ f = (DirectSum.toModule R ι N fun (i : ι) => ψ ∘ₗ DirectSum.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 DirectSum.linearMap_ext (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] {N : Type u₁} [AddCommMonoid N] [Module R N] ⦃ψ ψ' : (DirectSum ι fun (i : ι) => M i) →ₗ[R] N⦄ (H : ∀ (i : ι), ψ ∘ₗ DirectSum.lof R ι M i = ψ' ∘ₗ DirectSum.lof R ι M i) : ψ = ψ'

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

See note [partially-applied ext lemmas].

def DirectSum.lsetToSet (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (S T : Set ι) (H : S ⊆ T) : (DirectSum ↑S fun (i : ↑S) => M ↑i) →ₗ[R] DirectSum ↑T fun (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

• DirectSum.lsetToSet R S T H = DirectSum.toModule R (↑S) (DirectSum ↑T fun (i : ↑T) => M ↑i) fun (i : ↑S) => DirectSum.lof R (↑T) (fun (i : Subtype T) => M ↑i) ⟨↑i, ⋯⟩

def DirectSum.linearEquivFunOnFintype (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] : (DirectSum ι fun (i : ι) => M i) ≃ₗ[R] (i : ι) → M i

Given Fintype α, linearEquivFunOnFintype R is the natural R-linear equivalence between ⨁ i, M i and ∀ i, M i.

Equations

• DirectSum.linearEquivFunOnFintype R ι M = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯, invFun := DFinsupp.equivFunOnFintype.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem DirectSum.linearEquivFunOnFintype_apply (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (a✝ : Π₀ (i : ι), (fun (i : ι) => M i) i) (a : ι) : (DirectSum.linearEquivFunOnFintype R ι M) a✝ a = a✝ a

@[simp]

theorem DirectSum.linearEquivFunOnFintype_lof (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [Fintype ι] (i : ι) (m : M i) : (DirectSum.linearEquivFunOnFintype R ι M) ((DirectSum.lof R ι M i) m) = Pi.single i m

@[simp]

theorem DirectSum.linearEquivFunOnFintype_symm_single (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [Fintype ι] (i : ι) (m : M i) : (DirectSum.linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (DirectSum.lof R ι M i) m

@[simp]

theorem DirectSum.linearEquivFunOnFintype_symm_coe (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (f : DirectSum ι fun (i : ι) => M i) : (DirectSum.linearEquivFunOnFintype R ι M).symm ⇑f = f

def DirectSum.lid (R : Type u) [Semiring R] (M : Type v) (ι : Type u_1 := PUnit.{u_1 + 1} ) [AddCommMonoid M] [Module R M] [Unique ι] : (DirectSum ι fun (x : ι) => M) ≃ₗ[R] M

The natural linear equivalence between ⨁ _ : ι, M and M when Unique ι.

Equations

• DirectSum.lid R M ι = { toFun := (DirectSum.id M ι).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (DirectSum.id M ι).invFun, left_inv := ⋯, right_inv := ⋯ }

def DirectSum.component (R : Type u) [Semiring R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) : (DirectSum ι fun (i : ι) => M i) →ₗ[R] M i

The projection map onto one component, as a linear map.

Equations

• DirectSum.component R ι M i = DFinsupp.lapply i

theorem DirectSum.apply_eq_component (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (f : DirectSum ι fun (i : ι) => M i) (i : ι) : f i = (DirectSum.component R ι M i) f

theorem DirectSum.ext (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {f g : DirectSum ι fun (i : ι) => M i} (h : ∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g) : f = g

theorem DirectSum.ext_iff (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {f g : DirectSum ι fun (i : ι) => M i} : f = g ↔ ∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g

@[simp]

theorem DirectSum.lof_apply (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (b : M i) : ((DirectSum.lof R ι M i) b) i = b

@[simp]

theorem DirectSum.component.lof_self (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (b : M i) : (DirectSum.component R ι M i) ((DirectSum.lof R ι M i) b) = b

theorem DirectSum.component.of (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i j : ι) (b : M j) : (DirectSum.component R ι M i) ((DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0

def DirectSum.lequivCongrLeft (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type u_1} (h : ι ≃ κ) : (DirectSum ι fun (i : ι) => M i) ≃ₗ[R] DirectSum κ fun (k : κ) => M (h.symm k)

Reindexing terms of a direct sum is linear.

Equations

• DirectSum.lequivCongrLeft R h = { toFun := (DirectSum.equivCongrLeft h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (DirectSum.equivCongrLeft h).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem DirectSum.lequivCongrLeft_apply (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type u_1} (h : ι ≃ κ) (f : DirectSum ι fun (i : ι) => M i) (k : κ) : ((DirectSum.lequivCongrLeft R h) f) k = f (h.symm k)

def DirectSum.sigmaLcurry (R : Type u) [Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [DecidableEq ι] [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] : (DirectSum ((x : ι) × α x) fun (i : (x : ι) × α x) => δ i.fst i.snd) →ₗ[R] DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

curry as a linear map.

Equations

• DirectSum.sigmaLcurry R = { toFun := (↑DirectSum.sigmaCurry).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DirectSum.sigmaLcurry_apply (R : Type u) [Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [DecidableEq ι] [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] (f : DirectSum ((x : ι) × α x) fun (i : (x : ι) × α x) => δ i.fst i.snd) (i : ι) (j : α i) : (((DirectSum.sigmaLcurry R) f) i) j = f ⟨i, j⟩

def DirectSum.sigmaLuncurry (R : Type u) [Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [DecidableEq ι] [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] : (DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) →ₗ[R] DirectSum ((x : ι) × α x) fun (i : (x : ι) × α x) => δ i.fst i.snd

uncurry as a linear map.

Equations

• DirectSum.sigmaLuncurry R = { toFun := (↑DirectSum.sigmaUncurry).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DirectSum.sigmaLuncurry_apply (R : Type u) [Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [DecidableEq ι] [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] (f : DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) (i : ι) (j : α i) : ((DirectSum.sigmaLuncurry R) f) ⟨i, j⟩ = (f i) j

def DirectSum.sigmaLcurryEquiv (R : Type u) [Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [DecidableEq ι] [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] : (DirectSum ((x : ι) × α x) fun (i : (x : ι) × α x) => δ i.fst i.snd) ≃ₗ[R] DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

curryEquiv as a linear equiv.

Equations

• DirectSum.sigmaLcurryEquiv R = { toFun := DirectSum.sigmaCurryEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := DirectSum.sigmaCurryEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

noncomputable def DirectSum.lequivProdDirectSum (R : Type u) [Semiring R] {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] : (DirectSum (Option ι) fun (i : Option ι) => α i) ≃ₗ[R] α none × DirectSum ι fun (i : ι) => α (some i)

Linear isomorphism obtained by separating the term of index none of a direct sum over Option ι.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DirectSum.lequivProdDirectSum_symm_apply (R : Type u) [Semiring R] {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] (a✝ : α none × DirectSum ι fun (i : ι) => α (some i)) : (DirectSum.lequivProdDirectSum R).symm a✝ = DirectSum.addEquivProdDirectSum.invFun a✝

@[simp]

theorem DirectSum.lequivProdDirectSum_apply (R : Type u) [Semiring R] {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] (a✝ : DirectSum (Option ι) fun (i : Option ι) => α i) : (DirectSum.lequivProdDirectSum R) a✝ = DirectSum.addEquivProdDirectSum.toFun a✝

def DirectSum.coeLinearMap {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] (A : ι → Submodule R M) : (DirectSum ι fun (i : ι) => ↥(A i)) →ₗ[R] M

The canonical linear map from ⨁ i, A i to M where A is a collection of Submodule R M indexed by ι. This is DirectSum.coeAddMonoidHom as a LinearMap.

Equations

• DirectSum.coeLinearMap A = DirectSum.toModule R ι M fun (i : ι) => (A i).subtype

theorem DirectSum.coeLinearMap_eq_dfinsupp_sum {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] (A : ι → Submodule R M) [DecidableEq M] (x : DirectSum ι fun (i : ι) => ↥(A i)) : (DirectSum.coeLinearMap A) x = DFinsupp.sum x fun (i : ι) (x : ↥(A i)) => ↑x

@[simp]

theorem DirectSum.coeLinearMap_of {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] (A : ι → Submodule R M) (i : ι) (x : ↥(A i)) : (DirectSum.coeLinearMap A) ((DirectSum.of (fun (i : ι) => ↥(A i)) i) x) = ↑x

theorem DirectSum.range_coeLinearMap {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} : LinearMap.range (DirectSum.coeLinearMap A) = ⨆ (i : ι), A i

@[simp]

theorem DirectSum.IsInternal.ofBijective_coeLinearMap_same {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i : ι} (x : ↥(A i)) : ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) i = x

@[simp]

theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i j : ι} (hij : i ≠ j) (x : ↥(A i)) : ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) j = 0

theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i : ι} {x : M} (hx : x ∈ A i) : ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) i = ⟨x, hx⟩

theorem DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i j : ι} (hij : i ≠ j) {x : M} (hx : x ∈ A i) : ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) j = 0

theorem DirectSum.IsInternal.submodule_iSup_eq_top {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) : iSup A = ⊤

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

theorem DirectSum.IsInternal.submodule_independent {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) : CompleteLattice.Independent A

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

noncomputable def DirectSum.IsInternal.collectedBasis {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem DirectSum.IsInternal.collectedBasis_coe {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Basis (α i) R ↥(A i)) : ⇑(h.collectedBasis v) = fun (a : (i : ι) × α i) => ↑((v a.fst) a.snd)

theorem DirectSum.IsInternal.collectedBasis_mem {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Basis (α i) R ↥(A i)) (a : (i : ι) × α i) : (h.collectedBasis v) a ∈ A a.fst

theorem DirectSum.IsInternal.collectedBasis_repr_of_mem {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Basis (α i) R ↥(A i)) {x : M} {i : ι} {a : α i} (hx : x ∈ A i) : ((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a

theorem DirectSum.IsInternal.collectedBasis_repr_of_mem_ne {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Basis (α i) R ↥(A i)) {x : M} {i j : ι} (hij : i ≠ j) {a : α j} (hx : x ∈ A i) : ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0

theorem DirectSum.IsInternal.isCompl {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} {i j : ι} (hij : i ≠ j) (h : Set.univ = {i, j}) (hi : DirectSum.IsInternal A) : IsCompl (A i) (A j)

When indexed by only two distinct elements, DirectSum.IsInternal implies the two submodules are complementary. Over a Ring R, this is true as an iff, as DirectSum.isInternal_submodule_iff_isCompl.

theorem DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] {A : ι → Submodule R M} (hi : CompleteLattice.Independent A) (hs : iSup A = ⊤) : DirectSum.IsInternal A

Note that this is not generally true for [Semiring R]; see CompleteLattice.Independent.dfinsupp_lsum_injective for details.

theorem DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (A : ι → Submodule R M) : DirectSum.IsInternal A ↔ CompleteLattice.Independent A ∧ iSup A = ⊤

iff version of DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top, DirectSum.IsInternal.submodule_independent, and DirectSum.IsInternal.submodule_iSup_eq_top.

theorem DirectSum.isInternal_submodule_iff_isCompl {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j) (h : Set.univ = {i, j}) : DirectSum.IsInternal A ↔ IsCompl (A i) (A j)

If a collection of submodules has just two indices, i and j, then DirectSum.IsInternal is equivalent to isCompl.

@[simp]

theorem DirectSum.isInternal_ne_bot_iff {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] {A : ι → Submodule R M} : (DirectSum.IsInternal fun (i : { i : ι // A i ≠ ⊥ }) => A ↑i) ↔ DirectSum.IsInternal A

theorem DirectSum.isInternal_biSup_submodule_of_independent {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] {A : ι → Submodule R M} (s : Set ι) (h : CompleteLattice.Independent fun (i : ↑s) => A ↑i) : DirectSum.IsInternal fun (i : ↑s) => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Now copy the lemmas for subgroup and submonoids.

theorem DirectSum.IsInternal.addSubmonoid_independent {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_2} [AddCommMonoid M] {A : ι → AddSubmonoid M} (h : DirectSum.IsInternal A) : CompleteLattice.Independent A

theorem DirectSum.IsInternal.addSubgroup_independent {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_2} [AddCommGroup M] {A : ι → AddSubgroup M} (h : DirectSum.IsInternal A) : CompleteLattice.Independent A