Submodule.smul_bot'
theorem Submodule.smul_bot' :
∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α), a • ⊥ = ⊥
The theorem `Submodule.smul_bot'` states that for any type `α` which forms a monoid, a type `R` which forms a semiring, and a type `M` which is a module over `R` and also an additive commutative monoid, if `α` has a distributive multiplication action on `M` and the scalar multiplication is commutative, then scalar multiplication of the bottom submodule (`⊥`) by any element `a` of `α` results in the bottom submodule (`⊥`). In other words, multiplying the zero or base element of the module by any scalar results in the zero element.
More concisely: For any monoid `α`, semiring `R`, additive commutative monoid and `R`-module `M`, if `α` distributively acts on `M` and scalar multiplication is commutative, then `a⊥ = ⊥` for all `a ∈ α`, where `⊥` denotes the bottom element of `M`.
|
Submodule.smul_sup'
theorem Submodule.smul_sup' :
∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (S T : Submodule R M),
a • (S ⊔ T) = a • S ⊔ a • T
This theorem, `Submodule.smul_sup'`, states that for any semiring `R`, additive commutative monoid `M`, monoid `α`, a distributive multiplication action of `α` on `M`, and a scalar multiplication commutative class of `α`, `R`, and `M`, for any element `a` of `α`, and any two submodules `S` and `T` of `M`, the scalar multiplication of `a` with the superset (join) of `S` and `T` equals the superset of the scalar multiplication of `a` with `S` and the scalar multiplication of `a` with `T`. In other words, it says that scalar multiplication distributes over the superset operation for submodules.
More concisely: For any semiring `R`, additive commutative monoid `M`, monoid `α`, distributive multiplication action of `α` on `M`, and a scalar multiplication commutative class of `α`, `R`, and `M`, for all `a ∈ α` and submodules `S`, `T` of `M`, we have `a * (S ⊎ T) = a * S ⊎ a * T`.
|
Submodule.set_smul_eq_of_le
theorem Submodule.set_smul_eq_of_le :
∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] {S : Type u_4} [inst_1 : Monoid S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : DistribMulAction S M] (s : Set S) (N p : Submodule R M),
(∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → p ≤ s • N → s • N = p
The theorem `Submodule.set_smul_eq_of_le` states that for any types `R`, `M`, and `S`, given a semiring structure on `R`, a monoid structure on `S`, an additive commutative monoid structure on `M`, a module structure of `R` over `M`, a distributive multiplication action of `S` on `M`, a set `s` of type `S`, and two submodules `N` and `p` of `M`, if for every element `r` of `s` and every element `n` of `N`, the scalar multiplication `r • n` belongs to `p`, and if `p` is a subset of the scalar multiplication set `s • N`, then `s • N` is equal to `p`.
In simpler terms, this theorem is about the relationship between three mathematical structures - a set and two submodules - under certain operations. If all elements from the set and one submodule, when multiplied, result in an element of the other submodule, and this other submodule is a subset of the set scaled by the first submodule, then the set scaled by the first submodule is the other submodule.
More concisely: If a set `s` of a semiring `R`, acting distributively on an additive commutative monoid `M` with a module structure over `R`, maps every element of a submodule `N` to another submodule `p`, and `p` is contained in the submodule generated by `s` and `N`, then `s • N = p`.
|
Submodule.mem_set_smul_def
theorem Submodule.mem_set_smul_def :
∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] {S : Type u_4} [inst_1 : Monoid S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : DistribMulAction S M] (s : Set S) (N : Submodule R M) (x : M),
x ∈ s • N ↔ x ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}
The theorem `Submodule.mem_set_smul_def` states that for any type `R` being a semiring, `M` a commutative additive monoid forming a module over `R`, and `S` a monoid acting distributively on `M`, along with a set `s` of type `S`, a submodule `N` of `M`, and an element `x` of `M`, `x` is in the scalar multiplication of the set `s` and the submodule `N` if and only if `x` is in the infimum of the set of properties `p` such that for any element `r` of `S` and any element `n` of `M`, if `r` is in the set `s` and `n` is in the submodule `N`, then the scalar product of `r` and `n` is in `p`.
More concisely: For any semiring R, commutative additive monoid M making an R-module, monoid S acting distributively on M, set s of S, submodule N of M, and element x of M, x belongs to the scalar multiplication of set s and submodule N if and only if x is in the infimum of the set of properties p such that for all r in s and n in N, r * n is in p.
|
Submodule.set_smul_le
theorem Submodule.set_smul_le :
∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] {S : Type u_4} [inst_1 : Monoid S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : DistribMulAction S M] (s : Set S) (N p : Submodule R M),
(∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p
This theorem states that for any types `R`, `M`, and `S`, given a semiring structure on `R`, a monoid structure on `S`, an additive commutative monoid structure on `M`, a module structure of `R` over `M`, and a distributive multiplicative action of `S` on `M`, for any set `s` of type `S` and any two submodules `N` and `p` of `R` over `M`, if for every element `r` in `s` and `n` in `N`, the scalar multiplication of `r` and `n` is in `p`, then the scalar multiplication of the set `s` and the submodule `N` is a subset of `p`. In other words, this is a property about scalar multiplication in the context of module theory.
More concisely: If `s` is a set with a distributive multiplicative action on an `R`-module `M`, and for all `r in s` and `n in N`, the scalar multiplication `r * n` is in `p`, then `s * N` (the set of scalar multiplications of `s` on `N`) is a subset of `p`.
|
Submodule.set_smul_inductionOn
theorem Submodule.set_smul_inductionOn :
∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] {S : Type u_4} [inst_1 : Monoid S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : DistribMulAction S M] {s : Set S} {N : Submodule R M}
{motive : (x : M) → x ∈ s • N → Prop} (x : M) (hx : x ∈ s • N),
(∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯) →
(∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯) →
(∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N),
motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯) →
motive 0 ⋯ → motive x hx
This theorem is a principle of induction for sets acting on submodules. It asserts that to prove a property `P` holds for all elements of the form `s • N` (where `s` is a set and `N` is a submodule), it suffices to establish four conditions:
1. The property `P` holds for all elements of the form `r • n`, where `r` belongs to the set `s` and `n` belongs to the submodule `N`.
2. The property `P` holds for all elements of the form `r • m`, where `r` is any scalar and `m` belongs to the set `s • N`.
3. If the property `P` holds for elements `m₁` and `m₂`, then it also holds for their sum `m₁ + m₂`.
4. The property `P` holds for the zero element.
The theorem provides a mechanism to apply this induction principle by invoking `Submodule.set_smul_inductionOn` with an element `x` and a proof that `x` belongs to `s • N`.
More concisely: The theorem states that for a property `P` on sets acting on submodules, if `P` holds for all scalar multiples of elements in the set belonging to the submodule and satisfies the closure and identity properties, then `P` holds for all elements of the form `s • N`.
|
Submodule.mem_set_smul_of_mem_mem
theorem Submodule.mem_set_smul_of_mem_mem :
∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] {S : Type u_4} [inst_1 : Monoid S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : DistribMulAction S M] {s : Set S} {N : Submodule R M} {r : S} {m : M},
r ∈ s → m ∈ N → r • m ∈ s • N
This theorem, `Submodule.mem_set_smul_of_mem_mem`, states that for any given semiring `R`, type `M`, monoid `S`, set `s` of `S`, submodule `N` of `R` and `M`, and elements `r` of `S` and `m` of `M`, if `r` is in `s` and `m` is in `N`, then the scalar multiplication of `r` and `m` (denoted `r • m`) is in the set obtained by scalar multiplying all elements of `N` by all elements of `s` (denoted `s • N`). Here, `Semiring`, `Monoid`, `AddCommMonoid`, `Module`, and `DistribMulAction` are particular types of mathematical structures, and the elements and sets are assumed to behave according to the properties of these structures.
More concisely: If `r` is in `s` and `m` is in `N` for a semiring `R`, monoid `S`, set `s`, submodule `N` of `R` and `M`, then `r • m` is in `s • N`.
|