NoZeroSMulDivisors

This file defines the NoZeroSMulDivisors class, and includes some tests for the vanishing of elements (especially in modules over division rings).

Usage notes

NoZeroSMulDivisors R M is mathematically wrong when R isn't a domain, and one should use Module.IsTorsionFree R M instead whenever they are equivalent.

In fact, if M is non-trivial, NoZeroSMulDivisors R M implies NoZeroDivisors R (which in turn implies IsDomain R if R is a non-trivial ring): Take m : M is non-zero. Assume r s : R are such that r * s = 0. Then r • s • m = (r * s) • m = 0, so by NoZeroSMulDivisors we get r = 0 ∨ s = 0 ∨ m = 0. But m ≠ 0, so r = 0 ∨ s = 0, as wanted.

Therefore one should only use NoZeroSMulDivisors R M when R isn't a ring or if the zero module and ring are somehow relevant.

Note that we might get rid of NoZeroSMulDivisors entirely in the future. See https://github.com/leanprover-community/mathlib4/pull/33909.

class NoZeroSMulDivisors (R : Type u_4) (M : Type u_5) [Zero R] [Zero M] [SMul R M] : Prop

NoZeroSMulDivisors R M states that a scalar multiple is 0 only if either argument is 0. This is a version of saying that M is torsion free, without assuming R is zero-divisor free.

The main application of NoZeroSMulDivisors R M, when M is a module, is the result smul_eq_zero: a scalar multiple is 0 iff either argument is 0.

It is a generalization of the NoZeroDivisors class to heterogeneous multiplication.

• eq_zero_or_eq_zero_of_smul_eq_zero {c : R} {x : M} : c • x = 0 → c = 0 ∨ x = 0

  If scalar multiplication yields zero, either the scalar or the vector was zero.

theorem noZeroSMulDivisors_iff (R : Type u_4) (M : Type u_5) [Zero R] [Zero M] [SMul R M] : NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

theorem Function.Injective.noZeroSMulDivisors {R : Type u_4} {M : Type u_5} {N : Type u_6} [Zero R] [Zero M] [Zero N] [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M

Pullback a NoZeroSMulDivisors instance along an injective function.

@[instance 100]

instance NoZeroDivisors.toNoZeroSMulDivisors {R : Type u_1} [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R

theorem smul_ne_zero {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0

theorem noZeroSMulDivisors_iff_right_eq_zero_of_smul {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMul R M] : NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

@[simp]

theorem smul_eq_zero {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem smul_ne_zero_iff {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

theorem smul_eq_zero_iff_left {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x = 0 ↔ c = 0

theorem smul_eq_zero_iff_right {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_left {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

theorem smul_ne_zero_iff_right {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

instance IsAddTorsionFree.to_noZeroSMulDivisors_nat {M : Type u_2} [AddMonoid M] [IsAddTorsionFree M] : NoZeroSMulDivisors ℕ M

instance IsAddTorsionFree.to_noZeroSMulDivisors_int {G : Type u_3} [AddGroup G] [IsAddTorsionFree G] : NoZeroSMulDivisors ℤ G

@[simp]

theorem noZeroSMulDivisors_nat_iff_isAddTorsionFree {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℕ G ↔ IsAddTorsionFree G

@[simp]

theorem noZeroSMulDivisors_int_iff_isAddTorsionFree {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℤ G ↔ IsAddTorsionFree G

theorem IsAddTorsionFree.of_noZeroSMulDivisors_nat {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℕ G → IsAddTorsionFree G

Alias of the forward direction of noZeroSMulDivisors_nat_iff_isAddTorsionFree.

theorem IsAddTorsionFree.of_noZeroSMulDivisors_int {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℤ G → IsAddTorsionFree G

Alias of the forward direction of noZeroSMulDivisors_int_iff_isAddTorsionFree.