Documentation

Mathlib.Algebra.Regular.Basic

Regular elements #

We introduce left-regular, right-regular and regular elements, along with their to_additive analogues add-left-regular, add-right-regular and add-regular elements.

By definition, a regular element in a commutative ring is a non-zero divisor. Lemma isRegular_of_ne_zero implies that every non-zero element of an integral domain is regular. Since it assumes that the ring is a CancelMonoidWithZero it applies also, for instance, to ℕ.

The lemmas in Section MulZeroClass show that the 0 element is (left/right-)regular if and only if the MulZeroClass is trivial. This is useful when figuring out stopping conditions for regular sequences: if 0 is ever an element of a regular sequence, then we can extend the sequence by adding one further 0.

The final goal is to develop part of the API to prove, eventually, results about non-zero-divisors.

def IsAddLeftRegular {R : Type u_1} [inst : Add R] (c : R) :

An add-left-regular element is an element c such that addition on the left by c is injective.

Equations

IsAddLeftRegular c = Function.Injective fun x => c + x

def IsLeftRegular {R : Type u_1} [inst : Mul R] (c : R) :

A left-regular element is an element c such that multiplication on the left by c is injective.

Equations

IsLeftRegular c = Function.Injective fun x => c * x

def IsAddRightRegular {R : Type u_1} [inst : Add R] (c : R) :

An add-right-regular element is an element c such that addition on the right by c is injective.

Equations

IsAddRightRegular c = Function.Injective fun x => x + c

def IsRightRegular {R : Type u_1} [inst : Mul R] (c : R) :

A right-regular element is an element c such that multiplication on the right by c is injective.

Equations

IsRightRegular c = Function.Injective fun x => x * c

structure IsAddRegular {R : Type u_1} [inst : Add R] (c : R) :

An add-regular element c is left-regular
left : IsAddLeftRegular c
An add-regular element c is right-regular
right : IsAddRightRegular c

An add-regular element is an element c such that addition by c both on the left and on the right is injective.

Instances For

structure IsRegular {R : Type u_1} [inst : Mul R] (c : R) :

A regular element c is left-regular
left : IsLeftRegular c
A regular element c is right-regular
right : IsRightRegular c

A regular element is an element c such that multiplication by c both on the left and on the right is injective.

Instances For

theorem AddLECancellable.isAddLeftRegular {R : Type u_1} [inst : Add R] [inst : PartialOrder R] {a : R} (ha : AddLECancellable a) :

IsAddLeftRegular a

theorem MulLECancellable.isLeftRegular {R : Type u_1} [inst : Mul R] [inst : PartialOrder R] {a : R} (ha : MulLECancellable a) :

IsLeftRegular a

theorem IsLeftRegular.right_of_commute {R : Type u_1} [inst : Mul R] {a : R} (ca : ∀ (b : R), Commute a b) (h : IsLeftRegular a) :

IsRightRegular a

theorem Commute.isRegular_iff {R : Type u_1} [inst : Mul R] {a : R} (ca : ∀ (b : R), Commute a b) :

IsRegular a ↔ IsLeftRegular a

theorem IsAddLeftRegular.add {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} (lra : IsAddLeftRegular a) (lrb : IsAddLeftRegular b) :

IsAddLeftRegular (a + b)

In an additive semigroup, the sum of add-left-regular elements is add-left.regular.

theorem IsLeftRegular.mul {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} (lra : IsLeftRegular a) (lrb : IsLeftRegular b) :

IsLeftRegular (a * b)

In a semigroup, the product of left-regular elements is left-regular.

theorem IsAddRightRegular.add {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} (rra : IsAddRightRegular a) (rrb : IsAddRightRegular b) :

IsAddRightRegular (a + b)

In an additive semigroup, the sum of add-right-regular elements is add-right-regular.

theorem IsRightRegular.mul {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} (rra : IsRightRegular a) (rrb : IsRightRegular b) :

IsRightRegular (a * b)

In a semigroup, the product of right-regular elements is right-regular.

theorem IsAddLeftRegular.of_add {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} (ab : IsAddLeftRegular (a + b)) :

IsAddLeftRegular b

If an element b becomes add-left-regular after adding to it on the left a add-left-regular element, then b is add-left-regular.

theorem IsLeftRegular.of_mul {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} (ab : IsLeftRegular (a * b)) :

IsLeftRegular b

If an element b becomes left-regular after multiplying it on the left by a left-regular element, then b is left-regular.

@[simp]

theorem add_isAddLeftRegular_iff {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R) (ha : IsAddLeftRegular a) :

IsAddLeftRegular (a + b) ↔ IsAddLeftRegular b

An element is add-left-regular if and only if adding to it on the left a add-left-regular element is add-left-regular.

@[simp]

theorem mul_isLeftRegular_iff {R : Type u_1} [inst : Semigroup R] {a : R} (b : R) (ha : IsLeftRegular a) :

IsLeftRegular (a * b) ↔ IsLeftRegular b

An element is left-regular if and only if multiplying it on the left by a left-regular element is left-regular.

theorem IsAddRightRegular.of_add {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} (ab : IsAddRightRegular (b + a)) :

IsAddRightRegular b

If an element b becomes add-right-regular after adding to it on the right a add-right-regular element, then b is add-right-regular.

theorem IsRightRegular.of_mul {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} (ab : IsRightRegular (b * a)) :

IsRightRegular b

If an element b becomes right-regular after multiplying it on the right by a right-regular element, then b is right-regular.

@[simp]

theorem add_isAddRightRegular_iff {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R) (ha : IsAddRightRegular a) :

IsAddRightRegular (b + a) ↔ IsAddRightRegular b

An element is add-right-regular if and only if adding it on the right to a add-right-regular element is add-right-regular.

@[simp]

theorem mul_isRightRegular_iff {R : Type u_1} [inst : Semigroup R] {a : R} (b : R) (ha : IsRightRegular a) :

IsRightRegular (b * a) ↔ IsRightRegular b

An element is right-regular if and only if multiplying it on the right with a right-regular element is right-regular.

theorem isAddRegular_add_and_add_iff {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} :

IsAddRegular (a + b) ∧ IsAddRegular (b + a) ↔ IsAddRegular a ∧ IsAddRegular b

Two elements a and b are add-regular if and only if both sums a + b and b + a are add-regular.

theorem isRegular_mul_and_mul_iff {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} :

IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Two elements a and b are regular if and only if both products a * b and b * a are regular.

theorem IsAddRegular.and_of_add_of_add {R : Type u_1} [inst : AddSemigroup R] {a : R} {b : R} (ab : IsAddRegular (a + b)) (ba : IsAddRegular (b + a)) :

IsAddRegular a ∧ IsAddRegular b

The "most used" implication of add_and_add_iff, with split hypotheses, instead of ∧∧.

theorem IsRegular.and_of_mul_of_mul {R : Type u_1} [inst : Semigroup R] {a : R} {b : R} (ab : IsRegular (a * b)) (ba : IsRegular (b * a)) :

IsRegular a ∧ IsRegular b

The "most used" implication of mul_and_mul_iff, with split hypotheses, instead of ∧∧.

theorem IsLeftRegular.subsingleton {R : Type u_1} [inst : MulZeroClass R] (h : IsLeftRegular 0) :

The element 0 is left-regular if and only if R is trivial.

theorem IsRightRegular.subsingleton {R : Type u_1} [inst : MulZeroClass R] (h : IsRightRegular 0) :

The element 0 is right-regular if and only if R is trivial.

theorem IsRegular.subsingleton {R : Type u_1} [inst : MulZeroClass R] (h : IsRegular 0) :

The element 0 is regular if and only if R is trivial.

theorem isLeftRegular_zero_iff_subsingleton {R : Type u_1} [inst : MulZeroClass R] :

IsLeftRegular 0 ↔ Subsingleton R

The element 0 is left-regular if and only if R is trivial.

theorem not_isLeftRegular_zero_iff {R : Type u_1} [inst : MulZeroClass R] :

¬IsLeftRegular 0 ↔ Nontrivial R

In a non-trivial MulZeroClass, the 0 element is not left-regular.

theorem isRightRegular_zero_iff_subsingleton {R : Type u_1} [inst : MulZeroClass R] :

IsRightRegular 0 ↔ Subsingleton R

The element 0 is right-regular if and only if R is trivial.

theorem not_isRightRegular_zero_iff {R : Type u_1} [inst : MulZeroClass R] :

¬IsRightRegular 0 ↔ Nontrivial R

In a non-trivial MulZeroClass, the 0 element is not right-regular.

theorem isRegular_iff_subsingleton {R : Type u_1} [inst : MulZeroClass R] :

IsRegular 0 ↔ Subsingleton R

The element 0 is regular if and only if R is trivial.

theorem IsLeftRegular.ne_zero {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst : Nontrivial R] (la : IsLeftRegular a) :

a ≠ 0

A left-regular element of a Nontrivial MulZeroClass is non-zero.

theorem IsRightRegular.ne_zero {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst : Nontrivial R] (ra : IsRightRegular a) :

a ≠ 0

A right-regular element of a Nontrivial MulZeroClass is non-zero.

theorem IsRegular.ne_zero {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst : Nontrivial R] (la : IsRegular a) :

a ≠ 0

A regular element of a Nontrivial MulZeroClass is non-zero.

theorem not_isLeftRegular_zero {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R] :

¬IsLeftRegular 0

In a non-trivial ring, the element 0 is not left-regular -- with typeclasses.

theorem not_isRightRegular_zero {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R] :

¬IsRightRegular 0

In a non-trivial ring, the element 0 is not right-regular -- with typeclasses.

theorem not_isRegular_zero {R : Type u_1} [inst : MulZeroClass R] [inst : Nontrivial R] :

In a non-trivial ring, the element 0 is not regular -- with typeclasses.

theorem isAddRegular_zero {R : Type u_1} [inst : AddZeroClass R] :

If adding 0 on either side is the identity, 0 is regular.

theorem isRegular_one {R : Type u_1} [inst : MulOneClass R] :

If multiplying by 1 on either side is the identity, 1 is regular.

theorem isAddRegular_add_iff {R : Type u_1} [inst : AddCommSemigroup R] {a : R} {b : R} :

IsAddRegular (a + b) ↔ IsAddRegular a ∧ IsAddRegular b

A sum is add-regular if and only if the summands are.

theorem isRegular_mul_iff {R : Type u_1} [inst : CommSemigroup R] {a : R} {b : R} :

IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

A product is regular if and only if the factors are.

theorem isAddLeftRegular_of_add_eq_zero {R : Type u_1} [inst : AddMonoid R] {a : R} {b : R} (h : b + a = 0) :

IsAddLeftRegular a

An element admitting a left additive opposite is add-left-regular.

theorem isLeftRegular_of_mul_eq_one {R : Type u_1} [inst : Monoid R] {a : R} {b : R} (h : b * a = 1) :

IsLeftRegular a

An element admitting a left inverse is left-regular.

theorem isAddRightRegular_of_add_eq_zero {R : Type u_1} [inst : AddMonoid R] {a : R} {b : R} (h : a + b = 0) :

IsAddRightRegular a

An element admitting a right additive opposite is add-right-regular.

theorem isRightRegular_of_mul_eq_one {R : Type u_1} [inst : Monoid R] {a : R} {b : R} (h : a * b = 1) :

IsRightRegular a

An element admitting a right inverse is right-regular.

theorem AddUnits.isAddRegular {R : Type u_1} [inst : AddMonoid R] (a : AddUnits R) :

IsAddRegular ↑a

If R is an additive monoid, an element in add_units R is add-regular.

theorem Units.isRegular {R : Type u_1} [inst : Monoid R] (a : Rˣ) :

If R is a monoid, an element in Rˣ is regular.

theorem IsAddUnit.isAddRegular {R : Type u_1} [inst : AddMonoid R] {a : R} (ua : IsAddUnit a) :

An additive unit in an additive monoid is add-regular.

theorem IsUnit.isRegular {R : Type u_1} [inst : Monoid R] {a : R} (ua : IsUnit a) :

A unit in a monoid is regular.

theorem isAddLeftRegular_of_addLeftCancelSemigroup {R : Type u_1} [inst : AddLeftCancelSemigroup R] (g : R) :

IsAddLeftRegular g

Elements of an add left cancel semigroup are add-left-regular.

theorem isLeftRegular_of_leftCancelSemigroup {R : Type u_1} [inst : LeftCancelSemigroup R] (g : R) :

IsLeftRegular g

Elements of a left cancel semigroup are left regular.

theorem isAddRightRegular_of_addRightCancelSemigroup {R : Type u_1} [inst : AddRightCancelSemigroup R] (g : R) :

IsAddRightRegular g

Elements of an add right cancel semigroup are add-right-regular

theorem isRightRegular_of_rightCancelSemigroup {R : Type u_1} [inst : RightCancelSemigroup R] (g : R) :

IsRightRegular g

Elements of a right cancel semigroup are right regular.

theorem isAddRegular_of_addCancelMonoid {R : Type u_1} [inst : AddCancelMonoid R] (g : R) :

Elements of an add cancel monoid are regular. Add cancel semigroups do not appear to exist.

theorem isRegular_of_cancelMonoid {R : Type u_1} [inst : CancelMonoid R] (g : R) :

Elements of a cancel monoid are regular. Cancel semigroups do not appear to exist.

theorem isRegular_of_ne_zero {R : Type u_1} [inst : CancelMonoidWithZero R] {a : R} (a0 : a ≠ 0) :

Non-zero elements of an integral domain are regular.

theorem isRegular_iff_ne_zero {R : Type u_1} [inst : CancelMonoidWithZero R] {a : R} [inst : Nontrivial R] :

IsRegular a ↔ a ≠ 0

In a non-trivial integral domain, an element is regular iff it is non-zero.