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

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

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_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 • { val := x, property := ⋯ }

@[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.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.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.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.torsion'AddSubMonoid_coe (M : Type u_2) [AddCommMonoid M] (S : Type w) [CommMonoid S] [DistribMulAction S M] : ↑(Submodule.torsion'AddSubMonoid M S) = {x : M | ∃ (a : S), a • x = 0}

def Submodule.torsion'AddSubMonoid (M : Type u_2) [AddCommMonoid M] (S : Type w) [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 = { toAddSubsemigroup := { carrier := {x : M | ∃ (a : S), a • x = 0}, add_mem' := ⋯ }, zero_mem' := ⋯ }

@[simp]

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

@[reducible]

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

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

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

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

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

@[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 : Set R} {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 : R) (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 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 : Set.Pairwise ↑S 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 : Set.Pairwise ↑S fun (i j : ι) => p i ⊔ p j = ⊤) : Finset.SupIndep S 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 : Set.Pairwise (↑S) (IsCoprime on q)) : ⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (Finset.prod S fun (i : ι) => 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 : Set.Pairwise (↑S) (IsCoprime on q)) : Finset.SupIndep S 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 : Set.Pairwise ↑S 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 : Set.Pairwise (↑S) (IsCoprime on q)) (hM : Module.IsTorsionBy R M (Finset.prod S fun (i : ι) => 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

• Module.IsTorsionBySet.hasSMul hM = { smul := fun (b : R ⧸ I) (x : M) => Quotient.liftOn' b (fun (x_1 : R) => x_1 • x) ⋯ }

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

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

• Module.IsTorsionBySet.module hM = 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

• ⋯ = ⋯

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 modle over the quotient of the ring by the annihilator. Not an instance because it causes synthesis failures / timeouts.

Equations

• Module.quotientAnnihilator = Module.IsTorsionBySet.module ⋯

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

Equations

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

instance Submodule.instModuleQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringSubtypeMemSubmoduleToAddCommMonoidInstMembershipSetLikeTorsionBySetCoeSetLikeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleCommRingAddCommMonoid {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

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

@[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.instIsScalarTowerQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringSubtypeMemSubmoduleToAddCommMonoidInstMembershipSetLikeTorsionBySetCoeSetLikeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleInstSMul'ToRingToAddCommGroupToSMulZeroToSMulZeroClassInstZeroQuotientSubmoduleToSemiringToAddCommMonoidHasQuotientToSMulWithZeroToMonoidWithZeroCommRingToMulActionWithZeroAddCommMonoidInstModuleQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringSubtypeMemSubmoduleToAddCommMonoidInstMembershipSetLikeTorsionBySetCoeSetLikeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleCommRingAddCommMonoidSmul {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.IsTorsionBySet.module ⋯

instance Submodule.instModuleQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringSpanSingletonSetInstSingletonSetSubtypeMemSubmoduleToAddCommMonoidInstMembershipSetLikeTorsionByCommRingAddCommMonoid {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

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

@[simp]

theorem Submodule.torsionBy.mk_ideal_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) (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 : R) (b : R) (x : ↥(Submodule.torsionBy R M a)) : (Ideal.Quotient.mk (Submodule.span R {a})) b • x = b • x

instance Submodule.instIsScalarTowerQuotientSubmoduleToSemiringToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleInstHasQuotientIdealToSemiringToCommSemiringSpanSingletonSetInstSingletonSetSubtypeMemSubmoduleToAddCommMonoidInstMembershipSetLikeTorsionByInstSMul'ToRingToAddCommGroupToSMulZeroToSMulZeroClassInstZeroQuotientSubmoduleToSemiringToAddCommMonoidHasQuotientToSMulWithZeroToMonoidWithZeroCommRingToMulActionWithZeroAddCommMonoidInstModuleQuotientTorsionBySmul {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

@[simp]

theorem Submodule.instSMulSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion'_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.instSMulSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion' {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.instSMulSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion' S = { smul := fun (s : S) (x : ↥(Submodule.torsion' R M S)) => { val := s • ↑x, property := ⋯ } }

instance Submodule.instDistribMulActionSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion'ToMonoidToAddMonoidToAddMonoidToAddSubmonoid {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

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

instance Submodule.instSMulCommClassSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion'InstSMulSubtypeMemSubmoduleToSemiringInstMembershipSetLikeTorsion'SmulToSMulIdToSMulToZeroToAddMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToMulActionWithZeroLeftToMonoidToMulAction {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 ↑(Submodule.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) : ↑(Submodule.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.annihilator (Submodule.span R {x}) ≠ ⊥}

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.toAddSubgroup (Submodule.torsion ℤ G) = 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 : R) (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