Mathlib.Algebra.NoZeroSMulDivisors.Defs

NoZeroSMulDivisors structure

(R M : Type*) [Zero R] [Zero M] [SMul R M]

Full source

/-- `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.
-/
@[mk_iff]
class NoZeroSMulDivisors (R M : Type*) [Zero R] [Zero M] [SMul R M] : Prop where
  /-- If scalar multiplication yields zero, either the scalar or the vector was zero. -/
  eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

No Zero Scalar Multipliers Condition

Informal description

The structure `NoZeroSMulDivisors R M` asserts that for a scalar multiplication operation `• : R → M → M`, the equation `r • x = 0` holds if and only if either `r = 0` or `x = 0`. This generalizes the notion of having no zero divisors to heterogeneous multiplication, ensuring that the module `M` is torsion-free without requiring `R` to be free of zero divisors.

Function.Injective.noZeroSMulDivisors theorem

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

Full source

/-- Pullback a `NoZeroSMulDivisors` instance along an injective function. -/
theorem Function.Injective.noZeroSMulDivisors {R M N : Type*} [Zero R] [Zero M] [Zero N]
    [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f)
    (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M :=
  ⟨fun {_ _} h =>
    Or.imp_right (@hf _ _) <| h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [← hs, h, h0])⟩

Inheritance of No-Zero-Scalar-Multipliers Property via Injective Linear Map

Informal description

Let $R$, $M$, and $N$ be types with zero elements, equipped with scalar multiplication operations $R \times M \to M$ and $R \times N \to N$. Suppose $N$ satisfies the condition that $r \cdot x = 0$ implies $r = 0$ or $x = 0$ for any $r \in R$ and $x \in N$. Given an injective function $f : M \to N$ such that $f(0) = 0$ and $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in M$, then $M$ also satisfies the same no-zero-scalar-multipliers condition.

NoZeroDivisors.toNoZeroSMulDivisors instance

[Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R

Full source

instance (priority := 100) NoZeroDivisors.toNoZeroSMulDivisors [Zero R] [Mul R]
    [NoZeroDivisors R] : NoZeroSMulDivisors R R :=
  ⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩

No Zero Divisors Implies No Zero Scalar Multipliers

Informal description

For any type $R$ with a zero element and a multiplication operation, if $R$ has no zero divisors, then the scalar multiplication operation on $R$ (defined via multiplication) satisfies the condition that $r \• x = 0$ implies $r = 0$ or $x = 0$.

smul_ne_zero theorem

[Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0

Full source

theorem smul_ne_zero [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
    (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 := fun h =>
  (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx

Nonzero Scalar Multiplication of Nonzero Elements is Nonzero

Informal description

Let $R$ and $M$ be types with zero elements and equipped with a scalar multiplication operation $• : R \to M \to M$. If $R$ and $M$ satisfy the `NoZeroSMulDivisors` condition, then for any nonzero scalar $c \in R$ and any nonzero element $x \in M$, the scalar multiplication $c • x$ is also nonzero.

smul_eq_zero theorem

: c • x = 0 ↔ c = 0 ∨ x = 0

Full source

@[simp]
theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
  ⟨eq_zero_or_eq_zero_of_smul_eq_zero, fun h =>
    h.elim (fun h => h.symm ▸ zero_smul R x) fun h => h.symm ▸ smul_zero c⟩

Vanishing Condition for Scalar Multiplication: $c • x = 0 \leftrightarrow c = 0 \lor x = 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ where $R$ and $M$ have zero elements, the scalar product $c • x$ equals zero if and only if either $c = 0$ or $x = 0$.

smul_ne_zero_iff theorem

: c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

Full source

theorem smul_ne_zero_iff : c • x ≠ 0c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [Ne, smul_eq_zero, not_or]

Nonzero Scalar Multiplication Condition: $c • x \neq 0 \leftrightarrow c \neq 0 \land x \neq 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ where $R$ and $M$ have zero elements, the scalar product $c • x$ is nonzero if and only if both $c \neq 0$ and $x \neq 0$.

smul_eq_zero_iff_left theorem

(hx : x ≠ 0) : c • x = 0 ↔ c = 0

Full source

lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0 := by simp [hx]

Nonzero Element Scalar Multiplication Vanishing Condition: $c • x = 0 \leftrightarrow c = 0$ for $x \neq 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ where $R$ and $M$ have zero elements, if $x \in M$ is nonzero, then $c • x = 0$ if and only if $c = 0$.

smul_eq_zero_iff_right theorem

(hc : c ≠ 0) : c • x = 0 ↔ x = 0

Full source

lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0 := by simp [hc]

Nonzero Scalar Multiplication Vanishing Condition: $c • x = 0 \leftrightarrow x = 0$ for $c \neq 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ where $R$ and $M$ have zero elements, if $c \in R$ is nonzero, then $c • x = 0$ if and only if $x = 0$.

smul_ne_zero_iff_left theorem

(hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

Full source

lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0c • x ≠ 0 ↔ c ≠ 0 := by simp [hx]

Nonzero Scalar Multiplication Condition: $c • x \neq 0 \leftrightarrow c \neq 0$ for $x \neq 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ where $R$ and $M$ have zero elements, if $x \in M$ is nonzero, then $c • x \neq 0$ if and only if $c \in R$ is nonzero.

smul_ne_zero_iff_right theorem

(hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

Full source

lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0c • x ≠ 0 ↔ x ≠ 0 := by simp [hc]

Nonzero Scalar Multiplication Condition: $c • x \neq 0 \leftrightarrow x \neq 0$ for $c \neq 0$

Informal description

For a scalar multiplication operation $• : R \times M \to M$ with $R$ and $M$ having zero elements, if $c \in R$ is nonzero, then $c • x \neq 0$ if and only if $x \in M$ is nonzero.