Submodule.span_singleton_eq_span_singleton
theorem Submodule.span_singleton_eq_span_singleton :
∀ {R : Type u_9} {M : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {x y : M}, Submodule.span R {x} = Submodule.span R {y} ↔ ∃ z, z • x = y
The theorem `Submodule.span_singleton_eq_span_singleton` states that for any ring `R`, additive commutative group `M`, and a module `M` over `R`, with no zero scalar multiplication divisors in `R` and `M`, and given any two elements `x` and `y` of `M`, the span of the singleton set `{x}` being equal to the span of the singleton set `{y}` in `R` is equivalent to the existence of an element `z` in `R` such that `z` multiplied by `x` equals `y`. In other words, the spans of `x` and `y` are the same if and only if `y` is a scalar multiple of `x`.
More concisely: For any ring R, additive commutative group M, and element x, y in the module M with no zero scalar multiplication divisors, the spans of {x} and {y} in R are equal if and only if y is a scalar multiple of x.
|
Submodule.mem_sup
theorem Submodule.mem_sup :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
{p p' : Submodule R M}, x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x
This theorem states that for any semiring `R`, any additive commutative monoid `M`, and any module `M` over `R`, and given any element `x` of `M` and any two submodules `p` and `p'` of `M`, `x` is in the sup (supremum or join) of `p` and `p'` if and only if there exist elements `y` in `p` and `z` in `p'` such that the sum of `y` and `z` is `x`. In other words, any element in the supremum of two submodules can be expressed as the sum of an element from each of the original submodules.
More concisely: For any semiring `R`, additive commutative monoid `M` with an `R`-module structure, and submodules `p` and `p'` of `M`, the element `x` belongs to the supremum of `p` and `p'` if and only if there exist `y` in `p` and `z` in `p'` such that `x = y + z`.
|
Submodule.map_span
theorem Submodule.map_span :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] [inst_8 : RingHomSurjective σ₁₂]
(f : F) (s : Set M), Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
This theorem, named `Submodule.map_span`, states that for any sets of types `R`, `R₂`, `M`, `M₂`, `F`, where `R` and `R₂` are semirings, `M` and `M₂` are additively commutative monoids and modules over `R` and `R₂` respectively. `F` is a function-like object that maps elements from `M` to `M₂`, and `σ₁₂` is a semilinear map from `R` to `R₂`. If the ring homomorphism `σ₁₂` is surjective, then for any function `f` of type `F` and a set `s` of type `M`, mapping the span of `s` under `f` (where the span is the smallest submodule of `M` that contains `s`) equals the span in `R₂` of the image of `s` under `f`. In mathematical terms, this theorem is saying:
$$f(\text{span}_R(s)) = \text{span}_{R₂}(f(s)).$$
That is, the action of mapping a set's span with a function is the same as taking the span of the function's image of the set.
More concisely: If `σ₁₂:` R → R₂ is a surjective semilinear map between semirings `R` and `R₂`, and `F:` M → M₂ is a function-like object, then for any additively commutative monoids `M` and `M₂`, and any set `s ⊆ M`, `f(span₀ R s) = span₀ R₂ (fs)`, where `span₀` denotes the span in the respective rings.
|
LinearMap.map_span_le
theorem LinearMap.map_span_le :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] [inst_8 : RingHomSurjective σ₁₂]
(f : F) (s : Set M) (N : Submodule R₂ M₂), Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
The theorem `LinearMap.map_span_le` states that for any semiring `R`, additive commutative monoid `M`, module `R M`, semiring `R₂`, function-like mapping `F` from `M` to `M₂`, semilinear map class `F σ₁₂ M M₂` and a surjective ring homomorphism `σ₁₂`, a given function `f`, a set `s` of `M` and a submodule `N` of `M₂`, it holds that the submodule resulting from the map `f` applied to the span of `s` is contained within `N` if and only if for all `m` in `s`, the value `f m` is an element of `N`. This theorem essentially characterizes the relation between the image of the span of a set under a function and a given submodule in the codomain.
More concisely: For any semiring `R`, additive commutative monoid `M`, semiring `R₂`, function-like mapping `F` from `M` to `M₂`, semilinear map `F σ₁₂ M M₂`, and a surjective ring homomorphism `σ₁₂`, if `s` is a set of `M` and `N` is a submodule of `M₂`, then the image of the span of `s` under `F` is contained in `N` if and only if each element `m` in `s` maps to an element in `N` under `F`.
|
Submodule.span_eq_span
theorem Submodule.span_eq_span :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
s ⊆ ↑(Submodule.span R t) → t ⊆ ↑(Submodule.span R s) → Submodule.span R s = Submodule.span R t
This theorem states that for any semiring `R` and any additively commutative monoid `M` that forms a module over `R`, given two sets `s` and `t` of elements of `M`, if `s` is a subset of the span of `t` and `t` is a subset of the span of `s`, then the span of `s` is equal to the span of `t`. In other words, if two sets are each contained within the smallest subspace generated by the other, then the subspaces they generate are identical.
More concisely: If `R` is a semiring, `M` is an additively commutative `R`-module, and `s` and `t` are subsets of `M` such that `s` is contained in the span of `t` and `t` is contained in the span of `s`, then the span of `s` equals the span of `t`.
|
LinearMap.span_preimage_le
theorem LinearMap.span_preimage_le :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M₂),
Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)
This theorem, `LinearMap.span_preimage_le`, states that for any semiring `R`, additional semiring `R₂`, add-commutative monoid `M`, additional add-commutative monoid `M₂`, given a semilinear map `f` of type `F` from `M` to `M₂` where `F` is a function-like structure from `M` to `M₂`, and a set `s` in `M₂`, the span of the preimage of `s` under `f` over `R` is a submodule that is less than or equal to the comap of `f` over the span of `s` over `R₂`. In mathematical terms, it could be written as $span_R(f^{-1}(s)) \leq comap_f(span_{R₂}(s))$. Here, 'span' refers to the smallest submodule that contains a set, 'preimage' refers to the set of all elements which map to `s` under `f`, while 'comap' refers to the inverse image of a function on submodules.
More concisely: For any semilinear map `f` from an add-commutative monoid `M` to another add-commutative monoid `M₂` over a semiring `R`, the submodule generated by the preimage of a set `s` in `M₂` under `f` is less than or equal to the image under `f` of the submodule generated by `s` in `M₂` over `R`.
|
Submodule.covBy_span_singleton_sup
theorem Submodule.covBy_span_singleton_sup :
∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V}
{p : Submodule K V}, x ∉ p → p ⋖ Submodule.span K {x} ⊔ p
This theorem states that for any division ring 'K' and for any additive commutative group 'V' that is also a module over 'K', and for any element 'x' of 'V' and any submodule 'p' of 'V', if 'x' is not in 'p', then 'p' is covered by the subspace generated by 'x' and joined with 'p'. In other words, there is no vector subspace that sits strictly between 'p' and the subspace formed by the span of 'x' and 'p'. Here, `⊔` denotes the join operation, which forms the smallest subspace containing two given subspaces, and `⋖` denotes the "covered by" relation.
More concisely: For any division ring K, additive commutative group V as a K-module, element x in V, and submodule p of V, if x not in p then p is covered by the subspace generated by x and p (denoted as the join of x.span and p).
|
Mathlib.LinearAlgebra.Span._auxLemma.11
theorem Mathlib.LinearAlgebra.Span._auxLemma.11 :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
(x ∈ Submodule.span R {y}) = ∃ a, a • y = x
This theorem states that for all types `R` and `M`, where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a module over `R`, and for all elements `x` and `y` of `M`, `x` is in the submodule spanned by the singleton set `{y}` if and only if there exists a scalar `a` from `R` such that `x` is equal to the scalar multiplication `a • y`.
More concisely: For any semiring R, additive commutative monoid M (an R-module), and elements x, y in M, x lies in the submodule generated by {y} if and only if there exists an scalar a in R such that x = a • y.
|
Submodule.closure_induction'
theorem Submodule.closure_induction' :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
{p : (x : M) → x ∈ Submodule.span R s → Prop},
p 0 ⋯ →
(∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) →
(∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) → ∀ {x : M} (hx : x ∈ Submodule.span R s), p x hx
The theorem `Submodule.closure_induction'` is a generalization (dependent version) of `Submodule.closure_induction`. It states that for any semiring `R`, any additively commutative monoid `M`, any `R`-module structure on `M`, any set `s` of members of `M`, and any predicate `p` that maps elements `x` of `M` in the span of `s` to propositions, if `p` holds for the zero element, and if `p` holds for any `x` and `y` in the span of `s` then it holds for their sum, and if `p` holds for any scalar multiple `r • x` of any element `x` in `s`, then `p` holds for all elements in the span of `s`. Here, the span of a set `s` is the smallest submodule of `M` that contains `s`. The scalar multiplication `r • x` denotes the result of action of `r` on `x` under the module structure.
More concisely: If `p` is a predicate on an `R`-module `M` that satisfies `p(0)` and `p(x + y)` for all `x, y` in the span of a set `s` and `p(r • x)` for all scalars `r` in `R` and `x` in `s`, then `p` holds for all elements in the span of `s`.
|
LinearMap.ext_on_range
theorem LinearMap.ext_on_range :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {F : Type u_8}
{σ₁₂ : R →+* R₂} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {ι : Sort u_9} {v : ι → M}
{f g : F}, Submodule.span R (Set.range v) = ⊤ → (∀ (i : ι), f (v i) = g (v i)) → f = g
This theorem states that if we have a function `v` from some set `ι` to a module `M` over a semiring `R`, such that the span of the range of `v` generates the whole module, and two linear maps `f` and `g` from `M` to another module `M₂` over another semiring `R₂`, if `f` and `g` agree on the image of each element of `ι` under `v`, then `f` and `g` are identical. In plain words, if two linear maps agree on a set of vectors that generate the whole module, then these two linear maps are the same.
More concisely: If `v : ι → M` is a function whose range generates `M` over semiring `R`, and `f, g : M → M₂` are linear maps agreeing on the image of `v`, then `f = g`.
|
Submodule.span_subset_span
theorem Submodule.span_subset_span :
∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)
The theorem `Submodule.span_subset_span` asserts that for any types `R`, `M`, and `S` where `R` is a semiring, `M` is an additive commutative monoid and a module over `R`, `S` is a semiring, a module over `M`, and forms a scalar tower with `R` and `M`, and given a set `s` of `M`, the span of `s` over `R` is a subset of the span of `s` over `S`. In other words, when we form submodules by taking the spans of the same set `s` under two different scalars `R` and `S` with `S` being a scalar extension of `R`, the span formed by `R` is always contained within the span formed by `S`.
More concisely: For any semiring `R`, additive commutative monoid and `R`-module `M`, semiring `S` that forms a scalar tower with `R` and `M`, and set `s` of `M`, the span of `s` over `R` is contained in the span of `s` over `S`.
|
Submodule.closure_induction
theorem Submodule.closure_induction :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
{s : Set M} {p : M → Prop},
x ∈ Submodule.span R s → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (r : R), ∀ x ∈ s, p (r • x)) → p x
The theorem `Submodule.closure_induction` states that for any semiring `R`, additive commutative monoid `M` and `M` is a module over `R`, and for any set `s` of elements from `M` and a property `p` applicable to elements of `M`, if an element `x` of `M` is in the span of the set `s`, and if the property `p` holds for the 0 element, and if `p` is preserved under addition (i.e., if `p` holds for `x` and `y` then `p` also holds for `x + y`), and if for all scalars `r` from `R` and all `x` in `s`, `p` holds for `r • x`, then `p` holds for `x`. To put it more intuitively, the theorem allows us to verify a property for all elements in the span of a given set `s` by checking this property for the 0 element, checking its preservation under addition, and checking its validity for all scalar multiples of elements from `s`.
More concisely: If a property `p` holds for the 0 element of an `R`-module `M`, is preserved under addition, and holds for all scalar multiples of elements in a set `s` of `M`, then `p` holds for every element in the span of `s`.
|
Submodule.span_insert_eq_span
theorem Submodule.span_insert_eq_span :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
{s : Set M}, x ∈ Submodule.span R s → Submodule.span R (insert x s) = Submodule.span R s
This theorem, `Submodule.span_insert_eq_span`, states that for any semiring `R`, any commutative add monoid `M` and any module `M` over `R`, if an element `x` of `M` is already in the span of a set `s` in `M`, then the span of the set obtained by inserting `x` into `s` is the same as the span of `s`. In other words, if `x` is a linear combination of elements in `s`, then adding `x` to `s` does not change its span in the module.
More concisely: If `x` is in the span of a set `s` in a module `M` over a semiring `R`, then the span of `s ∪ {x}` equals the span of `s`.
|
Submodule.mem_span_singleton_self
theorem Submodule.mem_span_singleton_self :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
x ∈ Submodule.span R {x}
This theorem states that for any semiring `R`, any additive commutative monoid `M`, and any module structure on `M` over `R`, any element `x` of `M` is contained in the submodule of `M` generated by the singleton set that consists only of `x`. In mathematical terms, if you have a semiring `R` and an `R`-module `M`, then any element in `M` is always included in the span of the set containing only that element.
More concisely: For any semiring R, additive commutative monoid M with an R-module structure, and any x in M, the submodule of M generated by {x} contains x.
|
Submodule.iSup_induction'
theorem Submodule.iSup_induction' :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
(p : ι → Submodule R M) {C : (x : M) → x ∈ ⨆ i, p i → Prop},
(∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯) →
C 0 ⋯ →
(∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯) →
∀ {x : M} (hx : x ∈ ⨆ i, p i), C x hx
This theorem, `Submodule.iSup_induction'`, is a dependent version of `submodule.iSup_induction` in the context of module theory. It states that for every family of submodules `(p : ι → Submodule R M)` of a module `M` over a semiring `R`, and a property `C` that depends on an element `x` and the proof that `x` is in the supremum of the family of submodules, if `C` holds for every element in each submodule, `C` holds for `0`, and `C` is preserved under addition, then `C` holds for every element in the supremum of the family of submodules.
More concisely: Given a semiring R, a module M, a family of submodules p : ι -> Submodule R M, and a property C that depends on an element x and its membership in the supremum of the family, if C holds for every x in each submodule, C holds for 0, and C is closed under addition, then C holds for every x in the supremum of the family.
|
Submodule.subset_span
theorem Submodule.subset_span :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
s ⊆ ↑(Submodule.span R s)
This theorem states that for any semiring `R` and an additively commutative monoid `M` that forms a module over `R`, and for any set `s` of elements of `M`, the set `s` is a subset of the span of `s`. In mathematical terms, this theorem asserts that each element of the set `s` is contained within the smallest submodule of `M` that contains all elements of `s`. This is a fundamental property that defines the concept of a span in the context of module theory.
More concisely: For any semiring `R`, additively commutative `R`-module `M`, and set `s` of elements in `M`, the span of `s` contains `s`.
|
Submodule.span_singleton_le_iff_mem
theorem Submodule.span_singleton_le_iff_mem :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
(p : Submodule R M), Submodule.span R {m} ≤ p ↔ m ∈ p
This theorem states that for any semiring `R`, additive commutative monoid `M`, module `M` over `R`, element `m` of `M` and submodule `p` of `M`, the span of the singleton set `{m}` is a subset of the submodule `p` if and only if the element `m` is in the submodule `p`. In other words, it's saying that in this context, a submodule contains the span of a single element if and only if it contains that element itself.
More concisely: For any semiring R, additive commutative monoid M with R-module structure, and submodule p of M, the singleton set {m} spans p if and only if m is an element of p.
|
Submodule.span_singleton_eq_bot
theorem Submodule.span_singleton_eq_bot :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
Submodule.span R {x} = ⊥ ↔ x = 0
The theorem `Submodule.span_singleton_eq_bot` states that for any type `R` with a semiring structure, any type `M` with an additive commutative monoid structure and a module structure over `R`, and any element `x` of type `M`, the span of the singleton set containing `x` (which is the smallest submodule of `M` that contains the set `{x}`) is equal to the bottom element (or zero submodule) if and only if `x` equals to zero. This means that the only way for a singleton set to span a trivial submodule (one that contains only the zero element) is if the singleton set itself only contains the zero element.
More concisely: The span of a singleton set in an `R`-module `M` is the zero submodule if and only if the element in the set is the zero element of `M`.
|
Submodule.wcovBy_span_singleton_sup
theorem Submodule.wcovBy_span_singleton_sup :
∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (x : V)
(p : Submodule K V), p ⩿ Submodule.span K {x} ⊔ p
This theorem states that for any division ring `K`, add commutative group `V`, and module `K V`, given any vector `x` from `V` and any submodule `p` of `K V`, there is no vector subspace that is properly between `p` and the subspace generated by the union of `p` and the singleton set `{x}`. This is referred to as the weak cover (notated as `⩿`) by the span of the singleton set `{x}` and `p`.
More concisely: Given any division ring `K`, commutative additive group `V`, and `K`-module `V`, for any submodule `p` of `K V` and vector `x` in `V`, there does not exist any proper subspace of `K V` that contains both `p` and `x`, and is contained in the span of `p` and `{x}`.
|
Submodule.span_eq_of_le
theorem Submodule.span_eq_of_le :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M) {s : Set M}, s ⊆ ↑p → p ≤ Submodule.span R s → Submodule.span R s = p
This theorem states that for any given semiring `R`, additive commutative monoid `M` and a module `M` over `R`, if we have a submodule `p` of `M` and a set `s` of `M` such that `s` is a subset of `p` and `p` is less than or equal to the span of `s`, then the span of `s` is equal to `p`. In other words, if a submodule `p` contains a set `s` and is also contained within the span of `s`, then `p` is precisely the span of `s`. This defines an essential property of the span of a set in the context of module theory.
More concisely: If `p` is a submodule of an `R`-module `M` containing a set `s` such that `p` is contained in the span of `s`, then `p` equals the span of `s`.
|
Submodule.singleton_span_isCompactElement
theorem Submodule.singleton_span_isCompactElement :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
CompleteLattice.IsCompactElement (Submodule.span R {x})
This theorem states that for any semiring `R` and commutative additive monoid `M` that forms a module over `R`, and for any element `x` in `M`, the span of the singleton set `{x}` forms a compact element in the complete lattice of submodules of `M`. In other words, if any set of submodules of `M` has a supremum above the singleton span of `x`, then there exists a finite subset of this set whose supremum is also above the singleton span of `x`.
More concisely: Given a commutative additive monoid `M` over a semiring `R` with `{x} ⊆ M` being a generating set for a submodule, the span of `{x}` is compact in the lattice of submodules of `M`, i.e., any upward-closed set of submodules containing the span of `{x}` has a finite supremum above it.
|
Submodule.span_insert
theorem Submodule.span_insert :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M)
(s : Set M), Submodule.span R (insert x s) = Submodule.span R {x} ⊔ Submodule.span R s
This theorem states that for any semiring `R`, an additively commutative monoid `M` and any `R`-module `M`, for any `x` in `M` and any set `s` of `M`, the span of the set obtained by inserting `x` into `s` is equal to the sup (i.e., least upper bound) of the span of the set `{x}` and the span of `s`. In other words, the smallest submodule of `M` that contains both `x` and `s` is the least upper bound of the smallest submodule containing `x` and the smallest submodule containing `s`.
More concisely: For any semiring `R`, an additively commutative monoid `M`, and `R`-module `M`, the span of `{x}` together with the span of a set `s` in `M` is equal to the span of `x` union `s`. (Here, the span of a set is the submodule it generates.)
|
Submodule.not_mem_span_of_apply_not_mem_span_image
theorem Submodule.not_mem_span_of_apply_not_mem_span_image :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] [inst_8 : RingHomSurjective σ₁₂]
(f : F) {x : M} {s : Set M}, f x ∉ Submodule.span R₂ (⇑f '' s) → x ∉ Submodule.span R s
This theorem states that given two semirings `R` and `R₂`, two additive commutative monoids `M` and `M₂` which are also modules over `R` and `R₂` respectively, a morphism `σ₁₂` from `R` to `R₂`, a function `f` that is FunLike from `M` to `M₂`, and a set `s` of elements from `M`, if the image of an element `x` from `M` under `f` does not belong to the span of the image of `s` under `f` in `M₂` over `R₂`, then `x` itself does not belong to the span of `s` in `M` over `R`. This theorem is useful for reasoning about the relationship between elements and their images under a function in the context of modules and their spans.
More concisely: If `f` is a morphism of modules from the additive commutative semigroup `(M, +, R)` to `(M₂, +, R₂)`, `σ₁₂ : R ⟶ R₂`, and `s ⊆ M` such that the image of each `x ∈ s` under `f` is not in the span of `s` over `R₂`, then `x ∉ span(s)` in `M` over `R`.
|
Submodule.mem_span_finite_of_mem_span
theorem Submodule.mem_span_finite_of_mem_span :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M}
{x : M}, x ∈ Submodule.span R S → ∃ T, ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T
The theorem `Submodule.mem_span_finite_of_mem_span` states that for any given Ring `R`, an additive commutative monoid `M`, and a module structure over `M` with `R` as the ring, if we have a set `S` of elements from `M`, and an element `x` of `M` that lies in the span of the set `S`, then there exists a finite subset `T` of `S` such that `x` is in the span of `T`. In other words, any element in the span of a set can be expressed as a linear combination of a finite number of elements of the set.
More concisely: If `R` is a ring, `M` an additive commutative monoid with an `R`-module structure, `S ⊆ M`, and `x ∈ span S`, then there exists a finite subset `T ⊆ S` such that `x ∈ span T`.
|
Submodule.coe_scott_continuous
theorem Submodule.coe_scott_continuous :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
OmegaCompletePartialOrder.Continuous' SetLike.coe
The theorem `Submodule.coe_scott_continuous` states that for any semiring `R` and additive commutative monoid `M` that is a module over `R`, the function `coe` (coercion function) from the set-like type `Submodule R M` to `Set M` is Scott continuous with respect to the ω-complete partial order induced by the complete lattice structures. Scott continuity implies that the function `coe` is monotone and preserves directed suprema, which means that it preserves the order and joins of elements in the set-like structure.
More concisely: The coercion function from the type of submodules of a module over a semiring to the set of its elements is Scott continuous with respect to the induced ω-complete partial order.
|
Submodule.span_union
theorem Submodule.span_union :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s t : Set M),
Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t
The theorem `Submodule.span_union` states that for any semiring `R` and an additive commutative monoid `M` over which `R` is a module, and for any two sets `s` and `t` of elements in `M`, the span of the union of `s` and `t` is equal to the sup (join) of the span of `s` and the span of `t`. In other words, the smallest submodule of `M` that contains all elements of either `s` or `t` is the same as the smallest submodule that contains both the smallest submodule for `s` and the smallest submodule for `t`.
More concisely: The submodule generated by the union of two sets in an additive commutative monoid over a semiring is equal to the sum of the submodules generated by each set.
|
Submodule.span_smul_eq_of_isUnit
theorem Submodule.span_smul_eq_of_isUnit :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
(r : R), IsUnit r → Submodule.span R (r • s) = Submodule.span R s
This theorem, `Submodule.span_smul_eq_of_isUnit`, states that for any semiring `R`, additive commutative monoid `M`, set of `M` elements `s`, and element `r` of `R` that is a unit (an element with a two-sided inverse), the span of the set resulting from the scalar multiplication of `r` and `s` (denoted `r • s`) is equal to the span of `s`. In other words, scalar multiplication by a unit element in a semiring does not change the span of a set in a module over that semiring. This theorem is a more specific version of `Submodule.span_smul_eq`, which holds for arbitrary `r` in a commutative semiring.
More concisely: For any semiring `R`, additive commutative monoid `M`, unit `r` in `R`, and set `s` of `M`, the span of `r • s` is equal to the span of `s`.
|
Submodule.span_image
theorem Submodule.span_image :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {s : Set M}
[inst_8 : RingHomSurjective σ₁₂] (f : F), Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
This theorem, `Submodule.span_image`, states that for any semiring `R`, any semiring `R₂`, any additively commutative monoid `M`, any additively commutative monoid `M₂`, any module structure over `M` relative to `R`, any module structure over `M₂` relative to `R₂`, any ring homomorphism `σ₁₂` from `R` to `R₂`, any function `F` from `M` to `M₂` that behaves like a linear map respecting the semiring homomorphism `σ₁₂`, and any set of elements `s` in `M`, the span (the smallest submodule that contains `s`) in `M₂` of the image of `s` under the function `F` is equal to the image under `F` of the span of `s` in `M`. This is under the condition that the ring homomorphism `σ₁₂` is surjective. In simpler terms, this theorem describes a property of how linear mapping between two modules interacts with the process of taking spans of sets in those modules.
More concisely: Given a surjective ring homomorphism `σ₁₂` from semiring `R` to `R₂`, for any module `M` over `R`, `M₂` over `R₂`, and any function `F : M -> M₂` that respects the module structures and the semiring homomorphism, the span of `F(s)` in `M₂` equals the image of the span of `s` in `M`.
|
Submodule.comap_map_eq
theorem Submodule.comap_map_eq :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} [inst_6 : RingHomSurjective τ₁₂] {F : Type u_8} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F τ₁₂ M M₂] (f : F) (p : Submodule R M),
Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.ker f
The theorem `Submodule.comap_map_eq` asserts that for any semirings `R` and `R₂`, any commutative additive groups `M` and `M₂`, a module `M` over `R`, a module `M₂` over `R₂`, a surjective ring homomorphism `τ₁₂` from `R` to `R₂`, a function `f` which is a semilinear map from `M` to `M₂` with respect to `τ₁₂`, and a submodule `p` of `M`, the preimage under `f` of the image under `f` of `p` is equal to the join of `p` and the kernel of `f`. Here, the preimage is computed via the `Submodule.comap` function, the image via the `Submodule.map` function, and the join via the `⊔` operation. In other words, it describes how mapping and then comapping a submodule with a semilinear map corresponds to enlarging the original submodule by the kernel of the map.
More concisely: For any semirings R and R₂, commutative additive groups M and M₂, a module M over R, a module M₂ over R₂, a surjective ring homomorphism τ₁₂ from R to R₂, a semilinear map f from M to M₂ with respect to τ₁₂, and a submodule p of M, the preimage of the image of p under f, as computed by `Submodule.comap` and `Submodule.map`, equals the join of p and the kernel of f.
|
Submodule.mem_iSup_of_directed
theorem Submodule.mem_iSup_of_directed :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
[inst_3 : Nonempty ι] (S : ι → Submodule R M),
Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ iSup S ↔ ∃ i, x ∈ S i
This theorem states that for any semiring `R`, an additive commutative monoid `M`, a module structure on `M` over `R`, and an indexed family `S` of submodules of `M` over `R` that is directed with respect to the inclusion relation (i.e., for any two submodules in the family, there is another submodule in the family that contains both), a module element `x` belongs to the indexed supremum of the family `S` if and only if there exists an index `i` such that `x` belongs to the submodule `S i`.
More concisely: For any semiring `R`, an additive commutative monoid `M` with an `R`-module structure, and an indexed family `S` of `R`-submodules of `M` directed by inclusion, an element `x` of `M` lies in the supremum of `S` if and only if it belongs to some submodule in `S`.
|
Mathlib.LinearAlgebra.Span._auxLemma.18
theorem Mathlib.LinearAlgebra.Span._auxLemma.18 :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
(p : Submodule R M), (Submodule.span R {m} ≤ p) = (m ∈ p)
This theorem, named `Mathlib.LinearAlgebra.Span._auxLemma.18`, states that for any semiring `R`, any additive commutative monoid `M`, any `R`-module structure on `M`, any element `m` of `M`, and any submodule `p` of `M`, the span of the set containing only `m` is a subset of `p` if and only if `m` is an element of `p`. In other words, the smallest submodule of `M` that contains `m` is contained in `p` exactly when `m` itself is contained in `p`.
More concisely: The smallest R-submodule of an additive commutative monoid M that contains an element m is equal to M if and only if m is an element of the given submodule p.
|
Submodule.span_eq
theorem Submodule.span_eq :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), Submodule.span R ↑p = p
The theorem `Submodule.span_eq` states that for any semiring `R`, any commutative additive monoid `M`, and any module `M` over `R`, for any submodule `p` of `M`, the span of the set of elements in `p` (denoted as `Submodule.span R ↑p`) is equal to `p` itself. In other words, the smallest submodule that contains all elements of `p` is `p`.
More concisely: For any semiring `R`, commutative additive monoid `M`, and module `M` over `R`, the submodule generated by a submodule `p` of `M` (denoted as `Submodule.span R p`) equals `p` itself.
|
LinearMap.eqOn_span
theorem LinearMap.eqOn_span :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {F : Type u_8}
{σ₁₂ : R →+* R₂} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F},
Set.EqOn (⇑f) (⇑g) s → ∀ ⦃x : M⦄, x ∈ Submodule.span R s → f x = g x
This theorem states that if two linear maps, `f` and `g`, are equal on a set `s`, then they are also equal on the span of `s`. More formally, for any two linear maps `f` and `g` between modules `M` and `M₂` over semirings `R` and `R₂`, respectively, if two maps are equal for all elements of a set `s`, i.e., `Set.EqOn (⇑f) (⇑g) s` holds, then they are also equal for all elements `x` in the submodule spanned by `s`, i.e., `x ∈ Submodule.span R s` implies `f x = g x`. This theorem is essentially about the extension of equality of two linear maps from a set to its linear span.
More concisely: If two linear maps are equal on a set, they are equal on the submodule spanned by that set.
|
Submodule.span_eq_iSup_of_singleton_spans
theorem Submodule.span_eq_iSup_of_singleton_spans :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}
This theorem states that for any given set `s` of a type `M` that is a module over a semiring `R`, the span of `s` (i.e., the smallest submodule of `M` that contains `s`) is equivalent to the supremum of the spans of all singleton sets that contain elements of `s`. In other words, the smallest submodule that contains all elements of `s` is the same as the "largest" submodule that can be generated by taking the span of each individual element of `s` separately.
More concisely: The span of a set `s` in a module `M` over a semiring `R` is equal to the sum of the spans of all singleton sets contained in `s`.
|
Submodule.span_induction'
theorem Submodule.span_induction' :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
{p : (x : M) → x ∈ Submodule.span R s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
p 0 ⋯ →
(∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s),
p x hx → p y hy → p (x + y) ⋯) →
(∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯) →
∀ {x : M} (hx : x ∈ Submodule.span R s), p x hx
This theorem, named `Submodule.span_induction'`, is a dependent version of `Submodule.span_induction` theorem. It states that for all semirings `R`, all additive commutative monoids `M`, and for every submodule `s` of `M` over `R`, if a property `p` holds for all elements `x` in `s`, and `p` holds for the zero element, and `p` is preserved under addition and scalar multiplication in the span of `s`, then `p` holds for all elements in the span of `s`. More formally, if for all `x` and `y` in the span of `s`, `p` holds for `x` and `y`, then `p` also holds for the sum of `x` and `y`; and if `p` holds for an element `x` in the span of `s`, then `p` also holds for any scalar multiple `a • x` of `x`.
More concisely: If a property holds for all elements in a submodule and for the zero element, and is closed under addition and scalar multiplication, then it holds for all elements in the span of the submodule.
|
Submodule.span_mono
theorem Submodule.span_mono :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
s ⊆ t → Submodule.span R s ≤ Submodule.span R t
The theorem `Submodule.span_mono` states that for any semiring `R` and additive commutative monoid `M` which is a module over `R`, and for any two sets `s` and `t` of elements of `M`, if set `s` is a subset of set `t`, then the span of set `s` is a submodule of the span of set `t`. In other words, if every element of `s` is also an element of `t`, then every linear combination of elements of `s` is also a linear combination of elements of `t`.
More concisely: If `s` is a subset of `t` in an additive commutative `R`-module `M`, then the span of `s` is contained in the span of `t`.
|
Submodule.span_le_restrictScalars
theorem Submodule.span_le_restrictScalars :
∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
Submodule.span R s ≤ Submodule.restrictScalars R (Submodule.span S s)
The theorem `Submodule.span_le_restrictScalars` states that for any set `s` of elements in a module `M` over a semiring `R`, and for a larger semiring `S` that acts on the same module `M`, the submodule spanned by `s` with coefficients in `R` is a subset of the submodule spanned by `s` with coefficients in `S`, restricted to `R`. This implies that if `R` is a "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. The theorem relies on the condition that `R` is a scalar tower over `S` and `M`, which means that scalar multiplication in `M` by elements of `R` can be computed via scalar multiplication in `S`.
More concisely: For any set `s` of elements in a module `M` over a semiring `R`, the submodule of `M` spanned by `s` with coefficients in `R` is contained in the submodule spanned by `s` with coefficients in a larger semiring `S`, when `R` is a scalar tower over `S` and `M`.
|
Submodule.prod_top
theorem Submodule.prod_top :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_9}
[inst_3 : AddCommMonoid M'] [inst_4 : Module R M'], ⊤.prod ⊤ = ⊤
This theorem states that for any semiring `R`, additive commutative monoid `M`, and module `R M`, as well as any additional additive commutative monoid `M'` and module `R M'`, the product of the top submodule (i.e., the whole module) with itself is again the top submodule. In terms of algebra, this theorem is saying that the product of the entire module with itself is still the entire module, reflecting the closure property of a module over its ring of scalars.
More concisely: For any semiring `R`, additive commutative monoids `M` and `M'`, and `R`-modules `M` and `M'`, the top submodule of `M` is closed under the product operation with `M`, i.e., `⊤ M ⊤ M = ⊤ M`.
|
LinearMap.eqOn_span'
theorem LinearMap.eqOn_span' :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {F : Type u_8}
{σ₁₂ : R →+* R₂} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Submodule.span R s)
The theorem `LinearMap.eqOn_span'` states that if two linear maps, represented by `f` and `g`, are functionally equal over a set `s`, then they are also functionally equal over the span of set `s`. Here, the functional equality over a set, given by `Set.EqOn` definition, means that for any element `x` belonging to the set, the image of `x` under both functions `f` and `g` is the same. The span of a set `s`, represented by `Submodule.span R s`, is the smallest submodule that contains `s`. This theorem is applicable under the context where `R` is a semiring, `M` and `M₂` are additive commutative monoids, `R` and `M` form a module, `R₂` is a semiring, `M₂` is an additive commutative monoid, `R₂` and `M₂` form a module, and `F` is a function-like structure from `M` to `M₂`.
More concisely: If two linear maps between modules are equal on a set, they are equal on the span of that set.
|
Submodule.prod_bot
theorem Submodule.prod_bot :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_9}
[inst_3 : AddCommMonoid M'] [inst_4 : Module R M'], ⊥.prod ⊥ = ⊥
This theorem states that for any semiring `R`, add-commutative monoid `M` and `M'` (which are also `R`-modules), the product of the bottom element (`⊥`, representing the zero submodule) of `M` and `M'` is equal to the bottom element of the direct product module. In other words, in the context of modules over a semiring, the product of the zero submodule with itself is again the zero submodule.
More concisely: For any semiring `R`, any add-commutative `R`-modules `M` and `M'`, the bottom element of `M ⊥ M'` equals the product of the bottom element of `M` and the bottom element of `M'`.
|
Submodule.span_span_of_tower
theorem Submodule.span_span_of_tower :
∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
Submodule.span S ↑(Submodule.span R s) = Submodule.span S s
The theorem `Submodule.span_span_of_tower` states that for any semiring `R`, additively commutative monoid `M`, and semiring `S`, if `s` is a set of `M`, and there exists scalar multiplication between `R` and `S`, and `M` is a module over `S`, and an additional condition of scalar tower between `R`, `S`, and `M` is satisfied, then the span of the span of `s` by `R` under `S` is equal to the span of `s` by `S` only. In other words, taking the span of a set `s` with a larger ring `S` of the span by a smaller ring `R` results in the exact same set as taking the span with just the larger ring `S`. The condition of scalar tower ensures that the multiplication between the elements from the rings and the set is associated correctly.
More concisely: For any semiring `R`, additively commutative monoid `M`, and semiring `S` with scalar multiplication, if `s` is a set of `M` and `M` is a module over `S` with the scalar tower property between `R`, `S`, and `M`, then the span of `s` by `S` under `R` equals the span of `s` by `S`.
|
Submodule.span_induction
theorem Submodule.span_induction :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
{s : Set M} {p : M → Prop},
x ∈ Submodule.span R s →
(∀ x ∈ s, p x) → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (a : R) (x : M), p x → p (a • x)) → p x
This theorem, `Submodule.span_induction`, provides an induction principle for elements belonging to the span of a set in a module. More specifically, it states that if a property `p` holds for the zero element and all elements of a set `s` in a module `M` over a semiring `R`, and `p` is preserved under both addition and scalar multiplication, then `p` holds for all elements in the span of `s`. This induction principle is a crucial tool for making arguments about all elements of a spanned set in a module, typically in a linear algebraic context.
More concisely: If a property holds for the zero element and is closed under addition and scalar multiplication for every element in a set in a module, then it holds for all elements in the span of that set.
|
Submodule.span_empty
theorem Submodule.span_empty :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Submodule.span R ∅ = ⊥
The theorem `Submodule.span_empty` states that for any semiring `R` and any type `M` which is an additive commutative monoid and also a module over `R`, the span of the empty set is the bottom element of the lattice of submodules of `M`. This means the smallest submodule of `M` that contains no elements is the bottom submodule, typically the zero submodule.
More concisely: The empty set generates the zero submodule in any additive commutative monoid and R-module.
|
Submodule.iSup_induction
theorem Submodule.iSup_induction :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
(p : ι → Submodule R M) {C : M → Prop} {x : M},
x ∈ ⨆ i, p i → (∀ (i : ι), ∀ x ∈ p i, C x) → C 0 → (∀ (x y : M), C x → C y → C (x + y)) → C x
The given theorem is an induction principle for elements belonging to the supremum of the set `p`, where `p` is a function from some sort `ι` to the submodules of a module `M` over a semiring `R`. The theorem states that if a property `C` holds for `0` and for all elements of each submodule `p i` for all indices `i`, and if `C` is preserved under the addition operation, then `C` holds for all elements of the supremum of `p`.
More concisely: If `C(0)` holds and `C` is preserved under addition for all elements in each submodule `p i` of a function `p` from sort `ι` to submodules of module `M` over semiring `R`, then `C` holds for all elements in the supremum of `p`.
|
Submodule.image_span_subset
theorem Submodule.image_span_subset :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M)
(N : Submodule R₂ M₂), ⇑f '' ↑(Submodule.span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N
The theorem `Submodule.image_span_subset` states that for a semiring `R`, another semiring `R₂`, an additive commutative monoid `M`, another additive commutative monoid `M₂`, a module `M` over `R`, another module `M₂` over `R₂`, a ring homomorphism `σ₁₂` from `R` to `R₂`, a function `F` from `M` to `M₂`, a semilinear map `f` from `M` to `M₂` with respect to `σ₁₂`, a set `s` of elements of `M`, and a submodule `N` of `M₂` over `R₂`, the image under `f` of the span of `s` in `M` is a subset of `N` if and only if for all elements `m` in `s`, `f(m)` is an element of `N`. Here, "span" refers to the smallest submodule that contains a given set, and a "semilinear map" is a function that is both additive and satisfies a scalar multiplication condition.
More concisely: The image of the span of a set in a module under a semilinear map is contained in a submodule if and only if each element in the set maps to an element in the submodule.
|
LinearMap.ext_on
theorem LinearMap.ext_on :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {F : Type u_8}
{σ₁₂ : R →+* R₂} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F},
Submodule.span R s = ⊤ → Set.EqOn (⇑f) (⇑g) s → f = g
The theorem `LinearMap.ext_on` states that for any two semilinear maps `f` and `g` from a module `M` over a semiring `R` to a module `M₂` over a semiring `R₂`, if a set `s` generates the whole module `M`, and `f` and `g` are equal on `s`, then `f` and `g` must be identical. This means that a module homomorphism is determined completely by its action on the generating set of the module.
More concisely: If two semilinear maps between modules over semirings agree on a generating set, then they are equal.
|
Mathlib.LinearAlgebra.Span._auxLemma.28
theorem Mathlib.LinearAlgebra.Span._auxLemma.28 :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_9}
[inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {p : Submodule R M} {q : Submodule R M'} {x : M × M'},
(x ∈ p.prod q) = (x.1 ∈ p ∧ x.2 ∈ q)
This theorem states that for any type `R` that is a semiring, `M` and `M'` that are commutative monoids, and `p` and `q` that are submodules over `R` of `M` and `M'` respectively, a given element `x` is in the product of submodules `p` and `q` if and only if the first component of `x` is in `p` and the second component is in `q`. This provides a condition for membership in the product of two submodules in terms of their individual memberships.
More concisely: For any semiring `R`, commutative monoids `M` and `M'`, and submodules `p` of `M` and `q` of `M'`, an element `x` of `M x M'` (the cartesian product of `M` and `M'`) belongs to the product of `p` and `q` if and only if its first component belongs to `p` and its second component belongs to `q`.
|
Submodule.mem_span_singleton
theorem Submodule.mem_span_singleton :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
x ∈ Submodule.span R {y} ↔ ∃ a, a • y = x
This theorem, `Submodule.mem_span_singleton`, states that for any semiring `R` and any additive commutative monoid `M` that is also an `R`-module, and for any two elements `x` and `y` of `M`, the element `x` is in the submodule spanned by the singleton set `{y}` if and only if there exists an element `a` in `R` such that `a` scaled by `y` equals `x`. In other words, `x` is in the span of `{y}` if and only if `x` is a scalar multiple of `y`.
More concisely: For any semiring `R`, additive commutative monoid `M` being an `R`-module, and `x, y` in `M`, `x` belongs to the submodule spanned by `{y}` if and only if there exists `a` in `R` such that `x = a * y`.
|
Submodule.finset_span_isCompactElement
theorem Submodule.finset_span_isCompactElement :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Finset M),
CompleteLattice.IsCompactElement (Submodule.span R ↑S)
This theorem states that the span of a finite subset is a compact element in the lattice of submodules. Here, compactness refers to the property that if the supremum (greatest lower bound) of a set is above the compact element, then there exists a finite subset whose supremum is also above the compact element. In this context, the span of a set `s` in module `M` over the semiring `R` is defined as the smallest submodule of `M` that contains `s`. The theorem implies that for any finite subset `S` of module `M`, the span of `S` possesses this compactness property in the complete lattice structure of submodules of `M`.
More concisely: The span of a finite subset in a module is a compact element in the lattice of submodules.
|
Submodule.span_zero_singleton
theorem Submodule.span_zero_singleton :
∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Submodule.span R {0} = ⊥
This theorem states that for any given semiring `R` and an additive commutative monoid `M` which is also a `R`-module, the span of the singleton set consisting of only the zero element in `M` is the bottom (smallest) submodule. In other words, the smallest submodule of `M` that contains just the zero element is the bottom submodule.
More concisely: For any semiring `R` and additive commutative monoid `M` that is an `R`-module, the zero element's span is the bottom submodule of `M`.
|
Submodule.span_coe_eq_restrictScalars
theorem Submodule.span_coe_eq_restrictScalars :
∀ {R : Type u_1} {M : Type u_4} {S : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M) [inst_3 : Semiring S] [inst_4 : SMul S R] [inst_5 : Module S M]
[inst_6 : IsScalarTower S R M], Submodule.span S ↑p = Submodule.restrictScalars S p
This theorem, named `Submodule.span_coe_eq_restrictScalars`, states that for any semiring `R`, `AddCommMonoid` `M`, and semiring `S` with `M` a module over `R`, given a submodule `p` of `M` over `R`, if `S` acts on `R` by scalar multiplication and `M` is a module over `S`, and there exists a scalar tower between `S`, `R`, and `M`, then the span of the set `p` with coefficients in `S` is equal to the submodule of `M` over `R` restricted to scalars from `S`. In simpler words, it says that the smallest submodule containing `p` when considering `S` as the ring is the same as the original submodule `p` but with the scalar multiplication restricted to `S`.
More concisely: For any semiring `R`, AddCommMonoid `M`, semiring `S`, and submodule `p` of `M` over `R`, if `S` acts on `R` by scalar multiplication, `M` is a module over `S`, and there exists a scalar tower between `S`, `R`, and `M`, then the span of `p` in `M` with coefficients in `S` equals the submodule of `p` over `R` restricted to scalars from `S`.
|
Submodule.span_le
theorem Submodule.span_le :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
{p : Submodule R M}, Submodule.span R s ≤ p ↔ s ⊆ ↑p
The theorem `Submodule.span_le` states that for any semiring `R`, any additively commutative monoid `M`, and any `R`-module structure on `M`, given a set `s` of elements from `M` and a submodule `p` of `M`, the span of the set `s` is a subset of the submodule `p` if and only if the set `s` is a subset of the elements of the submodule `p`. In other words, the smallest submodule of `M` that contains `s` is a subset of `p` precisely when `s` is a subset of `p`.
More concisely: The smallest R-module subgenerated by a set s in an R-module M is contained in a submodule p if and only if s is contained in p.
|
Submodule.span_induction₂
theorem Submodule.span_induction₂ :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
{p : M → M → Prop} {a b : M},
a ∈ Submodule.span R s →
b ∈ Submodule.span R s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (y : M), p 0 y) →
(∀ (x : M), p x 0) →
(∀ (x₁ x₂ y : M), p x₁ y → p x₂ y → p (x₁ + x₂) y) →
(∀ (x y₁ y₂ : M), p x y₁ → p x y₂ → p x (y₁ + y₂)) →
(∀ (r : R) (x y : M), p x y → p (r • x) y) → (∀ (r : R) (x y : M), p x y → p x (r • y)) → p a b
This theorem is an induction principle for membership in a span of a set in a module. Given a semiring `R`, an additive commutative monoid `M`, a module structure over `M` with the semiring `R`, a set `s` of elements from `M`, and a binary predicate `p` over `M`, if two elements `a` and `b` from `M` are in the span of `s`, then, assuming that `p` holds for all pairs of elements in `s`, for the zero of `M` with any element, for any element with the zero of `M`, for sums of elements with any element and for any element with sums of elements, and for scaled versions of any element with any other element, then `p` holds for the pair of elements `a` and `b`. The scaling in the last two conditions are done with elements from the semiring `R`. This theorem can be used to prove properties that hold for all elements in the span of a set, using the properties of those elements in the set and the operations of sum and scaling.
More concisely: Given a semiring `R`, an additive commutative monoid `M` with a module structure over `R`, a set `s` of elements from `M`, and a binary predicate `p`, if `p` holds for all pairs of elements in the span of `s`, then `p` holds for any pair of elements in `M`.
|
Submodule.submodule_eq_sSup_le_nonzero_spans
theorem Submodule.submodule_eq_sSup_le_nonzero_spans :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = Submodule.span R {m}}
This theorem states that for any given submodule `p` of a module `M` over a semiring `R`, `p` is equal to the supremum of the spans of all non-zero elements in `p`. In other words, every submodule is composed by taking the smallest submodules that contain each of its non-zero elements (`Submodule.span R {m}` for each non-zero `m` in `p`), and then taking the supremum of these smaller submodules. Thus, all elements in the original submodule can be expressed as linear combinations of its non-zero elements.
More concisely: A submodule of a module over a semiring is equal to the supremum of the spans of its non-zero elements.
|
Submodule.IsPrincipal.principal
theorem Submodule.IsPrincipal.principal :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(S : Submodule R M) [inst_3 : S.IsPrincipal], ∃ a, S = Submodule.span R {a}
This theorem, named `Submodule.IsPrincipal.principal`, states that for any semiring `R`, any additive commutative monoid `M`, and any module `M` over `R`, if `S` is a principal submodule of this module (i.e., `S` is generated by a single element), then there exists an element `a` such that `S` is equal to the span of the singleton set containing `a`. In other words, every principal submodule of a module is the span of some single element.
More concisely: Every principal submodule of a module over a semiring is generated by a single element.
|
LinearMap.eqOn_span_iff
theorem LinearMap.eqOn_span_iff :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {F : Type u_8}
{σ₁₂ : R →+* R₂} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F},
Set.EqOn ⇑f ⇑g ↑(Submodule.span R s) ↔ Set.EqOn (⇑f) (⇑g) s
This theorem states that for any two linear maps `f` and `g` from a module `M` over a semiring `R` to a module `M₂` over a semiring `R₂`, the two maps are equal on the span of a set `s` (that is, the smallest submodule that contains `s`) if and only if they are equal on `s` itself. Here, equality on a set is defined as the two functions producing the same value for each element in the set. The type of the linear maps `F` is required to have a function-like structure that allows us to treat elements of `F` as functions. Moreover, the linear maps are required to be semilinear, which is a special type of linear map that has a scalar multiplication operation that intertwines with the multiplication operation in the semiring.
More concisely: For any semilinear maps `f` and `g` from a module `M` over a semiring `R` to a module `M₂` over a semiring `R₂`, `f` and `g` agree on the span of a set `s` if and only if they agree on `s` itself.
|
LinearMap.span_singleton_eq_range
theorem LinearMap.span_singleton_eq_range :
∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
Submodule.span R {x} = LinearMap.range (LinearMap.toSpanSingleton R M x)
This theorem declares that for any semiring `R`, any additive commutative monoid `M` and any module `M` over `R`, for any element `x` in `M`, the span of `{x}` in `M` (i.e., the smallest submodule of `M` containing `{x}`) is equal to the range of the linear map `toSpanSingleton x` (i.e., the set of all scalar multiples of `x`). In other words, all scalar multiples of a given element `x` in a module `M` over a semiring `R` precisely form the smallest submodule of `M` that contains `x`.
More concisely: The submodule generated by an element `x` in an `R`-module `M` is equal to the set of all scalar multiples of `x` in `M`, for any semiring `R` and additive commutative monoid `M`.
|
Submodule.mem_span
theorem Submodule.mem_span :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
{s : Set M}, x ∈ Submodule.span R s ↔ ∀ (p : Submodule R M), s ⊆ ↑p → x ∈ p
This theorem states that for any semiring `R` and an additive commutative monoid `M` that is also a module over `R`, a member `x` of type `M` is in the span of a set `s` (of elements of `M`) if and only if for every submodule `p` of `M` over `R`, whenever `s` is a subset of `p`, `x` is an element of `p`. In simple terms, it establishes that an element is in the span of a set if it belongs to every submodule that contains the set.
More concisely: An element of an additive commutative `R`-module is in the span of a set if and only if it belongs to every submodule containing the set.
|
Submodule.finite_span_isCompactElement
theorem Submodule.finite_span_isCompactElement :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Set M),
S.Finite → CompleteLattice.IsCompactElement (Submodule.span R S)
This theorem states that for any given set `S` of elements of type `M`, and given types `R` and `M` where `R` is a semiring and `M` is an additive commutative monoid that also has a module structure over `R`, if `S` is finite, then the span of `S` (which is the smallest submodule of `M` that contains `S`) is a compact element in the complete lattice of submodules of `M`. Here, a compact element of a complete lattice is defined as an element `k` such that for any set with supremum above `k`, there exists a finite subset with supremum also above `k`.
More concisely: Given a finite set `S` of elements in an additive commutative monoid `M` with an `R`-module structure where `R` is a semiring, the span of `S` is a compact element in the lattice of submodules of `M`.
|
LinearMap.map_span
theorem LinearMap.map_span :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
{F : Type u_8} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] [inst_8 : RingHomSurjective σ₁₂]
(f : F) (s : Set M), Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
The theorem `LinearMap.map_span` states that for any semiring `R`, additively commutative monoid `M`, module `M` over `R`, semiring `R₂`, a function `f` of type `F` that behaves like a function from `M` to `M₂`, and a set `s` of elements of `M`, the result of applying the function `f` to the span of `s` in `R` is equal to the span in `R₂` of the image of `s` under `f`. This is under the conditions that `F` is a type that behaves like a function from `M` to `M₂`, `f` is a semilinear map, and the ring homomorphism from `R` to `R₂` is surjective. Essentially, it asserts the preservation of the span of a set under a linear map.
More concisely: For any semiring `R`, additively commutative monoid `M` with an `R`-module structure, semiring `R₂`, a surjective ring homomorphism from `R` to `R₂`, a semilinear function `f : M →ₗ[R] M₂`, and a set `s ⊆ M`, the image of the span of `s` under `f` is equal to the span of the image of `s` in `R₂`.
|