Finsupp.total_surjective
theorem Finsupp.total_surjective :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{v : α → M}, Function.Surjective v → Function.Surjective ⇑(Finsupp.total α M R v)
The theorem `Finsupp.total_surjective` states that for all types `α`, `M`, and `R`, where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a `R`-module, given a function `v` from `α` to `M`, if the function `v` is surjective, then the function `total`, which interprets a linear combination of elements in the family `v` and evaluates this linear combination, is also surjective. In other words, for every element in the co-domain of `total`, there exists an element in its domain such that applying `total` to that element gives the element in the co-domain.
More concisely: Given a surjective function `v` from type `α` to an `R`-module `M` over a semiring `R`, the function `total` that evaluates linear combinations of `v` is also surjective.
|
Finsupp.mem_span_image_iff_total
theorem Finsupp.mem_span_image_iff_total :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{v : α → M} {s : Set α} {x : M},
x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ Finsupp.supported R R s, (Finsupp.total α M R v) l = x
The theorem `Finsupp.mem_span_image_iff_total` states that for any semiring `R`, an additively commutative monoid `M` that is also an `R`-module, a function `v` from an arbitrary type `α` to `M`, a set `s` of type `α`, and an element `x` of `M`, `x` belongs to the submodule spanned by the image of `s` under `v` in `R` if and only if there exists a function `l` in the submodule of all `p : α →₀ R` such that the support of `p` is a subset of `s` (denoted by `Finsupp.supported R R s`), such that the total of `l` with respect to `v` equals `x`. In other words, `x` is in the span of `s` mapped through `v` if and only if `x` can be expressed as a linear combination of elements in `s`, with the coefficients being the elements in the support of some `l`.
More concisely: For an additively commutative monoid M being an R-module, an R-valued function v from type α, set s of α, and an element x of M, x lies in the submodule spanned by s through v if and only if there exists a function p from s to R, such that the support of p is contained in s and the total of p applied to v equals x.
|
top_le_span_range_iff_forall_exists_fun
theorem top_le_span_range_iff_forall_exists_fun :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] {v : α → M},
⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ c, (Finset.univ.sum fun i => c i • v i) = x
This theorem states that for any types `α` and `M`, and type `R` with predefined instances of `Fintype α`, `Semiring R`, `AddCommMonoid M`, and `Module R M`, a family of vectors `v` (from `α` to `M`) generates the module `M` if and only if every element `x` in `M` can be represented as a finite linear combination of the vectors in `v`. Here, generation of the module `M` is represented by the top module `⊤` being less than or equal to the span of the range of `v`, and the finite linear combination is denoted by the sum over all `i` in the universe of `α` of the product of a scalar `c i` and a vector `v i`, which equals `x`.
More concisely: A family of vectors generates a module if and only if every element in the module can be expressed as a finite linear combination of the vectors.
|
Finsupp.total_id_surjective
theorem Finsupp.total_id_surjective :
∀ (R : Type u_5) [inst : Semiring R] (M : Type u_9) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Function.Surjective ⇑(Finsupp.total M M R id)
The theorem `Finsupp.total_id_surjective` asserts that for any module `M` over a semiring `R`, the function `Finsupp.total M M R id` from the free module `(M →₀ R)` to `M` is surjective. This means that every element of the module `M` can be expressed as a linear combination of elements from the free module `(M →₀ R)`. In other words, any module is a quotient of a free module.
More concisely: For any semiring `R` and module `M` over `R`, the total function from `M` to the free module `(M →₀ R)` is surjective.
|
Submodule.mem_iSup_iff_exists_finset
theorem Submodule.mem_iSup_iff_exists_finset :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
{p : ι → Submodule R M} {m : M}, m ∈ ⨆ i, p i ↔ ∃ s, m ∈ ⨆ i ∈ s, p i
This theorem, `Submodule.mem_iSup_iff_exists_finset`, establishes an equivalence for a module `M` over a semiring `R` and a family of submodules `p` indexed by `ι`. Specifically, it states that a module element `m` is a member of the indexed supremum of the submodules `p` (denoted by `⨆ i, p i`) if and only if there exists a finite set `s` such that `m` is a member of the supremum of the submodules `p` indexed over `s` (denoted by `⨆ i ∈ s, p i`).
More concisely: For a module `M` over a semiring `R` and a family of submodules `p` indexed by `ι`, an element `m` of `M` belongs to the indexed supremum `⨆ i, p i` if and only if it belongs to some finite supremum `⨆ i ∈ s, p i` for some finite set `s` of indices.
|
Finsupp.total_single
theorem Finsupp.total_single :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{v : α → M} (c : R) (a : α), ((Finsupp.total α M R v) fun₀ | a => c) = c • v a
The `Finsupp.total_single` theorem states that for any types `α`, `M`, and `R`, where `R` is a semiring, `M` is an additive commutative monoid and a module over `R`, and for any function `v` from `α` to `M`, and any elements `c` of `R` and `a` of `α`, applying the function `Finsupp.total α M R v` to the function that maps `a` to `c` and other elements of `α` to zero, is equal to the scalar multiplication of `c` and `v a`. In essence, it says that in the linear combination represented by `Finsupp.total`, individual terms are just the scalars times the corresponding vector.
More concisely: For any semiring `R`, additive commutative monoid and `R`-module `M`, function `v` from type `α` to `M`, and elements `c` of `R` and `a` of `α`, `Finsupp.total α M R v (λ x => if x = a then c else 0) = c * v a`.
|
Finsupp.lhom_ext'
theorem Finsupp.lhom_ext' :
∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄,
(∀ (a : α), φ ∘ₗ Finsupp.lsingle a = ψ ∘ₗ Finsupp.lsingle a) → φ = ψ
The theorem `Finsupp.lhom_ext'` states that for any semiring `R`, and for any types `α`, `M` and `N` with `M` and `N` being `R`-modules, if we have two `R`-linear maps `φ` and `ψ` from `Finsupp X M` to `N`, and these two maps agree on each `Finsupp.single a` for every `a` in `α`, then these two maps are equal everywhere.
The formulation of this fact is done using equality of linear maps `φ.comp (Finsupp.lsingle a)` and `ψ.comp (Finsupp.lsingle a)` to allow the `ext` tactic to apply a type-specific extensionality lemma to prove the equality of these maps. As an example, if `M` is equivalent to `R`, it suffices to verify `φ (Finsupp.single a 1) = ψ (Finsupp.single a 1)`.
More concisely: For any semiring `R`, and `R`-modules `M` and `N`, if two `R`-linear maps from `Finsupp X M` to `N` agree on each `Finsupp.single a` for every `a` in `α`, then they are equal everywhere.
|
Finsupp.total_apply
theorem Finsupp.total_apply :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{v : α → M} (l : α →₀ R), (Finsupp.total α M R v) l = l.sum fun i a => a • v i
The theorem `Finsupp.total_apply` states that for any types `α`, `M`, and `R`, where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a module over `R`, and for any function `v : α → M` and `l : α →₀ R`, applying the total function `Finsupp.total α M R v` to `l` is equivalent to computing the sum over `l` where each term in the sum is a scalar multiple of `v i`, where the scalar is `a` and the multiplication is given by the module structure. In simpler terms, this theorem equates the total of a linear combination to the sum of the scaled vectors in the combination.
More concisely: For any semiring `R`, additive commutative monoid `M` that is an `R`-module, function `v : α → M`, and `α`-indexed family `l : α →₀ R`, the sum of scaled vectors `∑ i in α, l i ⊤ v i` equals the application of the total function `Finsupp.total α M R v` to `l`.
|
mem_span_set'
theorem mem_span_set' :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M}
{s : Set M}, m ∈ Submodule.span R s ↔ ∃ n f g, (Finset.univ.sum fun i => f i • ↑(g i)) = m
The theorem `mem_span_set'` states that for any given element `m` from a module `M` over a semiring `R`, and any set `s` of elements from `M`, `m` belongs to the `R`-submodule spanned by the set `s` if and only if there exist an integer `n`, a function `f` from `Fin n` to `R`, and a function `g` from `Fin n` to the underlying set of `s` such that `m` equals to the sum, indexed by the universal finite set `Finset.univ`, of the scalar multiples (`f i • ↑(g i)`) of the images of `g`. In simple words, `m` belongs to the submodule spanned by `s` if and only if `m` can be expressed as a finite linear combination of elements from `s`.
More concisely: A module element `m` belongs to the submodule spanned by a set `s` of module elements if and only if it can be expressed as a finite linear combination of elements from `s`.
|
Finsupp.single_mem_supported
theorem Finsupp.single_mem_supported :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{s : Set α} {a : α} (b : M), a ∈ s → (fun₀ | a => b) ∈ Finsupp.supported M R s
The theorem `Finsupp.single_mem_supported` states that for any given type `α`, a semiring `R`, an additive commutative monoid `M` which is also a module over `R`, a set `s` of type `α`, an element `a` of type `α`, and an element `b` of type `M`, if `a` belongs to the set `s`, then the function `fun₀` such that it maps `a` to `b` and all other elements to `0`, belongs to the `R`-submodule of all functions from `α` to `M` (`α →₀ M`) whose support is a subset of `s`. This is essentially saying that a function mapping a single element of `s` to a non-zero value is within the submodule of all functions whose non-zero values are contained within `s`.
More concisely: If `s` is a set, `α` a type, `R` a semiring, `M` an additive commutative `R`-module, `a` an element of `α` in `s`, and `b` an element of `M`, then the function mapping `a` to `b` and all other elements to `0` belongs to the `R`-submodule of all functions from `α` to `M` with support contained in `s`.
|
Finsupp.span_eq_range_total
theorem Finsupp.span_eq_range_total :
∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
Submodule.span R s = LinearMap.range (Finsupp.total (↑s) M R Subtype.val)
This theorem, `Finsupp.span_eq_range_total`, establishes an equivalence between two mathematical concepts in the context of a module `M` over a semiring `R`. Specifically, it states that for any set `s` of elements within the module `M`, the span of `s` (i.e., the smallest submodule of `M` that contains `s`) is equal to the range of the function `Finsupp.total` when evaluated over the elements of `s`, viewed as subtypes, and mapped to `M` under `Subtype.val`. In simpler terms, all linear combinations of elements from `s` (as given by `Finsupp.total`) exactly constitute the span of `s`.
More concisely: The span of a set `s` in a module `M` over a semiring equals the range of the function `Finsupp.total` when applied to elements of `s` viewed as subtypes and mapped to `M` under `Subtype.val`.
|
Finsupp.supported_eq_span_single
theorem Finsupp.supported_eq_span_single :
∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] (s : Set α),
Finsupp.supported R R s = Submodule.span R ((fun i => fun₀ | i => 1) '' s)
This theorem states that for any given set `s` of type `α` and a semiring `R`, the `R`-submodule of all functions `p : α → R` such that the support of `p` is a subset of `s` (defined as `Finsupp.supported R R s`) is equal to the smallest submodule of `R` that contains the image set under the function which maps each element `i` in `s` to the function `fun₀ | i => 1` (defined as `Submodule.span R ((fun i => fun₀ | i => 1) '' s)`). Essentially, it says that the submodule of functions with support in `s` is the same as the submodule spanned by the singleton functions for each element in `s`.
More concisely: The submodule of functions on a set `α` with support in a subset `s` is equal to the submodule spanned by the singleton functions for elements in `s`.
|
mem_span_set
theorem mem_span_set :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M}
{s : Set M}, m ∈ Submodule.span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m
The theorem `mem_span_set` asserts that for any semiring `R`, any additive commutative monoid `M`, and any `R`-module structure on `M`, an element `m` of `M` is contained in the `R`-submodule spanned by a set `s` (a subset of `M`), if and only if `m` can be written as a finite `R`-linear combination of elements of `s`. Here, a finite `R`-linear combination of elements of `s` means a sum of the form `c.sum fun mi r => r • mi`, where `c` is a function whose support is a subset of `s`, `r` are elements of `R`, and `mi` are elements of `M`. The support of a function is the set of points where the function is non-zero. The `•` operation indicates scalar multiplication in the context of `R`-modules.
More concisely: An element of an `R`-module `M` is in the submodule spanned by a set `s` if and only if it can be expressed as a finite `R`-linear combination of elements in `s`.
|
mem_span_range_iff_exists_fun
theorem mem_span_range_iff_exists_fun :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] {v : α → M} {x : M},
x ∈ Submodule.span R (Set.range v) ↔ ∃ c, (Finset.univ.sum fun i => c i • v i) = x
This theorem states that for any given types `α`, `M`, and `R`, where `α` is a finite type, `R` is a semiring, and `M` is a module over `R`, and given a function `v` from `α` to `M` and an element `x` of `M`, `x` lies in the span of the range of `v` if and only if there exists a function `c` such that `x` equals the sum over all elements `i` of the finite type `α` of the scalar product of `c i` and `v i`. In other words, any element of the span of the range of `v` can be expressed as a linear combination of the elements in the range of `v`.
More concisely: For any finite type `α`, semiring `R`, and `R`-module `M`, function `v` from `α` to `M`, and `x` in `M`, `x` is in the span of `v` if and only if there exists `c` in `R^α` such that `x = ∑ i in α (c i ⊤ v i)`, where `∑` denotes summation and `⊤` denotes the transpose operation.
|
Finsupp.range_total
theorem Finsupp.range_total :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{v : α → M}, LinearMap.range (Finsupp.total α M R v) = Submodule.span R (Set.range v)
The theorem `Finsupp.range_total` states that for any given type `α`, type `M`, and semiring `R`, given the conditions that `M` is an additive commutative monoid and that `M` is a module over `R`, for any function `v` from `α` to `M`, the range of the linear map resulting from applying `Finsupp.total` to `v` (which interprets a finitely supported function as a linear combination of the elements in `v` and evaluates this linear combination) is equal to the span of the range of `v` in `M` (which is the smallest submodule of `M` that contains the range of `v`).
More concisely: For any type `α`, semiring `R`, additive commutative monoid and `R`-module `M`, and function `v` from `α` to `M`, the range of `Finsupp.total v` equals the span of the range of `v` in `M`.
|
Finsupp.mem_supported
theorem Finsupp.mem_supported :
∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{s : Set α} (p : α →₀ M), p ∈ Finsupp.supported M R s ↔ ↑p.support ⊆ s
The theorem `Finsupp.mem_supported` states that for any types `α`, `M`, and `R`, given a semiring `R`, an additive commutative monoid `M`, and a module structure on `M` over `R`, a function `p` from `α` to `M` is in the submodule `Finsupp.supported M R s` for a set `s` of `α` if and only if the support of `p` (the set of points where `p` is non-zero) is a subset of `s`. In other words, it describes the condition under which a function `p` belongs to the submodule of all functions whose non-zero values lie within a specified set `s`.
More concisely: A function from a type `α` to an additive commutative `R`-module `M` belongs to the submodule `Finsupp.supported M R s` if and only if the support of the function is contained in the set `s`.
|
Finsupp.lhom_ext
theorem Finsupp.lhom_ext :
∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄,
(∀ (a : α) (b : M), (φ fun₀ | a => b) = ψ fun₀ | a => b) → φ = ψ
The theorem `Finsupp.lhom_ext` states that for any two `R`-linear maps (`φ` and `ψ`) from the finitely supported function space `Finsupp X M` to `N`, if they agree on each singleton function (i.e., functions that map a single element `x` to a value `y`), then they agree everywhere. This is observed under the constraints that `R` forms a semiring, `M` and `N` are additive commutative monoids, and both `M` and `N` are `R`-modules.
More concisely: If `φ` and `ψ` are `R`-linear maps agreeing on singleton functions from the finitely supported function space `Finsupp X M` to an additive commutative monoid `N`, which are both `R`-modules, then `φ` and `ψ` are equal.
|
span_eq_iUnion_nat
theorem span_eq_iUnion_nat :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
↑(Submodule.span R s) =
⋃ n, (fun f => Finset.univ.sum fun i => (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}
The theorem `span_eq_iUnion_nat` states that for any semiring `R`, additive commutative monoid `M`, and any set `s` of elements from `M`, the span of `s` (which is the smallest submodule of `M` containing `s`) is equal to the union over all natural numbers `n` of the set of all linear combinations of at most `n` terms from `s`. Here, each linear combination is given by summing over all elements of the universal finite set of `n`, where each summand is the product of a scalar (first element of `f i`) and a vector from `s` (second element of `f i`), where `f` is a function that maps each element of `n` to a pair of a scalar and a vector from `s`.
More concisely: The span of a set in an additive commutative monoid is equal to the union of the sets of all linear combinations of at most each natural number of its elements.
|