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

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

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] [IsDomain R] (hr : r ≠ 0) : IsSMulRegular M r

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

@[instance 100]

instance IsAddTorsionFree.of_isDomain_charZero {R : Type u_1} [Semiring R] [IsDomain 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