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

source

@[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) :

(ideal.torsion_of R M x).carrier = ⇑(linear_map.to_span_singleton R M x) ⁻¹' {0}

source

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

ideal R

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

Equations

ideal.torsion_of R M x = linear_map.ker (linear_map.to_span_singleton R M x)

source

@[simp]

theorem ideal.torsion_of_zero (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] :

ideal.torsion_of R M 0 = ⊤

source

@[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

source

@[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) :

ideal.torsion_of R M m = ⊤ ↔ m = 0

source

@[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) :

ideal.torsion_of R M m = ⊥ ↔ m ≠ 0

source

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) = ⊥) :

linear_independent R v

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

source

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) :

(R ⧸ ideal.torsion_of R M x) ≃ₗ[R] ↥(submodule.span R {x})

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

Equations

ideal.quot_torsion_of_equiv_span_singleton R M x = (linear_map.to_span_singleton R M x).quot_ker_equiv_range.trans (linear_equiv.of_eq (linear_map.range (linear_map.to_span_singleton R M x)) (submodule.span R {x}) _)

source

@[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) :

⇑(ideal.quot_torsion_of_equiv_span_singleton R M x) (submodule.quotient.mk a) = a • ⟨x, _⟩

source

def submodule.torsion_by (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :

submodule R M

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

Equations

submodule.torsion_by R M a = linear_map.ker (distrib_mul_action.to_linear_map R M a)

Instances for ↥submodule.torsion_by

source

@[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) :

(submodule.torsion_by R M a).carrier = ⇑(distrib_mul_action.to_linear_map R M a) ⁻¹' {0}

source

@[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)

source

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) :

submodule R M

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

Equations

submodule.torsion_by_set R M s = has_Inf.Inf (submodule.torsion_by R M '' s)

Instances for ↥submodule.torsion_by_set

source

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] :

submodule R M

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

Equations

submodule.torsion' R M S = {carrier := {x : M | ∃ (a : S), a • x = 0}, add_mem' := _, zero_mem' := _, smul_mem' := _}

Instances for ↥submodule.torsion'

source

@[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}

source

@[reducible]

def submodule.torsion (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

submodule 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

submodule.torsion R M = submodule.torsion' R M ↥(non_zero_divisors R)

source

@[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

module.is_torsion_by R M a = ∀ ⦃x : M⦄, a • x = 0

source

@[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

module.is_torsion_by_set R M s = ∀ ⦃x : M⦄ ⦃a : ↥s⦄, ↑a • x = 0

source

@[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

module.is_torsion' M S = ∀ ⦃x : M⦄, ∃ (a : S), a • x = 0

source

@[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

module.is_torsion R M = ∀ ⦃x : M⦄, ∃ (a : ↥(non_zero_divisors R)), a • x = 0

source

@[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

source

@[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

source

@[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) :

x ∈ submodule.torsion_by R M a ↔ a • x = 0

source

@[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

source

@[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) :

submodule.torsion_by_set R M {a} = submodule.torsion_by R M a

source

theorem submodule.torsion_by_set_le_torsion_by_set_of_subset {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {s t : set R} (st : s ⊆ t) :

submodule.torsion_by_set R M t ≤ submodule.torsion_by_set R M s

source

theorem submodule.torsion_by_set_eq_torsion_by_span {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 = submodule.torsion_by_set R M ↑(ideal.span s)

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

source

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

submodule.torsion_by_set R M ↑(submodule.span R {a}) = submodule.torsion_by R M a

source

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) :

submodule.torsion_by R M a ≤ submodule.torsion_by R M b

source

@[simp]

theorem submodule.torsion_by_one {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

submodule.torsion_by R M 1 = ⊥

source

@[simp]

theorem submodule.torsion_by_univ {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

submodule.torsion_by_set R M set.univ = ⊥

source

@[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) :

module.is_torsion_by_set R M {a} ↔ module.is_torsion_by R M a

source

theorem module.is_torsion_by_set_iff_torsion_by_set_eq_top {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) :

module.is_torsion_by_set R M s ↔ submodule.torsion_by_set R M s = ⊤

source

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) :

module.is_torsion_by R M a ↔ submodule.torsion_by R M a = ⊤

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

source

theorem module.is_torsion_by_set_iff_is_torsion_by_span {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (s : set R) :

module.is_torsion_by_set R M s ↔ module.is_torsion_by_set R M ↑(ideal.span s)

source

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

module.is_torsion_by_set R M ↑(submodule.span R {a}) ↔ module.is_torsion_by R M a

source

theorem submodule.torsion_by_set_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) :

module.is_torsion_by_set R ↥(submodule.torsion_by_set R M s) s

source

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) :

module.is_torsion_by R ↥(submodule.torsion_by R M a) a

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

source

@[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) :

submodule.torsion_by R ↥(submodule.torsion_by R M a) a = ⊤

source

@[simp]

theorem submodule.torsion_by_set_torsion_by_set_eq_top {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 ↥(submodule.torsion_by_set R M s) s = ⊤

source

theorem submodule.torsion_gc (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

galois_connection submodule.annihilator (λ (I : (ideal R)ᵒᵈ), submodule.torsion_by_set R M ↑(⇑order_dual.of_dual I))

source

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)

source

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))

source

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))

source

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))

source

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)) :

direct_sum.is_internal (λ (i : ↥S), submodule.torsion_by_set R M ↑(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.

source

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))) :

direct_sum.is_internal (λ (i : ↥S), submodule.torsion_by R M (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.

source

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

hM.has_smul = {smul := λ (b : R ⧸ I) (x : M), quotient.lift_on' b (λ (_x : R), _x • x) _}

source

@[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) :

⇑(ideal.quotient.mk I) b • x = b • x

source

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

hM.module = function.surjective.module_left (ideal.quotient.mk I) ideal.quotient.mk_surjective _

source

@[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] :

is_scalar_tower S (R ⧸ I) M

source

@[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

module.has_quotient.quotient.module = module.is_torsion_by_set.module module.has_quotient.quotient.module._proof_1

source

@[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) :

module (R ⧸ I) ↥(submodule.torsion_by_set R M ↑I)

Equations

submodule.torsion_by_set.module I = _.module

source

@[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)) :

⇑(ideal.quotient.mk I) b • x = b • x

source

@[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] :

is_scalar_tower S (R ⧸ I) ↥(submodule.torsion_by_set R M ↑I)

source

@[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) :

module (R ⧸ submodule.span R {a}) ↥(submodule.torsion_by R M a)

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

Equations

submodule.torsion_by.module a = _.module

source

@[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)) :

⇑(ideal.quotient.mk (submodule.span R {a})) b • x = b • x

source

@[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] :

is_scalar_tower S (R ⧸ submodule.span R {a}) ↥(submodule.torsion_by R M a)

source

@[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

source

@[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

source

@[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] :

has_smul S ↥(submodule.torsion' R M S)

Equations

submodule.torsion'.has_smul S = {smul := λ (s : S) (x : ↥(submodule.torsion' R M S)), ⟨s • ↑x, _⟩}

source

@[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

source

@[protected, instance]

def submodule.torsion'.distrib_mul_action {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] :

distrib_mul_action S ↥(submodule.torsion' R M S)

Equations

submodule.torsion'.distrib_mul_action S = function.injective.distrib_mul_action (submodule.torsion' R M S).subtype.to_add_monoid_hom _ _

source

@[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] :

smul_comm_class S R ↥(submodule.torsion' R M S)

source

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] :

module.is_torsion' M S ↔ submodule.torsion' R M S = ⊤

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

source

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] :

module.is_torsion' ↥(submodule.torsion' R M S) S

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

source

@[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] :

submodule.torsion' R ↥(submodule.torsion' R M S) S = ⊤

source

@[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] :

submodule.torsion R ↥(submodule.torsion R M) = ⊤

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

source

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

module.is_torsion R ↥(submodule.torsion R M)

The torsion submodule is always a torsion module.

source

theorem module.is_torsion_by_set_annihilator_top (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

module.is_torsion_by_set R M ↑(⊤.annihilator)

source

theorem submodule.annihilator_top_inter_non_zero_divisors {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] [module.finite R M] (hM : module.is_torsion R M) :

↑(⊤.annihilator) ∩ ↑(non_zero_divisors R) ≠ ∅

source

theorem submodule.coe_torsion_eq_annihilator_ne_bot {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] [nontrivial R] :

↑(submodule.torsion R M) = {x : M | (submodule.span R {x}).annihilator ≠ ⊥}

source

theorem submodule.no_zero_smul_divisors_iff_torsion_eq_bot {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] [no_zero_divisors R] [nontrivial R] :

no_zero_smul_divisors R M ↔ submodule.torsion R M = ⊥

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

source

@[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] :

submodule.torsion R (M ⧸ submodule.torsion R M) = ⊥

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

source

@[protected, instance]

def submodule.quotient_torsion.no_zero_smul_divisors {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] [is_domain R] :

no_zero_smul_divisors R (M ⧸ submodule.torsion R M)

source

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

source

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

submodule.p_order hM x = nat.find _

source

@[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)] :

p ^ submodule.p_order hM x • x = 0

source

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))

source

theorem ideal.quotient.torsion_by_eq_span_singleton {R : Type u_1} [comm_ring R] (a b : R) (ha : a ∈ non_zero_divisors R) :

submodule.torsion_by R (R ⧸ submodule.span R {a * b}) a = submodule.span R {⇑(ideal.quotient.mk (submodule.span R {a * b})) b}

source

theorem add_monoid.is_torsion_iff_is_torsion_nat {M : Type u_2} [add_comm_monoid M] :

add_monoid.is_torsion M ↔ module.is_torsion ℕ M

source

theorem add_monoid.is_torsion_iff_is_torsion_int {M : Type u_2} [add_comm_group M] :

add_monoid.is_torsion M ↔ module.is_torsion ℤ M