Non-zero divisors and smul-divisors

In this file we define the submonoid nonZeroDivisors and nonZeroSMulDivisors of a MonoidWithZero. We also define nonZeroDivisorsLeft and nonZeroDivisorsRight for non-commutative monoids.

Notations

This file declares the notations:

• R⁰ for the submonoid of non-zero-divisors of R, in the locale nonZeroDivisors.
• R⁰[M] for the submonoid of non-zero smul-divisors of R with respect to M, in the locale nonZeroSMulDivisors

Use the statement open scoped nonZeroDivisors nonZeroSMulDivisors to access this notation in your own code.

def nonZeroDivisorsLeft (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀

The collection of elements of a MonoidWithZero that are not left zero divisors form a Submonoid.

Equations

• nonZeroDivisorsLeft M₀ = { carrier := {x : M₀ | ∀ (y : M₀), y * x = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (y : M₀), y * x = 0 → y = 0

theorem nmem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {r : M₀} : r ∉ nonZeroDivisorsLeft M₀ ↔ {s : M₀ | s * r = 0 ∧ s ≠ 0}.Nonempty

def nonZeroDivisorsRight (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀

The collection of elements of a MonoidWithZero that are not right zero divisors form a Submonoid.

Equations

• nonZeroDivisorsRight M₀ = { carrier := {x : M₀ | ∀ (y : M₀), x * y = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∈ nonZeroDivisorsRight M₀ ↔ ∀ (y : M₀), x * y = 0 → y = 0

theorem nmem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {r : M₀} : r ∉ nonZeroDivisorsRight M₀ ↔ {s : M₀ | r * s = 0 ∧ s ≠ 0}.Nonempty

theorem nonZeroDivisorsLeft_eq_right (M₀ : Type u_2) [CommMonoidWithZero M₀] : nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀

@[simp]

theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsLeft M₀) = {x : M₀ | x ≠ 0}

@[simp]

theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsRight M₀) = {x : M₀ | x ≠ 0}

def nonZeroDivisors (R : Type u_1) [MonoidWithZero R] : Submonoid R

The submonoid of non-zero-divisors of a MonoidWithZero R.

Equations

• nonZeroDivisors R = { carrier := {x : R | ∀ (z : R), z * x = 0 → z = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

def nonZeroSMulDivisors (R : Type u_1) [MonoidWithZero R] (M : Type u_2) [Zero M] [MulAction R M] : Submonoid R

Let R be a monoid with zero and M an additive monoid with an R-action, then the collection of non-zero smul-divisors forms a submonoid. These elements are also called M-regular.

Equations

• nonZeroSMulDivisors R M = { carrier := {r : R | ∀ (m : M), r • m = 0 → m = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

theorem mem_nonZeroDivisors_iff {M : Type u_1} [MonoidWithZero M] {r : M} : r ∈ nonZeroDivisors M ↔ ∀ (x : M), x * r = 0 → x = 0

theorem nmem_nonZeroDivisors_iff {M : Type u_1} [MonoidWithZero M] {r : M} : r ∉ nonZeroDivisors M ↔ {s : M | s * r = 0 ∧ s ≠ 0}.Nonempty

theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_1} [MonoidWithZero M] {x : M} {r : M} (hr : r ∈ nonZeroDivisors M) : x * r = 0 ↔ x = 0

@[simp]

theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M : Type u_1} [MonoidWithZero M] {x : M} {c : ↥(nonZeroDivisors M)} : x * ↑c = 0 ↔ x = 0

theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_3} [CommMonoidWithZero M₁] {r : M₁} {x : M₁} (hr : r ∈ nonZeroDivisors M₁) : r * x = 0 ↔ x = 0

@[simp]

theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₁ : Type u_3} [CommMonoidWithZero M₁] {c : ↥(nonZeroDivisors M₁)} {x : M₁} : ↑c * x = 0 ↔ x = 0

theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_4} [Ring R] {x : R} {y : R} {r : R} (hr : r ∈ nonZeroDivisors R) : x * r = y * r ↔ x = y

theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_4} [Ring R] {x : R} {y : R} {c : ↥(nonZeroDivisors R)} : x * ↑c = y * ↑c ↔ x = y

@[simp]

theorem mul_cancel_left_mem_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ∈ nonZeroDivisors R') : r * x = r * y ↔ x = y

theorem mul_cancel_left_coe_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {c : ↥(nonZeroDivisors R')} : ↑c * x = ↑c * y ↔ x = y

theorem dvd_cancel_right_mem_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ∈ nonZeroDivisors R') : x * r ∣ y * r ↔ x ∣ y

theorem dvd_cancel_right_coe_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {c : ↥(nonZeroDivisors R')} : x * ↑c ∣ y * ↑c ↔ x ∣ y

theorem dvd_cancel_left_mem_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ∈ nonZeroDivisors R') : r * x ∣ r * y ↔ x ∣ y

theorem dvd_cancel_left_coe_nonZeroDivisors {R' : Type u_5} [CommRing R'] {x : R'} {y : R'} {c : ↥(nonZeroDivisors R')} : ↑c * x ∣ ↑c * y ↔ x ∣ y

theorem zero_not_mem_nonZeroDivisors {M : Type u_1} [MonoidWithZero M] [Nontrivial M] : 0 ∉ nonZeroDivisors M

theorem nonZeroDivisors.ne_zero {M : Type u_1} [MonoidWithZero M] [Nontrivial M] {x : M} (hx : x ∈ nonZeroDivisors M) : x ≠ 0

@[simp]

theorem nonZeroDivisors.coe_ne_zero {M : Type u_1} [MonoidWithZero M] [Nontrivial M] (x : ↥(nonZeroDivisors M)) : ↑x ≠ 0

theorem mul_mem_nonZeroDivisors {M₁ : Type u_3} [CommMonoidWithZero M₁] {a : M₁} {b : M₁} : a * b ∈ nonZeroDivisors M₁ ↔ a ∈ nonZeroDivisors M₁ ∧ b ∈ nonZeroDivisors M₁

theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_7} [GroupWithZero G₀] {x : G₀} (hx : x ∈ nonZeroDivisors G₀) : IsUnit x

theorem IsUnit.mem_nonZeroDivisors {M : Type u_1} [MonoidWithZero M] {a : M} (ha : IsUnit a) : a ∈ nonZeroDivisors M

theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] {x : M} {y : M} (hnx : x ≠ 0) (hxy : y * x = 0) : y = 0

theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] {x : M} {y : M} (hnx : x ≠ 0) (hxy : x * y = 0) : y = 0

theorem mem_nonZeroDivisors_of_ne_zero {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] {x : M} (hx : x ≠ 0) : x ∈ nonZeroDivisors M

theorem mem_nonZeroDivisors_iff_ne_zero {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] [Nontrivial M] {x : M} : x ∈ nonZeroDivisors M ↔ x ≠ 0

theorem map_ne_zero_of_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_2} {F : Type u_6} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [Nontrivial M] [ZeroHomClass F M M'] (g : F) (hg : Function.Injective ⇑g) {x : M} (h : x ∈ nonZeroDivisors M) : g x ≠ 0

theorem map_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_2} {F : Type u_6} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [Nontrivial M] [NoZeroDivisors M'] [ZeroHomClass F M M'] (g : F) (hg : Function.Injective ⇑g) {x : M} (h : x ∈ nonZeroDivisors M) : g x ∈ nonZeroDivisors M'

theorem le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] {S : Submonoid M} (hS : 0 ∉ S) : S ≤ nonZeroDivisors M

theorem powers_le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [MonoidWithZero M] [NoZeroDivisors M] {a : M} (ha : a ≠ 0) : Submonoid.powers a ≤ nonZeroDivisors M

theorem map_le_nonZeroDivisors_of_injective {M : Type u_1} {M' : Type u_2} {F : Type u_6} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [NoZeroDivisors M'] [MonoidWithZeroHomClass F M M'] (f : F) (hf : Function.Injective ⇑f) {S : Submonoid M} (hS : S ≤ nonZeroDivisors M) : Submonoid.map f S ≤ nonZeroDivisors M'

theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective {M : Type u_1} {M' : Type u_2} {F : Type u_6} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [NoZeroDivisors M'] [MonoidWithZeroHomClass F M M'] (f : F) (hf : Function.Injective ⇑f) : nonZeroDivisors M ≤ Submonoid.comap f (nonZeroDivisors M')

theorem isUnit_iff_mem_nonZeroDivisors_of_finite {R : Type u_4} [Ring R] [Finite R] {a : R} : IsUnit a ↔ a ∈ nonZeroDivisors R

In a finite ring, an element is a unit iff it is a non-zero-divisor.

theorem mem_nonZeroSMulDivisors_iff {R : Type u_1} {M : Type u_2} [MonoidWithZero R] [Zero M] [MulAction R M] {x : R} : x ∈ nonZeroSMulDivisors R M ↔ ∀ (m : M), x • m = 0 → m = 0

@[simp]

theorem unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors (R : Type u_1) [MonoidWithZero R] : (nonZeroSMulDivisors Rᵐᵒᵖ R).unop = nonZeroDivisors R

theorem nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors (R : Type u_1) [MonoidWithZero R] : nonZeroSMulDivisors Rᵐᵒᵖ R = (nonZeroDivisors R).op

The non-zero •-divisors with • as right multiplication correspond with the non-zero divisors. Note that the MulOpposite is needed because we defined nonZeroDivisors with multiplication on the right.

def unitsNonZeroDivisorsEquiv {M₀ : Type u_1} [MonoidWithZero M₀] : (↥(nonZeroDivisors M₀))ˣ ≃* M₀ˣ

The units of the monoid of non-zero divisors of M₀ are equivalent to the units of M₀.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem unitsNonZeroDivisorsEquiv_apply {M₀ : Type u_1} [MonoidWithZero M₀] : ∀ (a : (↥(nonZeroDivisors M₀))ˣ), unitsNonZeroDivisorsEquiv a = (↑(Units.map (nonZeroDivisors M₀).subtype)).toFun a

@[simp]

theorem val_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u) = ↑u

@[simp]

theorem val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = ↑u⁻¹

@[simp]

theorem nonZeroDivisors.associated_coe {M₀ : Type u_1} [MonoidWithZero M₀] {a : ↥(nonZeroDivisors M₀)} {b : ↥(nonZeroDivisors M₀)} : Associated ↑a ↑b ↔ Associated a b

theorem mk_mem_nonZeroDivisors_associates {M₀ : Type u_1} [CommMonoidWithZero M₀] {a : M₀} : Associates.mk a ∈ nonZeroDivisors (Associates M₀) ↔ a ∈ nonZeroDivisors M₀

def associatesNonZeroDivisorsEquiv {M₀ : Type u_1} [CommMonoidWithZero M₀] : ↥(nonZeroDivisors (Associates M₀)) ≃* Associates ↥(nonZeroDivisors M₀)

The non-zero divisors of associates of a monoid with zero M₀ are isomorphic to the associates of the non-zero divisors of M₀ under the map ⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem associatesNonZeroDivisorsEquiv_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : ⟦a⟧ ∈ nonZeroDivisors (Associates M₀)) : associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, ⋯⟩⟧

@[simp]

theorem associatesNonZeroDivisorsEquiv_symm_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : a ∈ nonZeroDivisors M₀) : associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, ⋯⟩