# mathlib3documentation

algebra.module.torsion

# Torsion submodules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• torsion_of R M x : the torsion ideal of x, containing all a such that a • x = 0.
• submodule.torsion_by R M a : the a-torsion submodule, containing all elements x of M such that a • x = 0.
• submodule.torsion_by_set R M s : the submodule containing all elements x of M such that a • x = 0 for all a in s.
• submodule.torsion' R M S : the S-torsion submodule, containing all elements x of M such that a • x = 0 for some a in S.
• submodule.torsion R M : the torsion submoule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.
• module.is_torsion_by R M a : the property that defines a a-torsion module. Similarly, is_torsion_by_set, is_torsion' and is_torsion.
• module.is_torsion_by_set.module : Creates a R ⧸ I-module from a R-module that is_torsion_by_set R _ I.

## Main statements #

• quot_torsion_of_equiv_span_singleton : isomorphism between the span of an element of M and the quotient by its torsion ideal.
• torsion' R M S and torsion R M are submodules.
• torsion_by_set_eq_torsion_by_span : torsion by a set is torsion by the ideal generated by it.
• submodule.torsion_by_is_torsion_by : the a-torsion submodule is a a-torsion module. Similar lemmas for torsion' and torsion.
• submodule.torsion_by_is_internal : a ∏ i, p i-torsion module is the internal direct sum of its p i-torsion submodules when the p i are pairwise coprime. A more general version with coprime ideals is submodule.torsion_by_set_is_internal.
• submodule.no_zero_smul_divisors_iff_torsion_bot : a module over a domain has no_zero_smul_divisors (that is, there is no non-zero a, x such that a • x = 0) iff its torsion submodule is trivial.
• submodule.quotient_torsion.torsion_eq_bot : quotienting by the torsion submodule makes the torsion submodule of the new module trivial. If R is a domain, we can derive an instance submodule.quotient_torsion.no_zero_smul_divisors : no_zero_smul_divisors R (M ⧸ torsion R M).

## Notation #

• The notions are defined for a comm_semiring R and a module R M. Some additional hypotheses on R and M are required by some lemmas.
• The letters a, b, ... are used for scalars (in R), while x, y, ... are used for vectors (in M).

## Tags #

Torsion, submodule, module, quotient

@[simp]
theorem ideal.torsion_of_carrier (R : Type u_1) (M : Type u_2) [semiring R] [ M] (x : M) :
M x).carrier = x) ⁻¹' {0}
def ideal.torsion_of (R : Type u_1) (M : Type u_2) [semiring R] [ M] (x : M) :

The torsion ideal of x, containing all a such that a • x = 0.

Equations
• x =
@[simp]
theorem ideal.torsion_of_zero (R : Type u_1) (M : Type u_2) [semiring R] [ M] :
0 =
@[simp]
theorem ideal.mem_torsion_of_iff {R : Type u_1} {M : Type u_2} [semiring R] [ M] (x : M) (a : R) :
a x a x = 0
@[simp]
theorem ideal.torsion_of_eq_top_iff (R : Type u_1) {M : Type u_2} [semiring R] [ M] (m : M) :
m = m = 0
@[simp]
theorem ideal.torsion_of_eq_bot_iff_of_no_zero_smul_divisors (R : Type u_1) {M : Type u_2} [semiring R] [ M] [nontrivial R] (m : M) :
m = m 0
theorem ideal.complete_lattice.independent.linear_independent' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {v : ι M} [ring R] [ M] (hv : complete_lattice.independent (λ (i : ι), {v i})) (h_ne_zero : (i : ι), (v i) = ) :

See also complete_lattice.independent.linear_independent which provides the same conclusion but requires the stronger hypothesis no_zero_smul_divisors R M.

noncomputable def ideal.quot_torsion_of_equiv_span_singleton (R : Type u_1) (M : Type u_2) [ring R] [ M] (x : M) :
(R x) ≃ₗ[R] {x})

The span of x in M is isomorphic to R quotiented by the torsion ideal of x.

Equations
@[simp]
theorem ideal.quot_torsion_of_equiv_span_singleton_apply_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (x : M) (a : R) :
= a x, _⟩
def submodule.torsion_by (R : Type u_1) (M : Type u_2) [ M] (a : R) :
M

The a-torsion submodule for a in R, containing all elements x of M such that a • x = 0.

Equations
Instances for ↥submodule.torsion_by
@[simp]
theorem submodule.torsion_by_carrier (R : Type u_1) (M : Type u_2) [ M] (a : R) :
a).carrier = ⁻¹' {0}
@[simp]
theorem submodule.torsion_by_set_carrier (R : Type u_1) (M : Type u_2) [ M] (s : set R) :
s).carrier = (y : R) (x : y s), y)
def submodule.torsion_by_set (R : Type u_1) (M : Type u_2) [ M] (s : set R) :
M

The submodule containing all elements x of M such that a • x = 0 for all a in s.

Equations
Instances for ↥submodule.torsion_by_set
def submodule.torsion' (R : Type u_1) (M : Type u_2) [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
M

The S-torsion submodule, containing all elements x of M such that a • x = 0 for some a in S.

Equations
Instances for ↥submodule.torsion'
@[simp]
theorem submodule.torsion'_carrier (R : Type u_1) (M : Type u_2) [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S).carrier = {x : M | (a : S), a x = 0}
@[reducible]
def submodule.torsion (R : Type u_1) (M : Type u_2) [ M] :
M

The torsion submodule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.

Equations
@[reducible]
def module.is_torsion_by (R : Type u_1) (M : Type u_2) [ M] (a : R) :
Prop

A a-torsion module is a module where every element is a-torsion.

Equations
@[reducible]
def module.is_torsion_by_set (R : Type u_1) (M : Type u_2) [ M] (s : set R) :
Prop

A module where every element is a-torsion for all a in s.

Equations
@[reducible]
def module.is_torsion' (M : Type u_2) (S : Type u_1) [ M] :
Prop

A S-torsion module is a module where every element is a-torsion for some a in S.

Equations
@[reducible]
def module.is_torsion (R : Type u_1) (M : Type u_2) [ M] :
Prop

A torsion module is a module where every element is a-torsion for some non-zero-divisor a.

Equations
@[simp]
theorem submodule.smul_torsion_by {R : Type u_1} {M : Type u_2} [ M] (a : R) (x : a)) :
a x = 0
@[simp]
theorem submodule.smul_coe_torsion_by {R : Type u_1} {M : Type u_2} [ M] (a : R) (x : a)) :
a x = 0
@[simp]
theorem submodule.mem_torsion_by_iff {R : Type u_1} {M : Type u_2} [ M] (a : R) (x : M) :
x a a x = 0
@[simp]
theorem submodule.mem_torsion_by_set_iff {R : Type u_1} {M : Type u_2} [ M] (s : set R) (x : M) :
x (a : s), a x = 0
@[simp]
theorem submodule.torsion_by_singleton_eq {R : Type u_1} {M : Type u_2} [ M] (a : R) :
{a} = a
theorem submodule.torsion_by_set_le_torsion_by_set_of_subset {R : Type u_1} {M : Type u_2} [ M] {s t : set R} (st : s t) :
theorem submodule.torsion_by_set_eq_torsion_by_span {R : Type u_1} {M : Type u_2} [ M] (s : set R) :
=

Torsion by a set is torsion by the ideal generated by it.

theorem submodule.torsion_by_span_singleton_eq {R : Type u_1} {M : Type u_2} [ M] (a : R) :
{a}) = a
theorem submodule.torsion_by_le_torsion_by_of_dvd {R : Type u_1} {M : Type u_2} [ M] (a b : R) (dvd : a b) :
a b
@[simp]
theorem submodule.torsion_by_one {R : Type u_1} {M : Type u_2} [ M] :
1 =
@[simp]
theorem submodule.torsion_by_univ {R : Type u_1} {M : Type u_2} [ M] :
@[simp]
theorem module.is_torsion_by_singleton_iff {R : Type u_1} {M : Type u_2} [ M] (a : R) :
{a} a
theorem module.is_torsion_by_set_iff_torsion_by_set_eq_top {R : Type u_1} {M : Type u_2} [ M] (s : set R) :
theorem module.is_torsion_by_iff_torsion_by_eq_top {R : Type u_1} {M : Type u_2} [ M] (a : R) :
a a =

A a-torsion module is a module whose a-torsion submodule is the full space.

theorem module.is_torsion_by_set_iff_is_torsion_by_span {R : Type u_1} {M : Type u_2} [ M] (s : set R) :
theorem module.is_torsion_by_span_singleton_iff {R : Type u_1} {M : Type u_2} [ M] (a : R) :
{a}) a
theorem submodule.torsion_by_set_is_torsion_by_set {R : Type u_1} {M : Type u_2} [ M] (s : set R) :
theorem submodule.torsion_by_is_torsion_by {R : Type u_1} {M : Type u_2} [ M] (a : R) :
a

The a-torsion submodule is a a-torsion module.

@[simp]
theorem submodule.torsion_by_torsion_by_eq_top {R : Type u_1} {M : Type u_2} [ M] (a : R) :
a =
@[simp]
theorem submodule.torsion_by_set_torsion_by_set_eq_top {R : Type u_1} {M : Type u_2} [ M] (s : set R) :
theorem submodule.torsion_gc (R : Type u_1) (M : Type u_2) [ M] :
(λ (I : (ideal R)ᵒᵈ),
theorem submodule.supr_torsion_by_ideal_eq_torsion_by_infi {R : Type u_1} {M : Type u_2} [ M] {ι : Type u_3} {p : ι } {S : finset ι} (hp : S.pairwise (λ (i j : ι), p i p j = )) :
( (i : ι) (H : i S), (p i)) = ( (i : ι) (H : i S), p i)
theorem submodule.sup_indep_torsion_by_ideal {R : Type u_1} {M : Type u_2} [ M] {ι : Type u_3} {p : ι } {S : finset ι} (hp : S.pairwise (λ (i j : ι), p i p j = )) :
S.sup_indep (λ (i : ι), (p i))
theorem submodule.supr_torsion_by_eq_torsion_by_prod {R : Type u_1} {M : Type u_2} [ M] {ι : Type u_3} {S : finset ι} {q : ι R} (hq : S.pairwise (is_coprime on q)) :
( (i : ι) (H : i S), (q i)) = (S.prod (λ (i : ι), q i))
theorem submodule.sup_indep_torsion_by {R : Type u_1} {M : Type u_2} [ M] {ι : Type u_3} {S : finset ι} {q : ι R} (hq : S.pairwise (is_coprime on q)) :
S.sup_indep (λ (i : ι), (q i))
theorem submodule.torsion_by_set_is_internal {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} [decidable_eq ι] {S : finset ι} {p : ι } (hp : S.pairwise (λ (i j : ι), p i p j = )) (hM : ( (i : ι) (H : i S), p i)) :

If the p i are pairwise coprime, a ⨅ i, p i-torsion module is the internal direct sum of its p i-torsion submodules.

theorem submodule.torsion_by_is_internal {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} [decidable_eq ι] {S : finset ι} {q : ι R} (hq : S.pairwise (is_coprime on q)) (hM : (S.prod (λ (i : ι), q i))) :
direct_sum.is_internal (λ (i : S), (q i))

If the q i are pairwise coprime, a ∏ i, q i-torsion module is the internal direct sum of its q i-torsion submodules.

def module.is_torsion_by_set.has_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {I : ideal R} (hM : I) :
has_smul (R I) M

can't be an instance because hM can't be inferred

Equations
@[simp]
theorem module.is_torsion_by_set.mk_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {I : ideal R} (hM : I) (b : R) (x : M) :
b x = b x
def module.is_torsion_by_set.module {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {I : ideal R} (hM : I) :
module (R I) M

A (R ⧸ I)-module is a R-module which is_torsion_by_set R M I.

Equations
@[protected, instance]
def module.is_torsion_by_set.is_scalar_tower {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {I : ideal R} (hM : I) {S : Type u_3} [ R] [ M] [ M] [ R] :
(R I) M
@[protected, instance]
def module.has_quotient.quotient.module {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {I : ideal R} :
module (R I) (M I )
Equations
@[protected, instance]
def submodule.torsion_by_set.module {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (I : ideal R) :
module (R I) I)
Equations
@[simp]
theorem submodule.torsion_by_set.mk_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (I : ideal R) (b : R) (x : I)) :
b x = b x
@[protected, instance]
def submodule.torsion_by_set.is_scalar_tower {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (I : ideal R) {S : Type u_3} [ R] [ M] [ M] [ R] :
(R I) I)
@[protected, instance]
def submodule.torsion_by.module {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (a : R) :
module (R {a}) a)

The a-torsion submodule as a (R ⧸ R∙a)-module.

Equations
@[simp]
theorem submodule.torsion_by.mk_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (a b : R) (x : a)) :
(ideal.quotient.mk {a})) b x = b x
@[protected, instance]
def submodule.torsion_by.is_scalar_tower {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (a : R) {S : Type u_3} [ R] [ M] [ M] [ R] :
(R {a}) a)
@[simp]
theorem submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] (x : M) :
x S (a : S), a x = 0
@[simp]
theorem submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [ M] (x : M) :
x (a : , a x = 0
@[protected, instance]
def submodule.torsion'.has_smul {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S)
Equations
@[simp]
theorem submodule.torsion'.has_smul_smul_coe {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] (s : S) (x : S)) :
(s x) = s x
@[protected, instance]
def submodule.torsion'.distrib_mul_action {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S)
Equations
@[protected, instance]
def submodule.torsion'.smul_comm_class {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S)
theorem submodule.is_torsion'_iff_torsion'_eq_top {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S =

A S-torsion module is a module whose S-torsion submodule is the full space.

theorem submodule.torsion'_is_torsion' {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S

The S-torsion submodule is a S-torsion module.

@[simp]
theorem submodule.torsion'_torsion'_eq_top {R : Type u_1} {M : Type u_2} [ M] (S : Type u_3) [comm_monoid S] [ M] [ M] :
S) S =
@[simp]
theorem submodule.torsion_torsion_eq_top {R : Type u_1} {M : Type u_2} [ M] :

The torsion submodule of the torsion submodule (viewed as a module) is the full torsion module.

theorem submodule.torsion_is_torsion {R : Type u_1} {M : Type u_2} [ M] :

The torsion submodule is always a torsion module.

theorem module.is_torsion_by_set_annihilator_top (R : Type u_1) (M : Type u_2) [ M] :
theorem submodule.annihilator_top_inter_non_zero_divisors {R : Type u_1} {M : Type u_2} [ M] [ M] (hM : M) :
theorem submodule.coe_torsion_eq_annihilator_ne_bot {R : Type u_1} {M : Type u_2} [ M] [nontrivial R] :
M) = {x : M | {x}).annihilator }

A module over a domain has no_zero_smul_divisors iff its torsion submodule is trivial.

@[simp]
theorem submodule.quotient_torsion.torsion_eq_bot {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] :
(M =

Quotienting by the torsion submodule gives a torsion-free module.

@[protected, instance]
theorem submodule.is_torsion'_powers_iff {R : Type u_1} {M : Type u_2} [monoid R] [ M] (p : R) :
(x : M), (n : ), p ^ n x = 0
def submodule.p_order {R : Type u_1} {M : Type u_2} [monoid R] [ M] {p : R} (hM : ) (x : M) [Π (n : ), decidable (p ^ n x = 0)] :

In a p ^ ∞-torsion module (that is, a module where all elements are cancelled by scalar multiplication by some power of p), the smallest n such that p ^ n • x = 0.

Equations
@[simp]
theorem submodule.pow_p_order_smul {R : Type u_1} {M : Type u_2} [monoid R] [ M] {p : R} (hM : ) (x : M) [Π (n : ), decidable (p ^ n x = 0)] :
p ^ x = 0
theorem submodule.exists_is_torsion_by {R : Type u_1} {M : Type u_2} [ M] [Π (x : M), decidable (x = 0)] {p : R} (hM : ) (d : ) (hd : d 0) (s : fin d M) (hs : (set.range s) = ) :
(j : fin d), (p ^ (s j))
theorem ideal.quotient.torsion_by_eq_span_singleton {R : Type u_1} [comm_ring R] (a b : R) (ha : a ) :
(R {a * b}) a = {(ideal.quotient.mk {a * b})) b}