Submodule.isTorsion'_iff_torsion'_eq_top
theorem Submodule.isTorsion'_iff_torsion'_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(S : Type u_3) [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
Module.IsTorsion' M S ↔ Submodule.torsion' R M S = ⊤
This theorem states that for any commutative semiring `R`, any module `M` over `R` with addition being a commutative monoid, any type `S` with commutative monoid structure, any distributive multiplication action of `S` on `M`, and any scalar multiplication operation on `M` that commutes with the multiplication in `R` and `S`, a module `M` is an `S`-torsion module (i.e., every element of `M` is `S`-torsion) if and only if the `S`-torsion submodule of `M`, which includes all elements `x` in `M` such that `a • x = 0` for some `a` in `S`, is the entire space of `M`. Here, `a • x = 0` means that `x` is annihilated by scalar multiplication with `a`.
More concisely: A commutative `R`-module `M` with a commutative monoid structure on its scalars `S`, equipped with a distributive `S`-module action and commuting scalar multiplication, is `S`-torsion if and only if the `S`-torsion submodule generated by all elements annihilated by some scalar in `S` equals `M`.
|
Submodule.torsionBySet_eq_torsionBySet_span
theorem Submodule.torsionBySet_eq_torsionBySet_span :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Set R), Submodule.torsionBySet R M s = Submodule.torsionBySet R M ↑(Ideal.span s)
This theorem states that for any set `s` of elements from a commutative semiring `R` and an additive commutative monoid `M` that also forms an `R`-module, the submodule containing all elements `x` from `M` such that every element `a` in `s` annihilates `x` (i.e., `a • x = 0`) is the same as the submodule of `M` where every element is annihilated by the ideal generated by `s`. In other words, the torsion elements of `M` by `s` are the same as the torsion elements of `M` by the ideal spanned by `s`.
More concisely: For any commutative semiring `R`, commutative monoid `M` that is an `R`-module, and set `s` in `R`, the submodule of `M` consisting of elements annihilated by every `a` in `s` is equal to the submodule of `M` annihilated by the ideal generated by `s`.
|
Module.isTorsionBySet_iff_torsionBySet_eq_top
theorem Module.isTorsionBySet_iff_torsionBySet_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Set R), Module.IsTorsionBySet R M s ↔ Submodule.torsionBySet R M s = ⊤
This theorem states that for any set `s` of scalars from a commutative semiring `R` and any module `M` over `R`, the module `M` is `a`-torsion for all `a` in `s` if and only if the submodule containing all elements `x` of `M` such that `a • x = 0` for all `a` in `s` is the entire module `M`. In other words, all elements of the module are annihilated by some scalar in the set `s`.
More concisely: A module over a commutative semiring is torsion with respect to a set of scalars if and only if the submodule of elements annihilated by all scalars in the set is equal to the entire module.
|
Submodule.torsionBySet_le_torsionBySet_of_subset
theorem Submodule.torsionBySet_le_torsionBySet_of_subset :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{s t : Set R}, s ⊆ t → Submodule.torsionBySet R M t ≤ Submodule.torsionBySet R M s
This theorem states that for any two sets `s` and `t` of scalars in a commutative semiring `R` and a module `M` over `R`, if `s` is a subset of `t`, then the submodule of `M` generated by the torsion elements with respect to `t` is a subset of, or equal to, the submodule generated by the torsion elements with respect to `s`. Here, a torsion element of `M` by a set of scalars is an element that is annihilated by every scalar in the set.
More concisely: For any commutative semiring R and module M over R, if set s is a subset of set t of scalars, then the submodule of M generated by the torsion elements with respect to t is contained in, or equal to, the submodule generated by the torsion elements with respect to s.
|
Module.isTorsionBy_iff_torsionBy_eq_top
theorem Module.isTorsionBy_iff_torsionBy_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
Module.IsTorsionBy R M a ↔ Submodule.torsionBy R M a = ⊤
The theorem `Module.isTorsionBy_iff_torsionBy_eq_top` establishes an equivalence between two properties for a module `M` over a commutative semiring `R` and an element `a` of `R`. The first property, referred as `Module.IsTorsionBy R M a`, states that `M` is an `a`-torsion module, meaning that for every element `x` in `M`, the product of `a` and `x` equals zero. The second property states that the `a`-torsion submodule of `M`, which consists of all elements `x` of `M` such that `a` and `x` together yield zero, is actually equal to the full module `M` itself. Hence, the theorem demonstrates that `M` being an `a`-torsion module is equivalent to the `a`-torsion submodule of `M` being the entire space `M`.
More concisely: For a commutative semiring R and a module M over R, an element a of R makes M torsion if and only if the a-torsion submodule of M equals M as a whole.
|
Submodule.torsion'_isTorsion'
theorem Submodule.torsion'_isTorsion' :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(S : Type u_3) [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
Module.IsTorsion' (↥(Submodule.torsion' R M S)) S
The theorem `Submodule.torsion'_isTorsion'` states that, for any commutative semiring `R`, any additive commutative monoid `M` that is also an `R`-module, any commutative monoid `S` that acts distributively on `M` and commutes with the action of `R` on `M`, the `S`-torsion submodule of `M` is an `S`-torsion module. In other words, every element of the `S`-torsion submodule is `S`-torsion, which means there exists some element in `S` such that when it is scalar-multiplied with the submodule element, the result is zero.
More concisely: For any commutative semiring R, additive commutative monoid M that is an R-module, and commutative monoid S acting distributively and commuting with R's action on M, the `S`-torsion submodule of M is an `S`-torsion module, i.e., every element in the submodule is `S`-torsion.
|
Submodule.torsionBySet_singleton_eq
theorem Submodule.torsionBySet_singleton_eq :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
Submodule.torsionBySet R M {a} = Submodule.torsionBy R M a
The theorem `Submodule.torsionBySet_singleton_eq` states that for any commutative semiring `R`, an additive commutative monoid `M`, and a `R`-module `M`, for any element `a` of `R`, the submodule of `M` generated by the `a`-torsion elements (those `x` in `M` for which `a • x = 0`) when considered as a set `{a}` is the same as the submodule generated when `a` is considered individually. In simpler terms, it means that the set of all elements in `M` that become zero when scaled by `a`, remains the same whether `a` is seen as a singleton set `{a}` or as an individual element `a` in `R`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, and `R`-module `M`, the submodule generated by an element `a` in `R`'s `a`-torsion elements is equal to the submodule generated by the singleton set `{a}`.
|
Submodule.mem_torsionBySet_iff
theorem Submodule.mem_torsionBySet_iff :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R)
(x : M), x ∈ Submodule.torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
The theorem `Submodule.mem_torsionBySet_iff` establishes a characterization of membership in a certain submodule of a module. Specifically, for any commutative semiring `R`, any additive commutative monoid `M` that is also an `R`-module, any set `s` of scalars from `R`, and any element `x` from `M`, it states that `x` belongs to the submodule `torsionBySet R M s` (which consists of all elements in `M` annihilated by some scalar in `s`) if and only if for every scalar `a` in `s` (represented as `↑s`), the scalar multiplication `↑a • x` equals zero.
More concisely: A module element belongs to the submodule generated by scalars in a set if and only if it is annihilated by every scalar in the set.
|
Submodule.torsionBy_isTorsionBy
theorem Submodule.torsionBy_isTorsionBy :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
Module.IsTorsionBy R (↥(Submodule.torsionBy R M a)) a
The theorem `Submodule.torsionBy_isTorsionBy` states that for any commutative semiring `R`, any Additive Commutative Monoid `M` which is also an `R`-module, and any element `a` of `R`, the `a`-torsion submodule of `M` is an `a`-torsion module. In other words, all elements in the `a`-torsion submodule of `M` are `a`-torsion elements, meaning that they become the zero element when scaled by `a`.
More concisely: For any commutative semiring R, Additive Commutative Monoid M being an R-module, and element a of R, the a-torsion submodule of M is the set of a-torsion elements of M.
|
Submodule.torsion_isTorsion
theorem Submodule.torsion_isTorsion :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Module.IsTorsion R ↥(Submodule.torsion R M)
The theorem `Submodule.torsion_isTorsion` states that for any commutative semiring `R` and any additive commutative monoid `M`, where `M` is a module over `R`, the torsion submodule of `M` is always a torsion module. In more mathematical terms, it means that for any element in the torsion submodule (the set of all elements `x` in `M` such that `a * x = 0` for some non-zero-divisor `a` in `R`), there exists a non-zero-divisor `a` in `R` such that `a` times that element equals zero, which is the definition of a torsion module.
More concisely: For any commutative semiring `R` and additive commutative monoid `M` being an `R`-module, the torsion submodule of `M` is a submodule consisting of elements torsion over some non-zero-divisor in `R`.
|
Submodule.torsion_torsion_eq_top
theorem Submodule.torsion_torsion_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Submodule.torsion R ↥(Submodule.torsion R M) = ⊤
The theorem `Submodule.torsion_torsion_eq_top` states that for any given commutative semiring `R` and additive commutative monoid `M` that is also a module over `R`, the torsion submodule of the torsion submodule (when considered as a module itself) is equal to the full module. In other words, any element of the torsion submodule of the torsion submodule is also an element of the full module; or put another way, the set of all "torsion" elements (elements `x` such that `a • x = 0` for some non-zero-divisor `a` in `R`) in the torsion submodule also forms a full module.
More concisely: The torsion submodule of a commutative semiring's module is equal to the full module when considered as a submodule itself.
|
Ideal.CompleteLattice.Independent.linear_independent'
theorem Ideal.CompleteLattice.Independent.linear_independent' :
∀ {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M],
(CompleteLattice.Independent fun i => Submodule.span R {v i}) →
(∀ (i : ι), Ideal.torsionOf R M (v i) = ⊥) → LinearIndependent R v
The theorem `Ideal.CompleteLattice.Independent.linear_independent'` states that given some types `ι`, `R` and `M`, a function `v` from `ι` to `M`, a ring structure on `R`, an additive commutative group structure on `M`, and a module structure for `M` over `R`, if the set of submodules spanned by each vector in the image of `v` forms a complete lattice and is independent, and for every vector in the image of `v`, the torsion ideal is trivial (i.e., consists only of the zero element), then the set of vectors in the image of `v` is linearly independent over `R`. Here, "linearly independent" means that no vector in the set can be expressed as a linear combination of the other vectors in the set.
More concisely: Given a type `ι`, a function `v : ι → M` from a set to an `R`-module `M` over a ring `R`, if the image of `v` generates a complete lattice of submodules of `M` that are pairwise independent and each vector in the image has a trivial torsion ideal, then the set of vectors in the image of `v` is linearly independent over `R`.
|
Submodule.QuotientTorsion.torsion_eq_bot
theorem Submodule.QuotientTorsion.torsion_eq_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Submodule.torsion R (M ⧸ Submodule.torsion R M) = ⊥
The theorem `Submodule.QuotientTorsion.torsion_eq_bot` states that for any commutative ring `R` and any additive commutative group `M` that is also a module over `R`, when `M` is quotiented by its torsion submodule (i.e., the subgroup consisting of all elements `x` in `M` such that `a * x = 0` for some non-zero-divisor `a` in `R`), the resulting quotient module is torsion-free. In other words, the torsion submodule of the quotient module is the zero submodule. This implies that there are no elements in the quotient module that become zero when scaled by a non-zero element from the ring `R`.
More concisely: For any commutative ring `R` and an `R`-module `M`, the quotient `M/torsion M` is a torsion-free module, where `torsion M` is the submodule of `M` consisting of elements mapped to zero in the quotient.
|
Submodule.torsionBySet_isInternal
theorem Submodule.torsionBySet_isInternal :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
[inst_3 : DecidableEq ι] {S : Finset ι} {p : ι → Ideal R},
((↑S).Pairwise fun i j => p i ⊔ p j = ⊤) →
Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i) → DirectSum.IsInternal fun i => Submodule.torsionBySet R M ↑(p ↑i)
The theorem `Submodule.torsionBySet_isInternal` states that for a commutative ring `R` and an additive commutative group `M` that is also a module over `R`, given a set `S` of indices with decidable equality and a function `p` mapping each index to an ideal of `R`, if for every pair of distinct indices in `S`, the sum of their corresponding ideals is the whole ring (`⊤`), then for any module that is `⨅ i ∈ S, p i`-torsion (meaning every element is `a`-torsion for all `a` in the infimum of the ideals indexed by `S`), it is the internal direct sum of its `p i`-torsion submodules (each submodule contains elements `x` of `M` such that `a • x = 0` for all `a` in the ideal `p i`). In other words, this theorem is about the structure of a module that is torsion by a set of pairwise coprime ideals.
More concisely: If a module over a commutative ring is torsion by a set of pairwise coprime ideals, then it is the internal direct sum of its submodules consisting of elements mapping to the zero element under the ideals.
|
Submodule.torsionBy_isInternal
theorem Submodule.torsionBy_isInternal :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
[inst_3 : DecidableEq ι] {S : Finset ι} {q : ι → R},
(↑S).Pairwise (IsCoprime on q) →
Module.IsTorsionBy R M (S.prod fun i => q i) → DirectSum.IsInternal fun i => Submodule.torsionBy R M (q ↑i)
This theorem states that if a set of elements `{q i}` in a commutative ring `R` are pairwise coprime (meaning that for each pair `i` and `j` with `i ≠ j`, there exist elements `a` and `b` in the ring such that `a * q i + b * q j = 1`), then a module `M` over `R` that is `∏ i, q i`-torsion (meaning that for every element `x` in the module, `∏ i, q i * x = 0`) is the internal direct sum of its `{q i}`-torsion submodules.
In other words, under these conditions, each element of the module can be uniquely expressed as a sum of elements from the `{q i}`-torsion submodules, which are subsets of the module where each element `x` satisfies `q i * x = 0` for some `i`. This is a decomposition result for modules over commutative rings involving coprime and torsion elements.
More concisely: If a set of pairwise coprime elements in a commutative ring generates the identity, then every `∏ i, q i`-torsion module is the internal direct sum of its submodules of `q i`-torsion elements.
|
Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{ι : Type u_3} {p : ι → Ideal R} {S : Finset ι},
((↑S).Pairwise fun i j => p i ⊔ p j = ⊤) →
⨆ i ∈ S, Submodule.torsionBySet R M ↑(p i) = Submodule.torsionBySet R M ↑(⨅ i ∈ S, p i)
The theorem `Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf` states that for a commutative semiring `R` and an additive commutative monoid `M` that is also an `R`-module, given a family of ideals `p` indexed by type `ι` and a finite set `S` of these indices, if for every pair of distinct elements in `S`, the sup of their corresponding ideals is the whole ring (denoted as `p i ⊔ p j = ⊤`), then the supremum of the set of submodules obtained by taking the torsion elements of `M` by the set of elements of the ideals corresponding to each index in `S`, equals the submodule obtained by taking the torsion elements of `M` by the set of elements of the infimum of the ideals corresponding to each index in `S`. In other words, the "torsion part" of the supremum of a pairwise top set of ideals is the same as the "torsion part" of the infimum of these ideals.
More concisely: Given a commutative semiring R, an additive commutative monoid M that is an R-module, a family of ideals p indexed by type ι, and a finite set S of indices such that p i ⊔ p j = ⊤ for all distinct i, j ∈ S, the torsion submodules of M by the sets of elements of the infimum and supremum of the ideals indexed by S are equal.
|
Submodule.noZeroSMulDivisors_iff_torsion_eq_bot
theorem Submodule.noZeroSMulDivisors_iff_torsion_eq_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : NoZeroDivisors R] [inst_4 : Nontrivial R], NoZeroSMulDivisors R M ↔ Submodule.torsion R M = ⊥
This theorem states that for any commutative semiring `R` and any additive commutative monoid `M` that is also a module over `R`, if `R` has no zero divisors and is nontrivial (i.e., not just the zero element), then `M` has no zero smul divisors if and only if its torsion submodule is trivial.
In mathematical terms, a module over a domain has no zero scalar-multiplier divisors (an element `x` in `M` and a scalar `a` in `R` are called *zero smul divisors* if `a • x = 0` for some non-zero `a` in `R`) if and only if all elements `x` in `M` are non-torsion, i.e., there does not exist a non-zero divisor `a` in `R` such that `a • x = 0`. A submodule is said to be trivial if it only contains the zero element.
More concisely: For a commutative semiring `R` with no zero divisors and a commutative additive monoid `M` that is an `R`-module, `M` has no zero scalar-multiplier divisors if and only if its torsion submodule is trivial.
|
Submodule.torsionBySet_span_singleton_eq
theorem Submodule.torsionBySet_span_singleton_eq :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
Submodule.torsionBySet R M ↑(Submodule.span R {a}) = Submodule.torsionBy R M a
The theorem `Submodule.torsionBySet_span_singleton_eq` states that for any commutative semiring `R`, any additive commutative monoid `M` that is also an `R`-module, and any element `a` of `R`, the submodule of `M` consisting of all elements `x` such that `a • x = 0` for all `a` in the span of the singleton set `{a}` is the same as the `a`-torsion submodule, which consists of all elements `x` of `M` such that `a • x = 0`. Essentially, this theorem states that the torsion by a set generated by an element `a` is the same as the torsion by the element `a` itself.
More concisely: For any commutative semiring R, additive commutative monoid M being an R-module, and element a in R, the submodule of M consisting of elements x with a • x = 0 for all a in the span of {a} equals the a-torsion submodule of M, which consists of elements x with a • x = 0.
|