Torsion submodules

Main definitions

• torsionOf R M x : the torsion ideal of x, containing all a such that a • x = 0.
• Submodule.torsionBy R M a : the a-torsion submodule, containing all elements x of M such that a • x = 0.
• Submodule.torsionBySet 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 submodule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.
• Module.IsTorsionBy R M a : the property that defines an a-torsion module. Similarly, IsTorsionBySet, IsTorsion' and IsTorsion.
• Module.IsTorsionBySet.module : Creates an R ⧸ I-module from an R-module that IsTorsionBySet R _ I.

Main statements

• quot_torsionOf_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.
• torsionBySet_eq_torsionBySet_span : torsion by a set is torsion by the ideal generated by it.
• Submodule.torsionBy_is_torsionBy : the a-torsion submodule is an a-torsion module. Similar lemmas for torsion' and torsion.
• Submodule.torsionBy_isInternal : 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.torsionBySet_is_internal.
• Submodule.noZeroSMulDivisors_iff_torsion_bot : a module over a domain has NoZeroSMulDivisors (that is, there is no non-zero a, x such that a • x = 0) iff its torsion submodule is trivial.
• Submodule.QuotientTorsion.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.QuotientTorsion.noZeroSMulDivisors : NoZeroSMulDivisors R (M ⧸ torsion R M).

Notation

• The notions are defined for a CommSemiring 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

def Ideal.torsionOf (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : Ideal R

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

Equations

• Ideal.torsionOf R M x = LinearMap.ker (LinearMap.toSpanSingleton R M x)

@[simp]

theorem Ideal.torsionOf_carrier (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑(Ideal.torsionOf R M x) = ⇑(LinearMap.toSpanSingleton R M x) ⁻¹' {0}

@[simp]

theorem Ideal.torsionOf_zero (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Ideal.torsionOf R M 0 = ⊤

@[simp]

theorem Ideal.mem_torsionOf_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (a : R) : a ∈ Ideal.torsionOf R M x ↔ a • x = 0

@[simp]

theorem Ideal.torsionOf_eq_top_iff (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) : Ideal.torsionOf R M m = ⊤ ↔ m = 0

@[simp]

theorem Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] (m : M) : Ideal.torsionOf R M m = ⊥ ↔ m ≠ 0

theorem Ideal.CompleteLattice.Independent.linear_independent' {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] (hv : CompleteLattice.Independent fun (i : ι) => Submodule.span R {v i}) (h_ne_zero : ∀ (i : ι), Ideal.torsionOf R M (v i) = ⊥) : LinearIndependent R v

See also CompleteLattice.Independent.linearIndependent which provides the same conclusion but requires the stronger hypothesis NoZeroSMulDivisors R M.

noncomputable def Ideal.quotTorsionOfEquivSpanSingleton (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (x : M) : (R ⧸ Ideal.torsionOf 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.quotTorsionOfEquivSpanSingleton_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (x : M) (a : R) : (Ideal.quotTorsionOfEquivSpanSingleton R M x) (Submodule.Quotient.mk a) = a • ⟨x, ⋯⟩

def Submodule.torsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid 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.torsionBy R M a = LinearMap.ker (DistribMulAction.toLinearMap R M a)

@[simp]

theorem Submodule.torsionBy_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : ↑(Submodule.torsionBy R M a) = ⇑(DistribMulAction.toLinearMap R M a) ⁻¹' {0}

def Submodule.torsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid 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.torsionBySet R M s = sInf (Submodule.torsionBy R M '' s)

@[simp]

theorem Submodule.torsionBySet_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : ↑(Submodule.torsionBySet R M s) = ⋂ y ∈ s, ⇑(DistribMulAction.toLinearMap R M y) ⁻¹' {0}

def Submodule.torsion'AddSubMonoid (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] : AddSubmonoid M

The additive submonoid of all elements x of M such that a • x = 0 for some a in S.

Equations

• Submodule.torsion'AddSubMonoid M S = { carrier := {x : M | ∃ (a : S), a • x = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Submodule.coe_torsion'AddSubMonoid (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] : ↑(Submodule.torsion'AddSubMonoid M S) = {x : M | ∃ (a : S), a • x = 0}

def Submodule.torsion' (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass 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 = { toAddSubmonoid := Submodule.torsion'AddSubMonoid M S, smul_mem' := ⋯ }

@[simp]

theorem Submodule.torsion'_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : ↑(Submodule.torsion' R M S) = {x : M | ∃ (a : S), a • x = 0}

@[reducible, inline]

abbrev Submodule.torsion (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid 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 ↥(nonZeroDivisors R)

@[reducible, inline]

abbrev Module.IsTorsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Prop

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

Equations

• Module.IsTorsionBy R M a = ∀ ⦃x : M⦄, a • x = 0

@[reducible, inline]

abbrev Module.IsTorsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Prop

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

Equations

• Module.IsTorsionBySet R M s = ∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0

@[reducible, inline]

abbrev Module.IsTorsion' (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [SMul S M] : Prop

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

Equations

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

@[reducible, inline]

abbrev Module.IsTorsion (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid 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.IsTorsion R M = ∀ ⦃x : M⦄, ∃ (a : ↥(nonZeroDivisors R)), a • x = 0

theorem Module.isTorsionBySet_annihilator (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.IsTorsionBySet R M ↑(Module.annihilator R M)

theorem isSMulRegular_iff_torsionBy_eq_bot {R : Type u_2} (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : IsSMulRegular M r ↔ Submodule.torsionBy R M r = ⊥

@[simp]

theorem Submodule.smul_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : ↥(Submodule.torsionBy R M a)) : a • x = 0

@[simp]

theorem Submodule.smul_coe_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : ↥(Submodule.torsionBy R M a)) : a • ↑x = 0

@[simp]

theorem Submodule.mem_torsionBy_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : M) : x ∈ Submodule.torsionBy R M a ↔ a • x = 0

@[simp]

theorem Submodule.mem_torsionBySet_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (x : M) : x ∈ Submodule.torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0

@[simp]

theorem Submodule.torsionBySet_singleton_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Submodule.torsionBySet R M {a} = Submodule.torsionBy R M a

theorem Submodule.torsionBySet_le_torsionBySet_of_subset {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {s t : Set R} (st : s ⊆ t) : Submodule.torsionBySet R M t ≤ Submodule.torsionBySet R M s

theorem Submodule.torsionBySet_eq_torsionBySet_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Submodule.torsionBySet R M s = Submodule.torsionBySet R M ↑(Ideal.span s)

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

theorem Submodule.torsionBySet_span_singleton_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Submodule.torsionBySet R M ↑(Submodule.span R {a}) = Submodule.torsionBy R M a

theorem Submodule.torsionBy_le_torsionBy_of_dvd {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : R) (dvd : a ∣ b) : Submodule.torsionBy R M a ≤ Submodule.torsionBy R M b

@[simp]

theorem Submodule.torsionBy_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.torsionBy R M 1 = ⊥

@[simp]

theorem Submodule.torsionBySet_univ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.torsionBySet R M Set.univ = ⊥

@[simp]

theorem Module.isTorsionBySet_singleton_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Module.IsTorsionBySet R M {a} ↔ Module.IsTorsionBy R M a

theorem Module.isTorsionBySet_iff_torsionBySet_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Module.IsTorsionBySet R M s ↔ Submodule.torsionBySet R M s = ⊤

theorem Module.isTorsionBy_iff_torsionBy_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Module.IsTorsionBy R M a ↔ Submodule.torsionBy R M a = ⊤

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

theorem Module.isTorsionBySet_iff_is_torsion_by_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Module.IsTorsionBySet R M s ↔ Module.IsTorsionBySet R M ↑(Ideal.span s)

theorem Module.isTorsionBySet_span_singleton_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Module.IsTorsionBySet R M ↑(Submodule.span R {a}) ↔ Module.IsTorsionBy R M a

theorem Module.isTorsionBySet_iff_subseteq_ker_lsmul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Module.IsTorsionBySet R M s ↔ s ⊆ ↑(LinearMap.ker (LinearMap.lsmul R M))

theorem Module.isTorsionBy_iff_mem_ker_lsmul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Module.IsTorsionBy R M a ↔ a ∈ LinearMap.ker (LinearMap.lsmul R M)

theorem Submodule.torsionBySet_isTorsionBySet {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Module.IsTorsionBySet R (↥(Submodule.torsionBySet R M s)) s

theorem Submodule.torsionBy_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Module.IsTorsionBy R (↥(Submodule.torsionBy R M a)) a

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

@[simp]

theorem Submodule.torsionBy_torsionBy_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : Submodule.torsionBy R (↥(Submodule.torsionBy R M a)) a = ⊤

@[simp]

theorem Submodule.torsionBySet_torsionBySet_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : Submodule.torsionBySet R (↥(Submodule.torsionBySet R M s)) s = ⊤

theorem Submodule.torsion_gc (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : GaloisConnection Submodule.annihilator fun (I : (Ideal R)ᵒᵈ) => Submodule.torsionBySet R M ↑(OrderDual.ofDual I)

theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ι → Ideal R} {S : Finset ι} (hp : (↑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)

theorem Submodule.supIndep_torsionBySet_ideal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ι → Ideal R} {S : Finset ι} (hp : (↑S).Pairwise fun (i j : ι) => p i ⊔ p j = ⊤) : S.SupIndep fun (i : ι) => Submodule.torsionBySet R M ↑(p i)

theorem Submodule.iSup_torsionBy_eq_torsionBy_prod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (IsCoprime on q)) : ⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (∏ i ∈ S, q i)

theorem Submodule.supIndep_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (IsCoprime on q)) : S.SupIndep fun (i : ι) => Submodule.torsionBy R M (q i)

theorem Submodule.torsionBySet_isInternal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {p : ι → Ideal R} (hp : (↑S).Pairwise fun (i j : ι) => p i ⊔ p j = ⊤) (hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)) : DirectSum.IsInternal fun (i : { x : ι // x ∈ S }) => Submodule.torsionBySet 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.

theorem Submodule.torsionBy_isInternal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (IsCoprime on q)) (hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)) : DirectSum.IsInternal fun (i : { x : ι // x ∈ S }) => Submodule.torsionBy 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.

def Module.IsTorsionBySet.hasSMul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M ↑I) : SMul (R ⧸ I) M

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

Equations

• hM.hasSMul = { smul := fun (b : R ⧸ I) (x : M) => ((Submodule.liftQ I (LinearMap.lsmul R M) ⋯) b) x }

@[reducible, inline]

abbrev Module.IsTorsionBy.hasSMul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) : SMul (R ⧸ Ideal.span {r}) M

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

Equations

• hM.hasSMul = ⋯.hasSMul

@[simp]

theorem Module.IsTorsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M ↑I) (b : R) (x : M) : (Ideal.Quotient.mk I) b • x = b • x

@[simp]

theorem Module.IsTorsionBy.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) (b : R) (x : M) : (Ideal.Quotient.mk (Ideal.span {r})) b • x = b • x

def Module.IsTorsionBySet.module {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M ↑I) : Module (R ⧸ I) M

An (R ⧸ I)-module is an R-module which IsTorsionBySet R M I.

Equations

• hM.module = Function.Surjective.moduleLeft (Ideal.Quotient.mk I) ⋯ ⋯

instance Module.IsTorsionBySet.isScalarTower {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M ↑I) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] : IsScalarTower S (R ⧸ I) M

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Module.IsTorsionBy.module {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) : Module (R ⧸ Ideal.span {r}) M

An (R ⧸ Ideal.span {r})-module is an R-module for which IsTorsionBy R M r.

Equations

• hM.module = ⋯.module

def Module.quotientAnnihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : Module (R ⧸ Module.annihilator R M) M

Any module is also a module over the quotient of the ring by the annihilator. Not an instance because it causes synthesis failures / timeouts.

Equations

• Module.quotientAnnihilator = ⋯.module

theorem Module.isTorsionBy_quotient_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : Module.IsTorsionBy R (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N

theorem Module.IsTorsionBy.quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) {r : R} (h : Module.IsTorsionBy R M r) : Module.IsTorsionBy R (M ⧸ N) r

theorem Module.isTorsionBySet_quotient_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (s : Set R) : Module.IsTorsionBySet R (M ⧸ N) s ↔ ∀ (x : M), ∀ r ∈ s, r • x ∈ N

theorem Module.IsTorsionBySet.quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) {s : Set R} (h : Module.IsTorsionBySet R M s) : Module.IsTorsionBySet R (M ⧸ N) s

theorem Module.isTorsionBySet_quotient_set_smul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (s : Set R) : Module.IsTorsionBySet R (M ⧸ s • ⊤) s

theorem Module.isTorsionBy_quotient_element_smul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : Module.IsTorsionBy R (M ⧸ r • ⊤) r

theorem Module.isTorsionBySet_quotient_ideal_smul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : Module.IsTorsionBySet R (M ⧸ I • ⊤) ↑I

instance Module.instQuotientIdealSpanSubmoduleHSMulSetTop {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (s : Set R) : Module (R ⧸ Ideal.span s) (M ⧸ s • ⊤)

Equations

• Module.instQuotientIdealSpanSubmoduleHSMulSetTop M s = ⋯.module

instance Module.instQuotientIdealSubmoduleHSMulTop {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : Module (R ⧸ I) (M ⧸ I • ⊤)

Equations

• Module.instQuotientIdealSubmoduleHSMulTop M I = ⋯.module

instance Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : Module (R ⧸ Ideal.span {r}) (M ⧸ r • ⊤)

Equations

• Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop M r = ⋯.module

theorem Module.Quotient.mk_smul_mk {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (r : R) (m : M) : (Ideal.Quotient.mk I) r • Submodule.Quotient.mk m = Submodule.Quotient.mk (r • m)

instance Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : Module (R ⧸ I) ↥(Submodule.torsionBySet R M ↑I)

Equations

• Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe I = ⋯.module

@[simp]

theorem Submodule.torsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (b : R) (x : ↥(Submodule.torsionBySet R M ↑I)) : (Ideal.Quotient.mk I) b • x = b • x

instance Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] : IsScalarTower S (R ⧸ I) ↥(Submodule.torsionBySet R M ↑I)

Equations

• ⋯ = ⋯

instance Submodule.instModuleQuotientTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Module (R ⧸ Submodule.span R {a}) ↥(Submodule.torsionBy R M a)

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

Equations

• Submodule.instModuleQuotientTorsionBy a = ⋯.module

instance Submodule.instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Module (R ⧸ Ideal.span {a}) ↥(Submodule.torsionBy R M a)

Equations

• Submodule.instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy a = inferInstanceAs (Module (R ⧸ Submodule.span R {a}) ↥(Submodule.torsionBy R M a))

@[simp]

theorem Submodule.torsionBy.mk_ideal_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a b : R) (x : ↥(Submodule.torsionBy R M a)) : (Ideal.Quotient.mk (Ideal.span {a})) b • x = b • x

theorem Submodule.torsionBy.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a b : R) (x : ↥(Submodule.torsionBy R M a)) : (Ideal.Quotient.mk (Submodule.span R {a})) b • x = b • x

instance Submodule.instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] : IsScalarTower S (R ⧸ Submodule.span R {a}) ↥(Submodule.torsionBy R M a)

Equations

• ⋯ = ⋯

def Submodule.submodule_torsionBy_orderIso {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Submodule (R ⧸ Submodule.span R {a}) ↥(Submodule.torsionBy R M a) ≃o Submodule R ↥(Submodule.torsionBy R M a)

Given an R-module M and an element a in R, submodules of the a-torsion submodule of M do not depend on whether we take scalars to be R or R ⧸ R ∙ a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (x : M) : x ∈ Submodule.torsion' R M S ↔ ∃ (a : S), a • x = 0

theorem Submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : x ∈ Submodule.torsion R M ↔ ∃ (a : ↥(nonZeroDivisors R)), a • x = 0

instance Submodule.instSMulSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : SMul S ↥(Submodule.torsion' R M S)

Equations

• Submodule.instSMulSubtypeMemTorsion' S = { smul := fun (s : S) (x : ↥(Submodule.torsion' R M S)) => ⟨s • ↑x, ⋯⟩ }

@[simp]

theorem Submodule.instSMulSubtypeMemTorsion'_smul_coe {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (x : ↥(Submodule.torsion' R M S)) : ↑(s • x) = s • ↑x

instance Submodule.instDistribMulActionSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : DistribMulAction S ↥(Submodule.torsion' R M S)

Equations

• Submodule.instDistribMulActionSubtypeMemTorsion' S = Function.Injective.distribMulAction (Submodule.torsion' R M S).subtype.toAddMonoidHom ⋯ ⋯

instance Submodule.instSMulCommClassSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : SMulCommClass S R ↥(Submodule.torsion' R M S)

Equations

• ⋯ = ⋯

theorem Submodule.isTorsion'_iff_torsion'_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : Module.IsTorsion' M S ↔ Submodule.torsion' R M S = ⊤

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

theorem Submodule.torsion'_isTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : Module.IsTorsion' (↥(Submodule.torsion' R M S)) S

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

@[simp]

theorem Submodule.torsion'_torsion'_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : Submodule.torsion' R (↥(Submodule.torsion' R M S)) S = ⊤

theorem Submodule.torsion_torsion_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid 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.

theorem Submodule.torsion_isTorsion {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.IsTorsion R ↥(Submodule.torsion R M)

The torsion submodule is always a torsion module.

theorem Module.isTorsionBySet_annihilator_top (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.IsTorsionBySet R M ↑⊤.annihilator

theorem Submodule.annihilator_top_inter_nonZeroDivisors {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] (hM : Module.IsTorsion R M) : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅

theorem Submodule.coe_torsion_eq_annihilator_ne_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] [Nontrivial R] : ↑(Submodule.torsion R M) = {x : M | (Submodule.span R {x}).annihilator ≠ ⊥}

theorem Submodule.noZeroSMulDivisors_iff_torsion_eq_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] [Nontrivial R] : NoZeroSMulDivisors R M ↔ Submodule.torsion R M = ⊥

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

theorem Submodule.torsion_int {G : Type u_3} [AddCommGroup G] : (Submodule.torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G

@[simp]

theorem Submodule.QuotientTorsion.torsion_eq_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : Submodule.torsion R (M ⧸ Submodule.torsion R M) = ⊥

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

instance Submodule.QuotientTorsion.noZeroSMulDivisors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] : NoZeroSMulDivisors R (M ⧸ Submodule.torsion R M)

Equations

• ⋯ = ⋯

theorem Submodule.isTorsion'_powers_iff {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (p : R) : Module.IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0

def Submodule.pOrder {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' 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.pOrder hM x = Nat.find ⋯

@[simp]

theorem Submodule.pow_pOrder_smul {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (x : M) [(n : ℕ) → Decidable (p ^ n • x = 0)] : p ^ Submodule.pOrder hM x • x = 0

theorem Submodule.exists_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [(x : M) → Decidable (x = 0)] {p : R} (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (d : ℕ) (hd : d ≠ 0) (s : Fin d → M) (hs : Submodule.span R (Set.range s) = ⊤) : ∃ (j : Fin d), Module.IsTorsionBy R M (p ^ Submodule.pOrder hM (s j))

theorem Ideal.Quotient.torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a ∈ nonZeroDivisors R) : Submodule.torsionBy R (R ⧸ Submodule.span R {a * b}) a = Submodule.span R {(Ideal.Quotient.mk (Submodule.span R {a * b})) b}

theorem AddMonoid.isTorsion_iff_isTorsion_nat {M : Type u_2} [AddCommMonoid M] : AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M

theorem AddMonoid.isTorsion_iff_isTorsion_int {M : Type u_2} [AddCommGroup M] : AddMonoid.IsTorsion M ↔ Module.IsTorsion ℤ M

@[reducible]

def AddSubgroup.torsionBy (A : Type u_3) [AddCommGroup A] (n : ℤ) : AddSubgroup A

The additive n-torsion subgroup for an integer n.

Equations

• AddSubgroup.torsionBy A n = (Submodule.torsionBy ℤ A n).toAddSubgroup

def AddSubgroup.«term_[_]» : Lean.TrailingParserDescr

The additive n-torsion subgroup for an integer n.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubgroup.torsionBy.neg (A : Type u_3) [AddCommGroup A] (n : ℤ) : AddSubgroup.torsionBy A (-n) = AddSubgroup.torsionBy A n

@[simp]

theorem AddSubgroup.torsionBy.nsmul {A : Type u_3} [AddCommGroup A] {n : ℕ} (x : ↥(AddSubgroup.torsionBy A ↑n)) : n • x = 0

theorem AddSubgroup.torsionBy.nsmul_iff {A : Type u_3} [AddCommGroup A] {n : ℕ} {x : A} : x ∈ AddSubgroup.torsionBy A ↑n ↔ n • x = 0

theorem AddSubgroup.torsionBy.mod_self_nsmul {A : Type u_3} [AddCommGroup A] {n : ℕ} (s : ℕ) (x : ↥(AddSubgroup.torsionBy A ↑n)) : s • x = (s % n) • x

theorem AddSubgroup.torsionBy.mod_self_nsmul' {A : Type u_3} [AddCommGroup A] {n : ℕ} (s : ℕ) {x : A} (h : x ∈ AddSubgroup.torsionBy A ↑n) : s • x = (s % n) • x

def AddSubgroup.torsionBy.zmodModule {A : Type u_3} [AddCommGroup A] {n : ℕ} : Module (ZMod n) ↥(AddSubgroup.torsionBy A ↑n)

For a natural number n, the n-torsion subgroup of A is a ZMod n module.

Equations

• AddSubgroup.torsionBy.zmodModule = AddCommGroup.zmodModule ⋯

@[simp]

theorem infinite_range_add_smul_iff {R : Type u_1} {M : Type u_2} [AddCommGroup M] [Ring R] [Module R M] [Infinite R] [NoZeroSMulDivisors R M] (x y : M) : (Set.range fun (r : R) => x + r • y).Infinite ↔ y ≠ 0

@[simp]

theorem infinite_range_add_nsmul_iff {M : Type u_2} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] (x y : M) : (Set.range fun (n : ℕ) => x + n • y).Infinite ↔ y ≠ 0