Mathlib.Algebra.NoZeroSMulDivisors.Basic

Nat.noZeroSMulDivisors theorem

(R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] : NoZeroSMulDivisors ℕ M

Full source

theorem Nat.noZeroSMulDivisors
    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
    NoZeroSMulDivisors ℕ M where
  eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp

Natural Numbers Have No Zero Scalar Divisors on Modules over Characteristic Zero Semirings

Informal description

Let $R$ be a semiring of characteristic zero, and $M$ be an $R$-module with no zero scalar divisors. Then the natural numbers $\mathbb{N}$ also have no zero scalar divisors when acting on $M$, i.e., for any $n \in \mathbb{N}$ and $m \in M$, if $n \cdot m = 0$ then either $n = 0$ or $m = 0$.

two_nsmul_eq_zero theorem

 (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : 2 • v = 0 ↔ v = 0

Full source

theorem two_nsmul_eq_zero
    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : 2 • v = 0 ↔ v = 0 := by
  haveI := Nat.noZeroSMulDivisors R M
  simp [smul_eq_zero]

Vanishing of Twice an Element in Characteristic Zero Modules without Zero Divisors

Informal description

Let $R$ be a semiring of characteristic zero, and $M$ be an $R$-module with no zero scalar divisors. For any element $v \in M$, we have $2 \cdot v = 0$ if and only if $v = 0$.

CharZero.of_module theorem

(M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R

Full source

/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
zero as well. Usually `M` is an `R`-algebra. -/
theorem CharZero.of_module (M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R := by
  refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
  rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]

Characteristic Zero Transfer from Module to Semiring

Informal description

Let $R$ be a semiring and $M$ be an $R$-module that is also an additive commutative monoid with one. If $M$ has characteristic zero, then $R$ also has characteristic zero.

smul_right_injective theorem

[NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) : Function.Injective (c • · : M → M)

Full source

theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) :
    Function.Injective (c • · : M → M) :=
  (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc

Injectivity of Scalar Multiplication by Nonzero Elements in Modules without Zero Divisors

Informal description

Let $R$ be a semiring and $M$ be a module over $R$ with no zero scalar divisors. For any nonzero scalar $c \in R$, the function $x \mapsto c \cdot x$ is injective on $M$.

smul_right_inj theorem

[NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} : c • x = c • y ↔ x = y

Full source

theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} :
    c • x = c • y ↔ x = y :=
  (smul_right_injective M hc).eq_iff

Injectivity of Scalar Multiplication by Nonzero Elements in Modules without Zero Divisors

Informal description

Let $R$ be a semiring and $M$ be a module over $R$ with no zero scalar divisors. For any nonzero scalar $c \in R$ and any elements $x, y \in M$, we have $c \cdot x = c \cdot y$ if and only if $x = y$.

self_eq_neg theorem

(R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : v = -v ↔ v = 0

Full source

theorem self_eq_neg
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : v = -v ↔ v = 0 := by
  rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]

Element Equals its Negative if and only if Zero in Characteristic Zero Modules without Zero Divisors

Informal description

Let $R$ be a semiring of characteristic zero, and $M$ be an $R$-module with no zero scalar divisors. For any element $v \in M$, we have $v = -v$ if and only if $v = 0$.

neg_eq_self theorem

(R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : -v = v ↔ v = 0

Full source

theorem neg_eq_self
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : -v = v ↔ v = 0 := by
  rw [eq_comm, self_eq_neg R M]

Negation Equals Identity if and only if Zero in Characteristic Zero Modules without Zero Divisors

Informal description

Let $R$ be a semiring of characteristic zero and $M$ be an $R$-module with no zero scalar divisors. For any element $v \in M$, we have $-v = v$ if and only if $v = 0$.

self_ne_neg theorem

(R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : v ≠ -v ↔ v ≠ 0

Full source

theorem self_ne_neg
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : v ≠ -vv ≠ -v ↔ v ≠ 0 :=
  (self_eq_neg R M).not

Non-Zero Element Differs from its Negative in Characteristic Zero Modules without Zero Divisors

Informal description

Let $R$ be a semiring of characteristic zero, and $M$ be an $R$-module with no zero scalar divisors. For any element $v \in M$, we have $v \neq -v$ if and only if $v \neq 0$.

neg_ne_self theorem

(R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : -v ≠ v ↔ v ≠ 0

Full source

theorem neg_ne_self
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : -v ≠ v-v ≠ v ↔ v ≠ 0 :=
  (neg_eq_self R M).not

Non-Equality of Element and its Negative in Characteristic Zero Modules without Zero Divisors

Informal description

Let $R$ be a semiring of characteristic zero and $M$ be an $R$-module with no zero scalar divisors. For any element $v \in M$, we have $-v \neq v$ if and only if $v \neq 0$.

smul_left_injective theorem

{x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x

Full source

theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
  fun c d h =>
  sub_eq_zero.mp
    ((smul_eq_zero.mp
          (calc
            (c - d) • x = c • x - d • x := sub_smul c d x
            _ = 0 := sub_eq_zero.mpr h
            )).resolve_right
      hx)

Injectivity of Scalar Multiplication by Non-Zero Elements

Informal description

Let $R$ be a semiring and $M$ be an $R$-module with no non-trivial zero scalar divisors. For any non-zero element $x \in M$, the scalar multiplication map $c \mapsto c \bullet x$ from $R$ to $M$ is injective.

instNoZeroSMulDivisorsNatOfInt instance

[NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

Full source

instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩

Natural Number Scalar Zero Divisors from Integer Scalar Zero Divisors

Informal description

For any additive commutative group $M$ with no non-trivial integer scalar zero divisors, $M$ also has no non-trivial natural number scalar zero divisors. That is, if $n \cdot x = 0$ implies $n = 0$ or $x = 0$ for all $n \in \mathbb{Z}$ and $x \in M$, then the same holds for all $n \in \mathbb{N}$.

NoZeroSMulDivisors.int_of_charZero theorem

(R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℤ M

Full source

theorem NoZeroSMulDivisors.int_of_charZero
    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
    NoZeroSMulDivisors ℤ M :=
  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩

No Zero Scalar Divisors for $\mathbb{Z}$-Modules over Characteristic Zero Rings

Informal description

Let $R$ be a ring of characteristic zero and $M$ be an $R$-module with no non-trivial zero scalar divisors (i.e., for any $r \in R$ and $m \in M$, $r \cdot m = 0$ implies $r = 0$ or $m = 0$). Then $M$ also has no non-trivial zero scalar divisors when considered as a $\mathbb{Z}$-module (i.e., for any $n \in \mathbb{Z}$ and $m \in M$, $n \cdot m = 0$ implies $n = 0$ or $m = 0$).

CharZero.of_noZeroSMulDivisors theorem

[Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R

Full source

/-- Only a ring of characteristic zero can have a non-trivial module without additive or
scalar torsion. -/
theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
  refine ⟨fun {n m h} ↦ ?_⟩
  obtain ⟨x, hx⟩ := exists_ne (0 : M)
  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
  simpa using smul_left_injective ℤ hx h

Characteristic Zero from No Zero Scalar Divisors over Integers

Informal description

Let $R$ be a ring and $M$ be a nontrivial additive commutative group with a module structure over $R$. If there are no non-trivial zero scalar divisors for the $\mathbb{Z}$-module structure on $M$, then $R$ has characteristic zero. That is, the canonical map $\mathbb{N} \to R$ is injective.

instNoZeroSMulDivisorsNatOfInt_1 instance

[AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

Full source

instance [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ c x, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩

No Zero Scalar Divisors from Integers to Naturals

Informal description

For any additive commutative group $M$ with no zero scalar divisors over the integers $\mathbb{Z}$, $M$ also has no zero scalar divisors over the natural numbers $\mathbb{N}$.

GroupWithZero.toNoZeroSMulDivisors instance

: NoZeroSMulDivisors R M

Full source

/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
instance (priority := 100) GroupWithZero.toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩

Groups with Zero Have No Zero Scalar Divisors

Informal description

For any group with zero $R$ acting on an additive monoid $M$, the action has no zero scalar divisors. This means that for any nonzero $r \in R$ and any $m \in M$, if $r \cdot m = 0$ then $m = 0$.