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_isInternal.
• 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).

TODO

• Move the advanced material to a new file RingTheory.Torsion.
• Replace NoZeroSMulDivisors with Module.IsTorsionFree

Tags

Torsion, submodule, module, quotient

Torsion-free modules

class Module.IsTorsionFree (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

A R-module M is torsion-free if scalar multiplication by an element r : R is injective if multiplication (on R) by r is.

For domains, this is equivalent to the usual condition of r • m = 0 → r = 0 ∨ m = 0. TODO: Prove it.

• isSMulRegular ⦃r : R⦄ : IsRegular r → IsSMulRegular M r

instance Module.instIsTorsionFree {R : Type u_1} [Semiring R] : IsTorsionFree R R

instance Module.instIsTorsionFreeMulOpposite {R : Type u_1} [Semiring R] : IsTorsionFree Rᵐᵒᵖ R

instance Module.instIsTorsionFreeNatOfIsAddTorsionFree {M : Type u_2} [AddCommMonoid M] [IsAddTorsionFree M] : IsTorsionFree ℕ M

instance Module.instIsTorsionFreeIntOfIsAddTorsionFree {M : Type u_2} [AddCommGroup M] [IsAddTorsionFree M] : IsTorsionFree ℤ M

Torsion

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.coe_torsionOf (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑(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] : 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 ∈ 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) : 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) : torsionOf R M m = ⊥ ↔ m ≠ 0

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

See also iSupIndep.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 ⧸ 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) : (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.coe_torsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : ↑(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.coe_torsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : ↑(torsionBySet R M s) = ⋂ y ∈ s, ⇑(DistribMulAction.toLinearMap R M y) ⁻¹' {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 = { carrier := {x : M | ∃ (a : S), a • x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Submodule.coe_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] : ↑(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) [Semiring 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) [Semiring 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) [Semiring 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) [Semiring R] [AddCommMonoid M] [Module R M] : IsTorsionBySet R M ↑(annihilator R M)

theorem Module.isTorsionBy_iff_mem_annihilator (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {a : R} : IsTorsionBy R M a ↔ a ∈ annihilator R M

theorem Module.isTorsionBySet_iff_subset_annihilator (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set R} : IsTorsionBySet R M s ↔ s ⊆ ↑(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 : ↥(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 : ↥(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 ∈ 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 ∈ 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) : torsionBySet R M {a} = 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) : torsionBySet R M t ≤ 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) : torsionBySet R M s = 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) : torsionBySet R M ↑(span R {a}) = 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) : torsionBy R M a ≤ torsionBy R M b

@[simp]

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

@[simp]

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

theorem Module.isTorsionBySet_of_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set R} (h : s ⊆ t) (ht : IsTorsionBySet R M t) : IsTorsionBySet R M s

@[simp]

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

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

theorem Module.isTorsionBySet_span_singleton_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (a : R) : IsTorsionBySet R M ↑(Submodule.span R {a}) ↔ 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) : 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) : 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_subseteq_ker_lsmul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : 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) : 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 (↥(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 (↥(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) : torsionBy R (↥(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) : torsionBySet R (↥(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 annihilator fun (I : (Ideal R)ᵒᵈ) => 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, torsionBySet R M ↑(p i) = 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 : ι) => 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 (Function.onFun IsCoprime q)) : ⨆ i ∈ S, torsionBy R M (q i) = 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 (Function.onFun IsCoprime q)) : S.SupIndep fun (i : ι) => 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 }) => 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 (Function.onFun IsCoprime q)) (hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)) : DirectSum.IsInternal fun (i : { x : ι // x ∈ S }) => 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} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : 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) => ⇑((QuotientAddGroup.lift (Submodule.toAddSubgroup I) (smulAddHom R M) ⋯) b) }

@[reducible, inline]

abbrev Module.IsTorsionBy.hasSMul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {r : R} (hM : 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} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : 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} [Ring R] [AddCommGroup M] [Module R M] {r : R} [(Ideal.span {r}).IsTwoSided] (hM : 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} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : 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} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : 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

def Module.IsTorsionBySet.semilinearMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M ↑I) : have x := hM.module; M →ₛₗ[Ideal.Quotient.mk I] M

If a R-module M is annihilated by a two-sided ideal I, then the identity is a semilinear map from the R-module M to the R ⧸ I-module M.

Equations

• hM.semilinearMap = { toFun := id, map_add' := ⋯, map_smul' := ⋯ }

theorem Module.IsTorsionBySet.isSemisimpleModule_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M ↑I) : have x := hM.module; IsSemisimpleModule (R ⧸ I) M ↔ IsSemisimpleModule R M

@[reducible, inline]

abbrev Module.IsTorsionBy.module {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {r : R} [h : (Ideal.span {r}).IsTwoSided] (hM : 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} [Ring R] [AddCommGroup M] [Module R M] : Module (R ⧸ 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} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsTorsionBy R (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N

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

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

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

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

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

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

Equations

• Module.instQuotientIdealSubmoduleHSMulTop M I = ⋯.module

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

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

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

instance Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : Module (R ⧸ I) ↥(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 : ↥(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) ↥(torsionBySet R M ↑I)

instance Submodule.instModuleQuotientTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Module (R ⧸ span R {a}) ↥(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}) ↥(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 : ↥(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 : ↥(torsionBy R M a)) : (Ideal.Quotient.mk (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 ⧸ span R {a}) ↥(torsionBy R M a)

def Submodule.submodule_torsionBy_orderIso {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Submodule (R ⧸ span R {a}) ↥(torsionBy R M a) ≃o Submodule R ↥(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 ∈ 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 ∈ 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 ↥(torsion' R M S)

Equations

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

@[simp]

theorem Submodule.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 : ↥(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 ↥(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 ↥(torsion' R M S)

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 ↔ 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' (↥(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] : torsion' R (↥(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] : torsion R ↥(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 ↥(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] : 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] : ↑(torsion R M) = {x : M | (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 ↔ 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] : (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] : torsion R (M ⧸ 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 ⧸ torsion R M)

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 ^ 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 : span R (Set.range s) = ⊤) : ∃ (j : Fin d), Module.IsTorsionBy R M (p ^ 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 {(mk (Submodule.span R {a * b})) b}

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

theorem AddMonoid.isTorsion_iff_isTorsion_int {M : Type u_2} [AddCommGroup M] : 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, denoted as A[n].

Equations

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

def AddSubgroup.torsionByStx : Lean.TrailingParserDescr

The additive n-torsion subgroup for an integer n, denoted as A[n].

Equations

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

def AddSubgroup.torsionByUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for torsionBy.

Equations

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

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

@[simp]

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

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

theorem AddSubgroup.torsionBy.mod_self_nsmul {A : Type u_3} [AddCommGroup A] {n : ℕ} (s : ℕ) (x : ↥(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 ∈ torsionBy A ↑n) : s • x = (s % n) • x

def AddSubgroup.torsionBy.zmodModule {A : Type u_3} [AddCommGroup A] {n : ℕ} : Module (ZMod n) ↥(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