Torsion-free modules

This files defines a torsion-free R-(semi)module M as a (semi)module where scalar multiplication by a regular element r : R is injective as a map M → M.

In the case of a module (group over a ring), this is equivalent to saying that r • m = 0 for some r : R, m : M implies that r is a zero-divisor. If furthermore the base ring is a domain, this is equivalent to the naïve r • m = 0 ↔ r = 0 ∨ m = 0 definition.

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

An 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. See smul_eq_zero.

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

theorem IsRegular.isSMulRegular {R : Type u_1} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.IsTorsionFree R M] ⦃r : R⦄ : IsRegular r → IsSMulRegular M r

Alias of Module.IsTorsionFree.isSMulRegular.

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

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

theorem Function.Injective.moduleIsTorsionFree {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.IsTorsionFree R N] (f : M → N) (hf : Injective f) (smul : ∀ (r : R) (m : M), f (r • m) = r • f m) : Module.IsTorsionFree R M

Pullback an IsTorsionFree instance along an injective function.

theorem Module.IsTorsionFree.comap {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [IsTorsionFree S M] (f : R → S) (isRegular : ∀ (r : R), IsRegular r → IsRegular (f r)) (smul : ∀ (r : R) (m : M), f r • m = r • m) : IsTorsionFree R M

Pullback an IsTorsionFree instance along a function preserving scalar multiplication and regular elements.

instance IsAddTorsionFree.to_isTorsionFree_nat {M : Type u_3} [AddCommMonoid M] [IsAddTorsionFree M] : Module.IsTorsionFree ℕ M

instance Subsingleton.to_moduleIsTorsionFree {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : Module.IsTorsionFree R M

theorem IsRegular.smul_right_injective {R : Type u_1} (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {r : R} [Module.IsTorsionFree R M] (hr : IsRegular r) : Function.Injective fun (x : M) => r • x

@[simp]

theorem IsRegular.smul_right_inj {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m₁ m₂ : M} [Module.IsTorsionFree R M] (hr : IsRegular r) : r • m₁ = r • m₂ ↔ m₁ = m₂

@[simp]

theorem IsRegular.smul_eq_zero_iff_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] (hr : IsRegular r) : r • m = 0 ↔ m = 0

theorem IsRegular.smul_ne_zero_iff_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] (hr : IsRegular r) : r • m ≠ 0 ↔ m ≠ 0

theorem Module.IsTorsionFree.trans (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [IsTorsionFree R M] [Module S R] [IsTorsionFree S R] [IsScalarTower S R R] [SMulCommClass S R R] [IsScalarTower S R M] : IsTorsionFree S M

theorem IsSMulRegular.of_ne_zero {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) : IsSMulRegular M r

theorem smul_right_injective {R : Type u_1} (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {r : R} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) : Function.Injective fun (x : M) => r • x

@[simp]

theorem smul_right_inj {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m₁ m₂ : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) : r • m₁ = r • m₂ ↔ m₁ = m₂

theorem smul_eq_zero_iff_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) : r • m = 0 ↔ m = 0

theorem smul_ne_zero_iff_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) : r • m ≠ 0 ↔ m ≠ 0

@[simp]

theorem smul_eq_zero {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] : r • m = 0 ↔ r = 0 ∨ m = 0

theorem smul_ne_zero_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] : r • m ≠ 0 ↔ r ≠ 0 ∧ m ≠ 0

theorem smul_ne_zero {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hr : r ≠ 0) (hm : m ≠ 0) : r • m ≠ 0

theorem smul_eq_zero_iff_left {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hm : m ≠ 0) : r • m = 0 ↔ r = 0

theorem smul_ne_zero_iff_left {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} {m : M} [Module.IsTorsionFree R M] [IsCancelMulZero R] (hm : m ≠ 0) : r • m ≠ 0 ↔ r ≠ 0

theorem IsAddTorsionFree.of_isTorsionFree (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Module.IsTorsionFree R M] [IsCancelMulZero R] [CharZero R] : IsAddTorsionFree M

@[instance 100]

instance IsAddTorsionFree.of_isDomain_charZero {R : Type u_1} [Semiring R] [IsCancelMulZero R] [CharZero R] : IsAddTorsionFree R

A characteristic zero domain is torsion-free.

@[simp]

theorem Module.isTorsionFree_nat_iff_isAddTorsionFree {M : Type u_3} [AddCommMonoid M] : IsTorsionFree ℕ M ↔ IsAddTorsionFree M

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

@[simp]

theorem Module.isTorsionFree_int_iff_isAddTorsionFree {M : Type u_3} [AddCommGroup M] : IsTorsionFree ℤ M ↔ IsAddTorsionFree M

@[simp]

theorem isLeftRegular_natCast {R : Type u_1} [NonAssocSemiring R] {n : ℕ} : IsLeftRegular ↑n ↔ IsSMulRegular R n

@[simp]

theorem isRightRegular_natCast {R : Type u_1} [NonAssocSemiring R] {n : ℕ} : IsRightRegular ↑n ↔ IsSMulRegular R n

@[simp]

theorem isRegular_natCast {R : Type u_1} [NonAssocSemiring R] {n : ℕ} : IsRegular ↑n ↔ IsSMulRegular R n

theorem Module.IsTorsionFree.of_smul_eq_zero {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] (h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0) : IsTorsionFree R M

theorem Module.isTorsionFree_iff_smul_eq_zero {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] : IsTorsionFree R M ↔ ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0

theorem smul_left_injective (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {m : M} [IsCancelMulZero R] [Module.IsTorsionFree R M] (hm : m ≠ 0) : Function.Injective fun (x : R) => x • m

@[simp]

theorem smul_left_inj {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {m : M} {r₁ r₂ : R} [IsCancelMulZero R] [Module.IsTorsionFree R M] (hm : m ≠ 0) : r₁ • m = r₂ • m ↔ r₁ = r₂

theorem CharZero.of_isAddTorsionFree (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommGroup M] [Module R M] [Nontrivial M] [IsAddTorsionFree M] : CharZero R

Only a ring of characteristic zero can have a non-trivial module without additive or scalar torsion.

theorem isSelfNeg_of_isSMulRegular_two {R : Type u_1} [NonAssocRing R] (h : IsSMulRegular R 2) {a : R} : IsSelfNeg a ↔ a = 0