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:
M₀⁰for the submonoid of non-zero-divisors ofM₀, in the localenonZeroDivisors.M₀⁰[M]for the submonoid of non-zero smul-divisors ofM₀with respect toM, in the localenonZeroSMulDivisors
Use the statement open scoped nonZeroDivisors nonZeroSMulDivisors to access this notation in
your own code.
The collection of elements of a MonoidWithZero that are not left zero divisors form a
Submonoid.
@[simp]
The collection of elements of a MonoidWithZero that are not right zero divisors form a
Submonoid.
@[simp]
@[simp]
theorem
coe_nonZeroDivisorsLeft_eq
(M₀ : Type u_1)
[MonoidWithZero M₀]
[NoZeroDivisors M₀]
[Nontrivial M₀]
:
@[simp]
theorem
coe_nonZeroDivisorsRight_eq
(M₀ : Type u_1)
[MonoidWithZero M₀]
[NoZeroDivisors M₀]
[Nontrivial M₀]
:
The submonoid of non-zero-divisors of a MonoidWithZero M₀.
The notation for the submonoid of non-zero divisors.
Equations
- nonZeroDivisors.«term_⁰» = Lean.ParserDescr.trailingNode `nonZeroDivisors.«term_⁰» 9000 0 (Lean.ParserDescr.symbol "⁰")
def
nonZeroSMulDivisors
(M₀ : Type u_1)
[MonoidWithZero M₀]
(M : Type u_2)
[Zero M]
[MulAction M₀ M]
:
Submonoid M₀
Let M₀ be a monoid with zero and M an additive monoid with an M₀-action, then the
collection of non-zero smul-divisors forms a submonoid.
These elements are also called M-regular.
The notation for the submonoid of non-zero smul-divisors.
Equations
- One or more equations did not get rendered due to their size.
theorem
mul_right_mem_nonZeroDivisors_eq_zero_iff
{M₀ : Type u_2}
[MonoidWithZero M₀]
{r x : M₀}
(hr : r ∈ nonZeroDivisors M₀)
:
@[simp]
theorem
mul_right_coe_nonZeroDivisors_eq_zero_iff
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x : M₀}
{c : ↥(nonZeroDivisors M₀)}
:
theorem
zero_not_mem_nonZeroDivisors
{M₀ : Type u_2}
[MonoidWithZero M₀]
[Nontrivial M₀]
:
0 ∉ nonZeroDivisors M₀
theorem
nonZeroDivisors.ne_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x : M₀}
[Nontrivial M₀]
(hx : x ∈ nonZeroDivisors M₀)
:
@[simp]
theorem
nonZeroDivisors.coe_ne_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
[Nontrivial M₀]
(x : ↥(nonZeroDivisors M₀))
:
instance
instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero
{M₀ : Type u_2}
[MonoidWithZero M₀]
[Nontrivial M₀]
[IsLeftCancelMulZero M₀]
:
Equations
- instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero = { toMonoid := (nonZeroDivisors M₀).toMonoid, mul_left_cancel := ⋯ }
instance
instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero
{M₀ : Type u_2}
[MonoidWithZero M₀]
[Nontrivial M₀]
[IsRightCancelMulZero M₀]
:
Equations
- instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero = { toMonoid := (nonZeroDivisors M₀).toMonoid, mul_right_cancel := ⋯ }
theorem
eq_zero_of_ne_zero_of_mul_right_eq_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x y : M₀}
[NoZeroDivisors M₀]
(hx : x ≠ 0)
(hxy : y * x = 0)
:
theorem
eq_zero_of_ne_zero_of_mul_left_eq_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x y : M₀}
[NoZeroDivisors M₀]
(hx : x ≠ 0)
(hxy : x * y = 0)
:
theorem
mem_nonZeroDivisors_of_ne_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x : M₀}
[NoZeroDivisors M₀]
(hx : x ≠ 0)
:
@[simp]
theorem
mem_nonZeroDivisors_iff_ne_zero
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x : M₀}
[NoZeroDivisors M₀]
[Nontrivial M₀]
:
theorem
le_nonZeroDivisors_of_noZeroDivisors
{M₀ : Type u_2}
[MonoidWithZero M₀]
[NoZeroDivisors M₀]
{S : Submonoid M₀}
(hS : 0 ∉ S)
:
theorem
powers_le_nonZeroDivisors_of_noZeroDivisors
{M₀ : Type u_2}
[MonoidWithZero M₀]
{x : M₀}
[NoZeroDivisors M₀]
(hx : x ≠ 0)
:
theorem
map_ne_zero_of_mem_nonZeroDivisors
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[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₀)
:
theorem
map_mem_nonZeroDivisors
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[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₀)
:
theorem
MulEquivClass.map_nonZeroDivisors
{M₀ : Type u_4}
{S : Type u_5}
{F : Type u_6}
[MonoidWithZero M₀]
[MonoidWithZero S]
[EquivLike F M₀ S]
[MulEquivClass F M₀ S]
(h : F)
:
theorem
map_le_nonZeroDivisors_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[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₀)
:
theorem
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[MonoidWithZero M₀]
[MonoidWithZero M₀']
[FunLike F M₀ M₀']
[NoZeroDivisors M₀']
[MonoidWithZeroHomClass F M₀ M₀']
(f : F)
(hf : Function.Injective ⇑f)
:
theorem
mem_nonZeroDivisors_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[MonoidWithZero M₀]
[MonoidWithZero M₀']
{x : M₀}
[FunLike F M₀ M₀']
[MonoidWithZeroHomClass F M₀ M₀']
{f : F}
(hf : Function.Injective ⇑f)
(hx : f x ∈ nonZeroDivisors M₀')
:
If an element maps to a non-zero-divisor via injective homomorphism, then it is a non-zero-divisor.
@[deprecated mem_nonZeroDivisors_of_injective (since := "2025-02-03")]
theorem
mem_nonZeroDivisor_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[MonoidWithZero M₀]
[MonoidWithZero M₀']
{x : M₀}
[FunLike F M₀ M₀']
[MonoidWithZeroHomClass F M₀ M₀']
{f : F}
(hf : Function.Injective ⇑f)
(hx : f x ∈ nonZeroDivisors M₀')
:
Alias of mem_nonZeroDivisors_of_injective.
If an element maps to a non-zero-divisor via injective homomorphism, then it is a non-zero-divisor.
theorem
comap_nonZeroDivisors_le_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[MonoidWithZero M₀]
[MonoidWithZero M₀']
[FunLike F M₀ M₀']
[MonoidWithZeroHomClass F M₀ M₀']
{f : F}
(hf : Function.Injective ⇑f)
:
@[deprecated comap_nonZeroDivisors_le_of_injective (since := "2025-02-03")]
theorem
comap_nonZeroDivisor_le_of_injective
{F : Type u_1}
{M₀ : Type u_2}
{M₀' : Type u_3}
[MonoidWithZero M₀]
[MonoidWithZero M₀']
[FunLike F M₀ M₀']
[MonoidWithZeroHomClass F M₀ M₀']
{f : F}
(hf : Function.Injective ⇑f)
:
Alias of comap_nonZeroDivisors_le_of_injective.
theorem
mul_left_mem_nonZeroDivisors_eq_zero_iff
{M₀ : Type u_1}
[CommMonoidWithZero M₀]
{r x : M₀}
(hr : r ∈ nonZeroDivisors M₀)
:
@[simp]
theorem
mul_left_coe_nonZeroDivisors_eq_zero_iff
{M₀ : Type u_1}
[CommMonoidWithZero M₀]
{x : M₀}
{c : ↥(nonZeroDivisors M₀)}
:
Canonical isomorphism between the non-zero-divisors and units of a group with zero.
Equations
- nonZeroDivisorsEquivUnits = { toFun := fun (u : ↥(nonZeroDivisors G₀)) => Units.mk0 ↑u ⋯, invFun := fun (u : G₀ˣ) => ⟨↑u, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
@[simp]
@[simp]
theorem
nonZeroDivisorsEquivUnits_apply
{G₀ : Type u_1}
[GroupWithZero G₀]
(u : ↥(nonZeroDivisors G₀))
:
theorem
isUnit_of_mem_nonZeroDivisors
{G₀ : Type u_1}
[GroupWithZero G₀]
{x : G₀}
(hx : x ∈ nonZeroDivisors G₀)
:
IsUnit x
theorem
mem_nonZeroSMulDivisors_iff
{M₀ : Type u_1}
{M : Type u_2}
[MonoidWithZero M₀]
[Zero M]
[MulAction M₀ M]
{x : M₀}
:
@[simp]
theorem
unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors
(M₀ : Type u_1)
[MonoidWithZero M₀]
:
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.
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
val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe
{M₀ : Type u_1}
[MonoidWithZero M₀]
(u : M₀ˣ)
:
@[simp]
theorem
val_unitsNonZeroDivisorsEquiv_symm_apply_coe
{M₀ : Type u_1}
[MonoidWithZero M₀]
(u : M₀ˣ)
:
@[simp]
theorem
unitsNonZeroDivisorsEquiv_apply
{M₀ : Type u_1}
[MonoidWithZero M₀]
(a✝ : (↥(nonZeroDivisors M₀))ˣ)
:
@[simp]
theorem
nonZeroDivisors.associated_coe
{M₀ : Type u_1}
[MonoidWithZero M₀]
{a b : ↥(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₀))
:
@[simp]
theorem
associatesNonZeroDivisorsEquiv_symm_mk_mk
{M₀ : Type u_1}
[CommMonoidWithZero M₀]
(a : M₀)
(ha : a ∈ nonZeroDivisors M₀)
: