LinearMap.coeFn_sum
theorem LinearMap.coeFn_sum :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{σ₁₂ : R →+* R₂} {ι : Type u_10} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂),
⇑(t.sum fun i => f i) = t.sum fun i => ⇑(f i)
The theorem `LinearMap.coeFn_sum` states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, a ring homomorphism `σ₁₂` from `R` to `R₂`, a finite set `t` of type `ι`, and a function `f` mapping each element of `t` to a linear map from `M` to `M₂`, the function application of the sum of the linear maps (obtained by summing over `t`) is equal to the sum of the function applications of the individual linear maps. In other words, the operation of taking a function application distributes over the operation of taking a sum of linear maps.
More concisely: For any semirings R and R₂, additive commutative monoids M and M₂, modules M over R and M₂ over R₂, a ring homomorphism σ₁₂ from R to R₂, a finite set ι, and a function f from ι to the linear maps from M to M₂, the sum of the function applications of the linear maps in the set f is equal to the function application of the sum of these linear maps.
|
LinearMap.sum_apply
theorem LinearMap.sum_apply :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {ι : Type u_9} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
[inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M),
(t.sum fun d => f d) b = t.sum fun d => (f d) b
The theorem `LinearMap.sum_apply` states that for any semiring `R`, any semiring `R₂`, any additively commutative monoids `M` and `M₂`, any module `M` over `R`, any module `M₂` over `R₂`, any ring homomorphism from `R` to `R₂`, any finite set `t` of elements of some type `ι`, any function `f` from `ι` to the type of linear maps from `M` to `M₂` under the ring homomorphism, and any element `b` of `M`, the linear map obtained by summing over `t` the linear maps given by `f`, when applied to `b`, is equal to the sum, over `t`, of the results of applying the linear map given by `f` to `b`. In mathematical notation, this can be expressed as $(∑_{d \in t} f(d))(b) = ∑_{d \in t} f(d)(b)$.
More concisely: For any semirings R and R₂, additively commutative monoids M and M₂, module M over R, module M₂ over R₂, ring homomorphism r : R -> R₂, finite set ι, function f : ι -> LinMap(M -> M₂) under r, and b in M, (∑d in t. f(d))(b) = ∑d in t. f(d)(b).
|
Submodule.injective_subtype
theorem Submodule.injective_subtype :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M), Function.Injective ⇑p.subtype
This theorem states that for any given semiring `R`, an additive commutative monoid `M` and a module `M` over `R`, any submodule `p` of `M`, the function that embeds the submodule `p` into the ambient space `M` is injective. In mathematical terms, if we denote this embedding function as `f`, then for any two elements `x` and `y` in `p`, if `f(x) = f(y)` then `x = y`. This means that the embedding perfectly retains the distinctness of the elements in the submodule when they are mapped to the larger ambient space `M`.
More concisely: The embedding of a submodule of an `R`-module into the ambient space is an injective function.
|
Submodule.coe_sum
theorem Submodule.coe_sum :
∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) (x : ι → ↥p) (s : Finset ι), ↑(s.sum fun i => x i) = s.sum fun i => ↑(x i)
This theorem, named `Submodule.coe_sum`, states that for any semiring `R`, an additive commutative monoid `M` and a `Module` structure on `R` and `M`, if you have a submodule `p` of `M` and a function `x` from some index set `ι` into `p`, then the coercion to `M` of the sum (over a finite set `s` of indices) of the results of `x` is equal to the sum (over the same set `s`) of the coerced results of `x`. In plain words, summing first and then coercing yields the same result as coercing first and then summing. Note, the same lemma for `AddSubmonoid` is called `AddSubmonoid.coe_finset_sum`.
More concisely: For any semiring `R`, additive commutative monoid `M` with a `Module` structure, submodule `p` of `M`, and function `x` from some finite index set into `p`, the coercion of the sum of `x` to `M` is equal to the sum of the coerced values of `x`.
|