# 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 `Submodule`s are established in this file.

source
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

source
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)
source
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)
source
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)
source
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
source
def DirectSum.coeFnLinearMap (R : Type u) [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
(DirectSum ι fun (i : ι) => M i) →ₗ[R] (i : ι) → M i

Coercion from a `DirectSum` to a pi type is a `LinearMap`.

Equations

- DirectSum.coeFnLinearMap R = DFinsupp.coeFnLinearMap R

Instances For

source
@[simp]
theorem DirectSum.coeFnLinearMap_apply {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (v : DirectSum ι fun (i : ι) => M i) :
(coeFnLinearMap R) v = ⇑v
source
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

Instances For

source
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

Instances For

source
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) :
(lof R ι M i) b = (of M i) b
source
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 = (lof R ι M i) b
source
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) :
(mk M s) (c • x) = c • (mk M s) x

Scalar multiplication commutes with direct sums.

source
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) :
(of M i) (c • x) = c • (of M i) x

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

source
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
source
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 ℕ) φ

Instances For

source
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) :
⇑(toModule R ι N φ) = ⇑(toAddMonoid fun (i : ι) => (φ i).toAddMonoidHom)

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

source
@[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) :
(toModule R ι N φ) ((lof R ι M i) x) = (φ i) x

The map constructed using the universal property gives back the original maps when restricted to each component.

source
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 = (toModule R ι N fun (i : ι) => ψ ∘ₗ 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.

source
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 : ι), ψ ∘ₗ lof R ι M i = ψ' ∘ₗ lof R ι M i) :
ψ = ψ'

Two `LinearMap`s out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas].

source
theorem DirectSum.linearMap_ext_iff {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} :
ψ = ψ' ↔ ∀ (i : ι), ψ ∘ₗ lof R ι M i = ψ' ∘ₗ lof R ι M i
source
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, ⋯⟩

Instances For

source
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 = DFinsupp.linearEquivFunOnFintype

Instances For

source
@[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) (i : ι) :
(linearEquivFunOnFintype R ι M) a✝ i = a✝ i
source
@[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) :
(linearEquivFunOnFintype R ι M) ((lof R ι M i) m) = Pi.single i m
source
@[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) :
(linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (lof R ι M i) m
source
@[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) :
(linearEquivFunOnFintype R ι M).symm ⇑f = f
source
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 := ⋯ }

Instances For

source
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

Instances For

source
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 = (component R ι M i) f
source
theorem DirectSum.ext_component (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 : ι), (component R ι M i) f = (component R ι M i) g) :
f = g
source
theorem DirectSum.ext_component_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 : ι), (component R ι M i) f = (component R ι M i) g
source
@[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) :
((lof R ι M i) b) i = b
source
@[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) :
(component R ι M i) ((lof R ι M i) b) = b
source
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) :
(component R ι M i) ((lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0
source
theorem DirectSum.mker_map {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i) :
AddMonoidHom.mker (map f) = AddSubmonoid.comap (coeFnAddMonoidHom M) (AddSubmonoid.pi Set.univ fun (i : ι) => AddMonoidHom.mker (f i))
source
theorem DirectSum.mrange_map {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i) :
AddMonoidHom.mrange (map f) = AddSubmonoid.comap (coeFnAddMonoidHom N) (AddSubmonoid.pi Set.univ fun (i : ι) => AddMonoidHom.mrange (f i))
source
def DirectSum.lmap {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
(DirectSum ι fun (i : ι) => M i) →ₗ[R] DirectSum ι fun (i : ι) => N i

The linear map between direct sums induced by a family of linear maps.

Equations

- DirectSum.lmap f = DFinsupp.mapRange.linearMap f

Instances For

source
@[simp]
theorem DirectSum.lmap_apply {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x : DirectSum ι fun (i : ι) => M i) (i : ι) :
((lmap f) x) i = (f i) (x i)
source
@[simp]
theorem DirectSum.lmap_of {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) [DecidableEq ι] (i : ι) (x : M i) :
(lmap f) ((of M i) x) = (of N i) ((f i) x)
source
@[simp]
theorem DirectSum.lmap_lof {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) [DecidableEq ι] (i : ι) (x : M i) :
(lmap f) ((lof R ι M i) x) = (lof R ι N i) ((f i) x)
source
@[simp]
theorem DirectSum.lmap_id {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
(lmap fun (i : ι) => LinearMap.id) = LinearMap.id
source
@[simp]
theorem DirectSum.lmap_comp {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) {K : ι → Type u_2} [(i : ι) → AddCommMonoid (K i)] [(i : ι) → Module R (K i)] (g : (i : ι) → N i →ₗ[R] K i) :
(lmap fun (i : ι) => g i ∘ₗ f i) = lmap g ∘ₗ lmap f
source
theorem DirectSum.lmap_injective {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
Function.Injective ⇑(lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)
source
theorem DirectSum.lmap_surjective {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
Function.Surjective ⇑(lmap f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)
source
theorem DirectSum.lmap_eq_iff {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x y : DirectSum ι fun (i : ι) => M i) :
(lmap f) x = (lmap f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)
source
theorem DirectSum.toAddMonoidHom_lmap {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
(lmap f).toAddMonoidHom = map fun (i : ι) => (f i).toAddMonoidHom
source
theorem DirectSum.lmap_eq_map {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x : DirectSum ι fun (i : ι) => M i) :
(lmap f) x = (map fun (i : ι) => (f i).toAddMonoidHom) x
source
theorem DirectSum.ker_lmap {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
LinearMap.ker (lmap f) = Submodule.comap (coeFnLinearMap R) (Submodule.pi Set.univ fun (i : ι) => LinearMap.ker (f i))
source
theorem DirectSum.range_lmap {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_1} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) :
LinearMap.range (lmap f) = Submodule.comap (coeFnLinearMap R) (Submodule.pi Set.univ fun (i : ι) => LinearMap.range (f i))
source
theorem DirectSum.ker_map {ι : Type v} {M : ι → Type w} {N : ι → Type u_2} [(i : ι) → AddCommGroup (M i)] [(i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i) :
(map f).ker = AddSubgroup.comap (coeFnAddMonoidHom M) (AddSubgroup.pi Set.univ fun (x : ι) => (f x).ker)
source
theorem DirectSum.range_map {ι : Type v} {M : ι → Type w} {N : ι → Type u_2} [(i : ι) → AddCommGroup (M i)] [(i : ι) → AddCommGroup (N i)] (f : (i : ι) → M i →+ N i) :
(map f).range = AddSubgroup.comap (coeFnAddMonoidHom N) (AddSubgroup.pi Set.univ fun (x : ι) => (f x).range)
source
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 = DFinsupp.domLCongr h

Instances For

source
@[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 : κ) :
((lequivCongrLeft R h) f) k = f (h.symm k)
source
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' := ⋯ }

Instances For

source
@[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) :
(((sigmaLcurry R) f) i) j = f ⟨i, j⟩
source
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' := ⋯ }

Instances For

source
@[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) :
((sigmaLuncurry R) f) ⟨i, j⟩ = (f i) j
source
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 = DFinsupp.sigmaCurryLEquiv

Instances For

source
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.

Instances For

source
@[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) :
(lequivProdDirectSum R) a✝ = addEquivProdDirectSum.toFun a✝
source
@[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)) :
(lequivProdDirectSum R).symm a✝ = addEquivProdDirectSum.invFun a✝
source
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

Instances For

source
theorem DirectSum.coeLinearMap_eq_dfinsuppSum {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)) :
(coeLinearMap A) x = DFinsupp.sum x fun (i : ι) (x : ↥(A i)) => ↑x
source
@[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)) :
(coeLinearMap A) ((of (fun (i : ι) => ↥(A i)) i) x) = ↑x
source
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 (coeLinearMap A) = ⨆ (i : ι), A i
source
@[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 : IsInternal A) {i : ι} (x : ↥(A i)) :
((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x
source
@[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 : IsInternal A) {i j : ι} (hij : i ≠ j) (x : ↥(A i)) :
((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) j = 0
source
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 : IsInternal A) {i : ι} {x : M} (hx : x ∈ A i) :
((LinearEquiv.ofBijective (coeLinearMap A) h).symm x) i = ⟨x, hx⟩
source
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 : IsInternal A) {i j : ι} (hij : i ≠ j) {x : M} (hx : x ∈ A i) :
((LinearEquiv.ofBijective (coeLinearMap A) h).symm x) j = 0
source
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 : IsInternal A) :
iSup A = ⊤

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

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

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

source
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 : IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.Basis (α i) R ↥(A i)) :
Module.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.

Instances For

source
@[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 : IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.Basis (α i) R ↥(A i)) :
⇑(h.collectedBasis v) = fun (a : (i : ι) × α i) => ↑((v a.fst) a.snd)
source
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 : IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.Basis (α i) R ↥(A i)) (a : (i : ι) × α i) :
(h.collectedBasis v) a ∈ A a.fst
source
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 : IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.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
source
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 : IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.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
source
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 : 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`.

source
theorem DirectSum.isInternal_submodule_of_iSupIndep_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 : iSupIndep A) (hs : iSup A = ⊤) :
IsInternal A

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

source
theorem DirectSum.isInternal_submodule_iff_iSupIndep_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) :
IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤

`iff` version of `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top`, `DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`.

source
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}) :
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`.

source
@[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} :
(IsInternal fun (i : { i : ι // A i ≠ ⊥ }) => A ↑i) ↔ IsInternal A
source
theorem DirectSum.isInternal_biSup_submodule_of_iSupIndep {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 : iSupIndep fun (i : ↑s) => A ↑i) :
IsInternal fun (i : ↑s) => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Now copy the lemmas for subgroup and submonoids.

source
theorem DirectSum.IsInternal.addSubmonoid_iSupIndep {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_2} [AddCommMonoid M] {A : ι → AddSubmonoid M} (h : IsInternal A) :
iSupIndep A
source
theorem DirectSum.IsInternal.addSubgroup_iSupIndep {ι : Type v} [dec_ι : DecidableEq ι] {G : Type u_2} [AddCommGroup G] {A : ι → AddSubgroup G} (h : IsInternal A) :
iSupIndep A