mathlib documentation

algebra.module.torsion

Torsion submodules #

Main definitions #

Main statements #

Notation #

Tags #

Torsion, submodule, module, quotient

@[simp]
theorem ideal.torsion_of_carrier (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] (x : M) :
def ideal.torsion_of (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] (x : M) :

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

Equations
@[simp]
theorem ideal.torsion_of_zero (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem ideal.mem_torsion_of_iff {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (x : M) (a : R) :
a ideal.torsion_of R M x a x = 0
@[simp]
theorem ideal.torsion_of_eq_top_iff (R : Type u_1) {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (m : M) :
@[simp]
theorem ideal.torsion_of_eq_bot_iff_of_no_zero_smul_divisors (R : Type u_1) {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [nontrivial R] [no_zero_smul_divisors R M] (m : M) :
theorem ideal.complete_lattice.independent.linear_independent' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : complete_lattice.independent (λ (i : ι), submodule.span R {v i})) (h_ne_zero : ∀ (i : ι), ideal.torsion_of R M (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] [add_comm_group M] [module R M] (x : M) :

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] [add_comm_group M] [module R M] (x : M) (a : R) :
def submodule.torsion_by (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :

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) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :
@[simp]
theorem submodule.torsion_by_set_carrier (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) :
(submodule.torsion_by_set R M s).carrier = ⋂ (y : R) (x : y s), (submodule.torsion_by R M y)
def submodule.torsion_by_set (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) :

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) [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R 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) [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :
(submodule.torsion' R M S).carrier = {x : M | ∃ (a : S), a x = 0}
@[reducible]
def submodule.torsion (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R 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) [comm_semiring R] [add_comm_monoid M] [module R 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) [comm_semiring R] [add_comm_monoid M] [module R 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) [add_comm_monoid M] (S : Type u_1) [has_smul S 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) [comm_semiring R] [add_comm_monoid M] [module R 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} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) (x : (submodule.torsion_by R M a)) :
a x = 0
@[simp]
theorem submodule.smul_coe_torsion_by {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) (x : (submodule.torsion_by R M a)) :
a x = 0
@[simp]
theorem submodule.mem_torsion_by_iff {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) (x : M) :
@[simp]
theorem submodule.mem_torsion_by_set_iff {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) (x : M) :
x submodule.torsion_by_set R M s ∀ (a : s), a x = 0
@[simp]
theorem submodule.torsion_by_singleton_eq {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :

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

theorem submodule.torsion_by_le_torsion_by_of_dvd {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a b : R) (dvd : a b) :
@[simp]
theorem submodule.torsion_by_one {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.torsion_by_univ {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem module.is_torsion_by_singleton_iff {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :
theorem module.is_torsion_by_iff_torsion_by_eq_top {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :

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

theorem submodule.torsion_by_is_torsion_by {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :

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} [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :
theorem submodule.supr_torsion_by_ideal_eq_torsion_by_infi {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {p : ι → ideal R} {S : finset ι} (hp : S.pairwise (λ (i j : ι), p i p j = )) :
(⨆ (i : ι) (H : i S), submodule.torsion_by_set R M (p i)) = submodule.torsion_by_set R M (⨅ (i : ι) (H : i S), p i)
theorem submodule.sup_indep_torsion_by_ideal {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {p : ι → ideal R} {S : finset ι} (hp : S.pairwise (λ (i j : ι), p i p j = )) :
S.sup_indep (λ (i : ι), submodule.torsion_by_set R M (p i))
theorem submodule.supr_torsion_by_eq_torsion_by_prod {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {S : finset ι} {q : ι → R} (hq : S.pairwise (is_coprime on q)) :
(⨆ (i : ι) (H : i S), submodule.torsion_by R M (q i)) = submodule.torsion_by R M (S.prod (λ (i : ι), q i))
theorem submodule.sup_indep_torsion_by {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {S : finset ι} {q : ι → R} (hq : S.pairwise (is_coprime on q)) :
S.sup_indep (λ (i : ι), submodule.torsion_by R M (q i))
theorem submodule.torsion_by_set_is_internal {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] {S : finset ι} {p : ι → ideal R} (hp : S.pairwise (λ (i j : ι), p i p j = )) (hM : module.is_torsion_by_set R M (⨅ (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] [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] {S : finset ι} {q : ι → R} (hq : S.pairwise (is_coprime on q)) (hM : module.is_torsion_by R M (S.prod (λ (i : ι), 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] [add_comm_group M] [module R M] {I : ideal R} (hM : module.is_torsion_by_set R M 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] [add_comm_group M] [module R M] {I : ideal R} (hM : module.is_torsion_by_set R M I) (b : R) (x : M) :
def module.is_torsion_by_set.module {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (hM : module.is_torsion_by_set R M 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] [add_comm_group M] [module R M] {I : ideal R} (hM : module.is_torsion_by_set R M I) {S : Type u_3} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] [is_scalar_tower S R R] :
@[protected, instance]
def module.has_quotient.quotient.module {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module 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] [add_comm_group M] [module R M] (I : ideal R) :
Equations
@[simp]
theorem submodule.torsion_by_set.mk_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (b : R) (x : (submodule.torsion_by_set R M I)) :
@[protected, instance]
def submodule.torsion_by_set.is_scalar_tower {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) {S : Type u_3} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] [is_scalar_tower S R R] :
@[protected, instance]
def submodule.torsion_by.module {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (a : R) :

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] [add_comm_group M] [module R M] (a b : R) (x : (submodule.torsion_by R M a)) :
@[protected, instance]
def submodule.torsion_by.is_scalar_tower {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (a : R) {S : Type u_3} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] [is_scalar_tower S R R] :
@[simp]
theorem submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] (x : M) :
x submodule.torsion' R M S ∃ (a : S), a x = 0
@[simp]
theorem submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (x : M) :
x submodule.torsion R M ∃ (a : (non_zero_divisors R)), a x = 0
@[protected, instance]
def submodule.torsion'.has_smul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :
Equations
@[simp]
theorem submodule.torsion'.has_smul_smul_coe {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] (s : S) (x : (submodule.torsion' R M S)) :
(s x) = s x
@[protected, instance]
def submodule.torsion'.smul_comm_class {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :
theorem submodule.is_torsion'_iff_torsion'_eq_top {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :

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} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :

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

@[simp]
theorem submodule.torsion'_torsion'_eq_top {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (S : Type u_3) [comm_monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :
@[simp]
theorem submodule.torsion_torsion_eq_top {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R 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} [comm_semiring R] [add_comm_monoid M] [module R M] :

The torsion submodule is always a torsion module.

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] [add_comm_group M] [module R 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] [add_comm_monoid M] [distrib_mul_action R M] (p : R) :
module.is_torsion' M (submonoid.powers p) ∀ (x : M), ∃ (n : ), p ^ n x = 0
def submodule.p_order {R : Type u_1} {M : Type u_2} [monoid R] [add_comm_monoid M] [distrib_mul_action R M] {p : R} (hM : module.is_torsion' M (submonoid.powers p)) (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] [add_comm_monoid M] [distrib_mul_action R M] {p : R} (hM : module.is_torsion' M (submonoid.powers p)) (x : M) [Π (n : ), decidable (p ^ n x = 0)] :
theorem submodule.exists_is_torsion_by {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] [Π (x : M), decidable (x = 0)] {p : R} (hM : module.is_torsion' M (submonoid.powers p)) (d : ) (hd : d 0) (s : fin d → M) (hs : submodule.span R (set.range s) = ) :
∃ (j : fin d), module.is_torsion_by R M (p ^ submodule.p_order hM (s j))