NoZeroSMulDivisors

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

TODO

NoZeroSMulDivisors is mathematically incorrect for semimodules. Replace it with a new typeclass Module.IsTorsionFree, cf https://github.com/kbuzzard/ClassFieldTheory. Torsion-free monoids have seen the same change happen already.

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.