Submodule.mul_induction_on'
theorem Submodule.mul_induction_on' :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{M N : Submodule R A} {C : (r : A) → r ∈ M * N → Prop},
(∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯) →
(∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯) →
∀ {r : A} (hr : r ∈ M * N), C r hr
This theorem, `Submodule.mul_induction_on'`, is a dependent version of `mul_induction_on` for submodules. Given a commutative semiring `R`, a semiring `A`, an algebra structure on `A` over `R`, and two submodules `M` and `N` of `A`, it states that for any property `C` that holds for every element of the form `m * n` where `m` is in `M` and `n` is in `N`, and for the sum of any two elements in `M * N` for which `C` holds, then `C` holds for every element in `M * N`.
More concisely: Given commutative semirings R, a semiring A with an algebra structure over R, and submodules M and N of A, if a property C holds for every product m * n with m in M and n in N, and for every a in M * N such that C(a) holds, then C holds for all elements in M * N.
|
Submodule.mul_mem_mul
theorem Submodule.mul_mem_mul :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{M N : Submodule R A} {m n : A}, m ∈ M → n ∈ N → m * n ∈ M * N
This theorem is stating that for any commutative semiring `R` and any semiring `A` that is an `R`-algebra, given any two submodules `M` and `N` of `A`, and any two elements `m` and `n` from `A`, if `m` is an element of `M` and `n` is an element of `N`, then the product `m * n` is an element of the submodule generated by the set of all products of an element from `M` and an element from `N`.
More concisely: For any commutative semiring `R`, `R`-algebra `A`, submodules `M` and `N` of `A`, and elements `m ∈ M` and `n ∈ N`, `m * n` belongs to the submodule generated by the set of products `{x * y | x ∈ M, y ∈ N}`.
|
Submodule.map_mul
theorem Submodule.map_mul :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(M N : Submodule R A) {A' : Type u_1} [inst_3 : Semiring A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N
The theorem `Submodule.map_mul` states that for any commutative semiring `R`, semirings `A` and `A'`, algebraic structures over `R` on `A` and `A'`, two submodules `M` and `N` of `A`, and an algebra homomorphism `f` from `A` to `A'`, the image under `f` of the product of `M` and `N` (i.e., `Submodule.map (AlgHom.toLinearMap f) (M * N)`) is equal to the product of the image under `f` of `M` and `N` (i.e., `Submodule.map (AlgHom.toLinearMap f) M * Submodule.map (AlgHom.toLinearMap f) N`). This is analogous to the property of a homomorphism in algebra that the image of a product is the product of the images.
More concisely: The theorem asserts that for any commutative semiring `R`, algebraic structures `A` and `A'`, submodules `M` and `N` of `A`, and an algebra homomorphism `f` from `A` to `A'`, we have `Submodule.map (AlgHom.toLinearMap f) (M * N) = Submodule.map (AlgHom.toLinearMap f) M * Submodule.map (AlgHom.toLinearMap f) N`.
|
Submodule.span_mul_span
theorem Submodule.span_mul_span :
∀ (R : Type u) [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Set A),
Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
This theorem states that for any commutative semiring `R` and any semiring `A` that is also an `R`-algebra, given any two sets `S` and `T` of elements of `A`, the span over `R` of the set `S` multiplied by the span over `R` of the set `T` is equal to the span over `R` of the set of all products of an element from `S` and an element from `T`. In simpler terms, the product of the spans of two sets is the same as the span of the products of the elements in the two sets.
More concisely: For any commutative semiring `R`, `R`-algebra `A`, sets `S` and `T` in `A`, the span of `S` multiplied by the span of `T` equals the span of the set of all products of elements from `S` and `T`.
|
Submodule.pow_induction_on_right
theorem Submodule.pow_induction_on_right :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
{C : A → Prop},
(∀ (r : R), C ((algebraMap R A) r)) →
(∀ (x y : A), C x → C y → C (x + y)) →
(∀ (x : A), C x → ∀ m ∈ M, C (x * m)) → ∀ {x : A} {n : ℕ}, x ∈ M ^ n → C x
This theorem states that for a given commutative semiring `R`, a semiring `A`, and an `R`-submodule `M` of `A`, if you want to prove a property `C` for all elements of the `n`-th power of `M`, it is sufficient to show three things:
1. The property `C` holds for all elements of `R` under the algebra map (`R` to `A`).
2. The property `C` is preserved under addition, i.e., if `C` holds for two elements `x` and `y` in `A`, it will also hold for their sum `x + y`.
3. The property `C` is preserved under multiplication with elements from `M`, i.e., for any element `x` in `A` for which `C` holds, and any element `m` in `M`, `C` will also hold for the product `x * m`.
Then, for any element `x` in the `n`-th power of `M`, the property `C` will hold.
More concisely: If `R` is a commutative semiring, `A` is an `R`-algebra, and `M` is an `R`-submodule of `A`, for any property `C` on `A`, if `C` holds for the image of `R` under the algebra map, and `C` is additively and multiplicatively preserved, then `C` holds for all elements in the `n`-th power of `M`.
|
Submodule.mul_bot
theorem Submodule.mul_bot :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(M : Submodule R A), M * ⊥ = ⊥
This theorem states that for any module `M` over a commutative semiring `R` and a semiring `A`, which also has a defined algebra structure over `R`, the product of `M` and the bottom element (denoted by `⊥`) equals the bottom element. Essentially, it says that multiplying any submodule with the zero submodule results in the zero submodule.
More concisely: For any module M over a commutative semiring R and a semiring A with an algebra structure over R, the product of M and the bottom element of A is the bottom element of the module M. In other words, M⊤ = ⊥M, where ⊤ is the bottom element of A and ⊥M is the bottom element of M.
|
Submodule.mul_le
theorem Submodule.mul_le :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{M N P : Submodule R A}, M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
This theorem, `Submodule.mul_le`, states that for any Commutative Semiring `R`, Semiring `A` and an algebra `A` over `R`, and for any submodules `M`, `N`, and `P` of `A`, the product of `M` and `N` is a subset of `P` if and only if for all elements `m` in `M` and `n` in `N`, the product `m * n` is an element of `P`. This is a theorem about the multiplicative properties of submodules in a ring.
More concisely: For any commutative semirings R, semiring A, algebra A over R, and submodules M, N, and P of A, M * N ⊆ P if and only if m * n ∈ P for all m ∈ M and n ∈ N.
|
Submodule.pow_induction_on_right'
theorem Submodule.pow_induction_on_right' :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
{C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop},
(∀ (r : R), C 0 ((algebraMap R A) r) ⋯) →
(∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) →
(∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯) →
∀ {n : ℕ} {x : A} (hx : x ∈ M ^ n), C n x hx
This theorem, `Submodule.pow_induction_on_right'`, is a dependent version of `Submodule.pow_induction_on_right`. It states that, for any type `R` with a `CommSemiring` instance and any type `A` with a `Semiring` and `Algebra R A` instances, and a given `Submodule` `M` of `R` and `A`, we can define a property `C` dependent on a natural number `n`, an element `x` of type `A`, and the proof that `x` belongs to the `n`th power of the submodule `M`. If this property holds for zero and any ring element `r` under `algebraMap R A`, and if it is preserved under addition of elements `x` and `y` in the `i`th power of `M`, and under multiplication by an element `m` in `M`, then this property holds for any natural number `n`, any element `x` of `A` and any proof that `x` belongs to the `n`th power of `M`.
More concisely: Given a commutative semiring `R`, a semiring `A` with an algebra structure over `R`, a submodule `M` of `R`, and a natural number `n`, if a property `C` holds for `x` in `A` and the `n`th power of `M` when `x` lies in the `0`th power of `M` and is preserved under addition and multiplication, then `C` holds for any `x` in `A` and proof of `x` belonging to the `n`th power of `M`.
|
Submodule.pow_induction_on_left
theorem Submodule.pow_induction_on_left :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
{C : A → Prop},
(∀ (r : R), C ((algebraMap R A) r)) →
(∀ (x y : A), C x → C y → C (x + y)) →
(∀ m ∈ M, ∀ (x : A), C x → C (m * x)) → ∀ {x : A} {n : ℕ}, x ∈ M ^ n → C x
The theorem `Submodule.pow_induction_on_left` states that to prove a property `C` holds for all elements `x` of a power `M ^ n` of a submodule `M` over an algebra `A` of a commutative semiring `R`, we can do so by showing three things: first, that `C` holds for all elements of `R` when they are mapped into `A` using the algebra structure; second, that `C` is closed under addition in `A`; and third, that if `C` holds for an element `x` in `A`, then it also holds for the element resulting from the multiplication of `x` with any element `m` from `M`.
In other words, it provides an induction principle for proving properties about elements in the powers of a submodule of an algebra.
More concisely: To prove a property holds for all elements in the power of a submodule of a commutative semiring algebra, it suffices to show that it holds for elements mapped from the base semiring, is closed under addition, and is multiplicatively closed.
|
Mathlib.Algebra.Algebra.Operations._auxLemma.1
theorem Mathlib.Algebra.Algebra.Operations._auxLemma.1 :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
(x ∈ 1) = ∃ y, (algebraMap R A) y = x
This theorem states that for any type `R` with a commutative semiring structure and another type `A` with a semiring structure and an algebra structure over `R`, and for any element `x` of `A`, `x` belongs to `1` if and only if there exists an element `y` from `R` such that when `y` is mapped into `A` using the algebra structure, it equals `x`. In other words, every element in the unit of `A` can be represented as an image of an element from `R` under the algebra map.
More concisely: For any commutative semiring `R` and an `R`-algebra `A` with unit `1`, an element `x` of `A` belongs to the unit if and only if there exists `r` in `R` such that `x = alg_map r 1`, where `alg_map` is the algebra map from `R` to `A`.
|
Submodule.pow_induction_on_left'
theorem Submodule.pow_induction_on_left' :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
{C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop},
(∀ (r : R), C 0 ((algebraMap R A) r) ⋯) →
(∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) →
(∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯) →
∀ {n : ℕ} {x : A} (hx : x ∈ M ^ n), C n x hx
This theorem, called `Submodule.pow_induction_on_left'`, is a version of the principle of mathematical induction for powers of submodules in an algebraic structure. Given a commutative semiring `R`, a semiring `A`, and an algebra structure on `A` over `R`, for any submodule `M` of `A` and a property `C` that assigns to each natural number `n` and to each element `x` in the `n`th power of `M` a proposition, the theorem states that if `C` holds for each element of the image of `R` under the algebra map at the zeroth power of `M`, and if `C` is preserved under addition and multiplication by elements of `M` within each power of `M`, then `C` holds for all elements in all powers of `M`. Moreover, the property `C` depends on the evidence that `x` is in the `n`th power of `M`.
More concisely: If `M` is a submodule of a commutative semiring `A` with an algebra structure over a semiring `R`, and `C` is a property that holds for each element in the image of `R` under the algebra map at the zeroth power of `M`, and is preserved under addition and multiplication by elements of `M` within each power of `M`, then `C` holds for all elements in all powers of `M`.
|
Submodule.one_eq_span
theorem Submodule.one_eq_span :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
1 = Submodule.span R {1}
The theorem `Submodule.one_eq_span` states that for any commutative semiring `R`, any semiring `A`, and any algebra structure over `A` with `R` as the scalar ring, the submodule generated by `{1}` (i.e., the set containing only the multiplicative identity) in the algebra is equal to `1`. This means that the smallest submodule of `A` that contains the multiplicative identity `1` is, in fact, the `1` itself. This is typically an important property in algebra where the multiplicative identity plays a critical role.
More concisely: In any commutative semiring-algebra, the submodule generated by {1} is equal to the multiplicative identity 1.
|
Submodule.mul_induction_on
theorem Submodule.mul_induction_on :
∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{M N : Submodule R A} {C : A → Prop} {r : A},
r ∈ M * N → (∀ m ∈ M, ∀ n ∈ N, C (m * n)) → (∀ (x y : A), C x → C y → C (x + y)) → C r
This theorem, `Submodule.mul_induction_on`, establishes a form of mathematical induction for the multiplication operation on submodules of an algebra over a commutative semiring. Specifically, given two submodules `M` and `N` of an algebra `A` over a commutative semiring `R`, and a property `C` that applies to elements of `A`, if every product of an element from `M` and an element from `N` satisfies `C`, and `C` is preserved under addition, then `C` is true for all elements of the submodule generated by the product of `M` and `N`.
More concisely: Given submodules M and N of a commutative semiring algebra A, if every m ∈ M and n ∈ N satisfy property C on their product, and property C is additively closed, then property C holds for all elements of the submodule generated by the products of M and N.
|