DirectSum.of_smul
theorem DirectSum.of_smul :
∀ (R : Type u) [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] (i : ι) (c : R) (x : M i),
(DirectSum.of M i) (c • x) = c • (DirectSum.of M i) x
The theorem `DirectSum.of_smul` states that for any semiring `R`, any type `ι` with decidable equality, and any indexed type `M` where each `M i` is an `R`-module (i.e., an additive commutative monoid and a module over the semiring `R`), scalar multiplication commutes with the inclusion of each component into the direct sum. More specifically, for any index `i`, scalar `c` from `R`, and element `x` from `M i`, the direct sum of the scaled element `c • x` equals the scaled direct sum of the element `x`, where `•` denotes scalar multiplication.
More concisely: For any semiring `R`, type `ι` with decidable equality, and indexed `R-module M i`, the scalar multiplication of an element `x` from `M i` by `c` in `R` commutes with the inclusion of `x` into the direct sum of `M i`, i.e., `c • x = (∑ i: ι, c • x i)`.
|
DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
theorem DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
[inst_2 : Module R M] {A : ι → Submodule R M},
CompleteLattice.Independent A → iSup A = ⊤ → DirectSum.IsInternal A
This theorem, `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top`, states that for any ring `R`, an index type `ι` with decidable equality, and a type `M` that is both an additive commutative group and an `R`-module, if `A` is a function from the index type to a submodule of the `R`-module, then if `A` is a complete lattice independent and the indexed supremum (iSup) of `A` is the top element (⊤), then `A` is an internal direct sum. Essentially, it ensures that under these conditions, the set `A` of submodules forms an internal direct sum in the ring `R`. Note that the theorem is not always true for semirings, and more details can be found at `CompleteLattice.Independent.dfinsupp_lsum_injective`.
More concisely: If `R` is a ring, `ι` is an index type with decidable equality, `M` is an additive commutative group and an `R`-module, `A : ι → submodule M`, and `A` is a complete lattice independent such that iSup `A` = ⊤, then `A` is an internal direct sum of submodules in `M`.
|
DirectSum.IsInternal.submodule_iSup_eq_top
theorem DirectSum.IsInternal.submodule_iSup_eq_top :
∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {A : ι → Submodule R M}, DirectSum.IsInternal A → iSup A = ⊤
This theorem states that if a direct sum of submodules is internal, then these submodules span the entire module.
More specifically, for any semiring `R`, and any type `ι` with decidable equality, given a module `M` over `R` that is an additive commutative monoid, and a family `A` of submodules of `M` indexed by `ι`, if the direct sum of the submodules in `A` is internal, then the supremum of the submodules in `A`, denoted as `iSup A`, equals the entire module `M`, denoted as `⊤`. This essentially means that the submodules in `A` cover the whole module `M`.
More concisely: If `M` is a module over a semiring `R` with decidable equality, and `A` is a family of submodules of `M` whose internal direct sum equals `M`, then the supremum of `A` equals `M`.
|
DirectSum.linearMap_ext
theorem DirectSum.linearMap_ext :
∀ (R : Type u) [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] {N : Type u₁}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] ⦃ψ ψ' : (DirectSum ι fun i => M i) →ₗ[R] N⦄,
(∀ (i : ι), ψ ∘ₗ DirectSum.lof R ι M i = ψ' ∘ₗ DirectSum.lof R ι M i) → ψ = ψ'
The theorem `DirectSum.linearMap_ext` states that given a type `R` which is a semiring, a type `ι` with decidable equality, a type family `M` indexed by `ι` such that for each `i` we have an additive commutative monoid and a module over `R`, a type `N` which is an additive commutative monoid and a module over `R`, and two linear maps `ψ` and `ψ'` from the direct sum of `M` to `N`; if for all `i` in `ι`, the composition of `ψ` and the inclusion map of `M i` into the direct sum is equal to the composition of `ψ'` and the inclusion map, then `ψ` is equal to `ψ'`. This theorem is essentially capturing the property that a linear map out of a direct sum is uniquely determined by its values on the constituent parts of the sum.
More concisely: Given semiring `R`, decidable type `ι`, additive commutative monoid and `R`-modules `M i` and `N`, and linear maps `ψ` and `ψ'` from the direct sum of `M` to `N`, if `ψ ∘ i = ψ' ∘ i` for all `i` in `ι`, then `ψ = ψ'`.
|
DirectSum.toModule_lof
theorem DirectSum.toModule_lof :
∀ (R : Type u) [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] {N : Type u₁}
[inst_3 : AddCommMonoid N] [inst_4 : 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 theorem `DirectSum.toModule_lof` asserts that for any semiring `R`, a type `ι` with decidable equality, a family of `R`-modules indexed by `ι` (represented as `M : ι → Type w`), and any `R`-module `N`, for any linear maps `φ : (i : ι) → M i →ₗ[R] N` and any element `i : ι` and `x : M i`, the map constructed using the universal property of the coproduct (the direct sum), when applied to the inclusion of `x` from the `i`-th component into the direct sum, gives back the original linear map applied to `x`. This is to say, the universal property-based map and the original maps agree on each component of the direct sum.
More concisely: For any semiring `R`, given families of `R`-modules `M : ι → Type` and `N : Type`, linear maps `φ : ι → M → N`, and elements `i : ι` and `x : M i`, the map obtained from the universal property of the direct sum of `M` and the inclusion of `x` into the direct sum agrees with the original linear map `φ` applied to `x`.
|
DirectSum.IsInternal.isCompl
theorem DirectSum.IsInternal.isCompl :
∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {A : ι → Submodule R M} {i j : ι},
i ≠ j → Set.univ = {i, j} → DirectSum.IsInternal A → IsCompl (A i) (A j)
This theorem states that given a semiring `R`, a type `ι` with decidable equality, an additively commutative monoid `M`, and a module over `R` and `M`, along with a function `A` mapping elements of `ι` to submodules of `R` and `M`, and two distinct elements `i` and `j` of `ι`, if the universal set is equal to the set containing only `i` and `j` and `A` forms an internal direct sum, then the submodules `A i` and `A j` are complementary. In other words, for a ring `R` and two distinct submodules indexed by `ι`, if the submodules form an internal direct sum, they complement each other. This is a bi-directional relationship as shown in `DirectSum.isInternal_submodule_iff_isCompl`.
More concisely: Given a semiring `R`, a type `ι` with decidable equality, an additively commutative monoid `M`, a module `M` over `R`, and a family `A` of submodules of `R` and `M` indexed by `ι`, if the submodules `A i` and `A j` form an internal direct sum for distinct indices `i` and `j`, then `A i` is the complement of `A j` and vice versa.
|
DirectSum.mk_smul
theorem DirectSum.mk_smul :
∀ (R : Type u) [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] (s : Finset ι) (c : R)
(x : (i : ↑↑s) → M ↑i), (DirectSum.mk M s) (c • x) = c • (DirectSum.mk M s) x
The theorem `DirectSum.mk_smul` states that for any semiring `R`, any type `ι` with decidable equality, any type family `M` indexed by `ι` such that each `M i` is an additive commutative monoid and a module over `R`, any finset `s` of `ι`, any scalar `c` from `R`, and any function `x` from elements of `s` to respective `M i`, scalar multiplication commutes with the operation of forming direct sums. In other words, scaling the function `x` by `c` and then forming the direct sum is the same as first forming the direct sum of `x` and then scaling the result by `c`.
More concisely: For any semiring R, type ι with decidable equality, type family M indexed by ι over additive commutative monoids and R-modules, finset s of ι, scalar c from R, and function x from s to M i, we have x.sum (map (λ i => c * x i)) = c * (sum x).
Here, `sum` refers to the direct sum operation, and `map` is the function application and composition of functions. `x.sum` is the direct sum of the elements in the function `x`, and `sum x` is the direct sum of the indices in the finset `s`. The statement says that scaling each element by `c` and then summing them up is the same as first summing them up and then scaling the sum by `c`.
|
DirectSum.isInternal_submodule_iff_isCompl
theorem DirectSum.isInternal_submodule_iff_isCompl :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
[inst_2 : Module R M] (A : ι → Submodule R M) {i j : ι},
i ≠ j → Set.univ = {i, j} → (DirectSum.IsInternal A ↔ IsCompl (A i) (A j))
This theorem states that for any ring `R`, index type `ι` with decidable equality, and type `M` that forms an additive commutative group and is a module over `R`, with `A` being a function from `ι` to submodules of `R` and `M`, and given two distinct indices `i` and `j` such that the universal set is equal to the set containing only `i` and `j`, then the assertion that the direct sum `A` is internal is equivalent to the assertion that the submodule `A i` and the submodule `A j` are complements of each other. In other words, if a collection of submodules indexed by `ι` has exactly two indices `i` and `j`, then the collection being an internal direct sum is equivalent to the two corresponding submodules being complements of each other.
More concisely: For any ring `R`, index type `ι` with decidable equality, and module `M` over `R`, if `A` is a function from `ι` to submodules of `M` such that `|ι| = 2` and `A i` and `A j` are complements of each other, then `A` forms an internal direct sum of `M`.
|
DirectSum.IsInternal.submodule_independent
theorem DirectSum.IsInternal.submodule_independent :
∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {A : ι → Submodule R M}, DirectSum.IsInternal A → CompleteLattice.Independent A
The theorem `DirectSum.IsInternal.submodule_independent` states that for any semiring `R` and any type `ι` with decidable equality, given an additive commutative monoid `M` that is also a `R`-module, if the direct sum of submodules indexed by `ι` is internal to `M`, then these submodules are independent. In other words, if we have a family of submodules (`A : ι → Submodule R M`) such that their direct sum forms an internal structure in the module `M`, then the submodules in this family are independent in the sense of the complete lattice structure.
More concisely: If `M` is an additive commutative `R`-module with decidable equality and the family `(A : ι → Submodule R M)` of its submodules has an internal direct sum in `M`, then the submodules `A i` are pairwise independent.
|
DirectSum.toModule.unique
theorem DirectSum.toModule.unique :
∀ (R : Type u) [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] {N : Type u₁}
[inst_3 : AddCommMonoid N] [inst_4 : 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
The theorem `DirectSum.toModule.unique` states that for any semiring `R`, any set `ι` with decidable equality, any family of `R`-modules `M i` indexed by `ι`, and any `R`-module `N`, every linear map `ψ` from the direct sum of the `M i` into `N` agrees with the linear map obtained by applying the universal property of the direct sum to each component of `ψ`. In other words, if `f` is an element of the direct sum, the effect of applying `ψ` to `f` is the same as constructing a new linear map by applying the universal property to each component of `ψ` and then applying this new map to `f`.
More concisely: Given any semiring `R`, set `ι` with decidable equality, a family of `R`-modules `M i` indexed by `ι`, and an `R`-module `N`, any linear map `ψ` from the direct sum of `M i` into `N` coincides with the linear map obtained by applying the universal property to each component of `ψ`.
|
DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top
theorem DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
[inst_2 : Module R M] (A : ι → Submodule R M),
DirectSum.IsInternal A ↔ CompleteLattice.Independent A ∧ iSup A = ⊤
This theorem, `DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top`, states the following: for any ring `R`, type `ι` with decidable equality, additive commutative group `M`, and `R`-module structure on `M`, given a function `A` that maps elements of type `ι` to submodules of `R` on `M`, the assertion `DirectSum.IsInternal A` is equivalent to the conjunction of two conditions: `CompleteLattice.Independent A`, meaning that the submodules are independent, and `iSup A = ⊤`, meaning that the indexed supremum of the submodules equals the top element of the lattice. In other words, the direct sum of the submodules is internal if and only if the submodules are independent and their supremum is the entire space.
More concisely: A family of submodules of an additive commutative group endowed with an R-module structure is the internal direct sum of its submodules if and only if the submodules are independent and their supremum equals the entire space.
|
DirectSum.coe_toModule_eq_coe_toAddMonoid
theorem DirectSum.coe_toModule_eq_coe_toAddMonoid :
∀ (R : Type u) [inst : Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] {M : ι → Type w}
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] (N : Type u₁)
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] (φ : (i : ι) → M i →ₗ[R] N),
⇑(DirectSum.toModule R ι N φ) = ⇑(DirectSum.toAddMonoid fun i => (φ i).toAddMonoidHom)
The theorem `DirectSum.coe_toModule_eq_coe_toAddMonoid` states that for any semiring `R`, any type `ι` with decidable equality, any family of types `M` indexed by `ι` such that for each `i` in `ι`, `M i` is an additive commutative monoid and a module over `R`, any type `N` that is also an additive commutative monoid and a module over `R`, and any family of linear maps `φ` from `M i` to `N` indexed by `ι`, the function associated with the linear map from the direct sum of the `M i` to `N` (constructed using the universal property of the coproduct) is the same as the function associated with the homomorphism from the direct sum of the `M i` to `N` (induced by a family of homomorphisms from `M i` to `N`). In other words, this theorem asserts that coproducts in the categories of modules and additive monoids commute with the forgetful functor from modules to additive monoids.
More concisely: Given any semiring R, type ι with decidable equality, families M i of additive commutative monoids and R-modules, and N an additive commutative monoid and R-module, the function from the direct sum of the M i to N constructed via the universal property of the coproduct equals the function induced by the family of homomorphisms from M i to N.
|