mathlib documentation

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 is_regular_of_ne_zero implies that every non-zero element of an integral domain is regular. Since it assumes that the ring is a cancel_monoid_with_zero it applies also, for instance, to ℕ.

The lemmas in Section mul_zero_class show that the 0 element is (left/right-)regular if and only if the mul_zero_class 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 is_left_regular {R : Type u_1} [has_mul R] (c : R) :

Prop

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

Equations

is_left_regular c = function.injective (has_mul.mul c)

def is_add_left_regular {R : Type u_1} [has_add R] (c : R) :

Prop

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

Equations

is_add_left_regular c = function.injective (has_add.add c)

def is_add_right_regular {R : Type u_1} [has_add R] (c : R) :

Prop

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

Equations

is_add_right_regular c = function.injective (λ (_x : R), _x + c)

def is_right_regular {R : Type u_1} [has_mul R] (c : R) :

Prop

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

Equations

is_right_regular c = function.injective (λ (_x : R), _x * c)

structure is_add_regular {R : Type u_2} [has_add R] (c : R) :

Prop

left : is_add_left_regular c
right : is_add_right_regular c

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

structure is_regular {R : Type u_1} [has_mul R] (c : R) :

Prop

left : is_left_regular c
right : is_right_regular c

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

@[protected]

theorem add_le_cancellable.is_add_left_regular {R : Type u_1} [has_add R] [partial_order R] {a : R} (ha : add_le_cancellable a) :

is_add_left_regular a

@[protected]

theorem mul_le_cancellable.is_left_regular {R : Type u_1} [has_mul R] [partial_order R] {a : R} (ha : mul_le_cancellable a) :

is_left_regular a

theorem is_left_regular.right_of_commute {R : Type u_1} [has_mul R] {a : R} (ca : ∀ (b : R), commute a b) (h : is_left_regular a) :

is_right_regular a

theorem commute.is_regular_iff {R : Type u_1} [has_mul R] {a : R} (ca : ∀ (b : R), commute a b) :

is_regular a ↔ is_left_regular a

theorem is_left_regular.mul {R : Type u_1} {a b : R} [semigroup R] (lra : is_left_regular a) (lrb : is_left_regular b) :

is_left_regular (a * b)

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

theorem is_add_left_regular.add {R : Type u_1} {a b : R} [add_semigroup R] (lra : is_add_left_regular a) (lrb : is_add_left_regular b) :

is_add_left_regular (a + b)

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

theorem is_right_regular.mul {R : Type u_1} {a b : R} [semigroup R] (rra : is_right_regular a) (rrb : is_right_regular b) :

is_right_regular (a * b)

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

theorem is_add_right_regular.add {R : Type u_1} {a b : R} [add_semigroup R] (rra : is_add_right_regular a) (rrb : is_add_right_regular b) :

is_add_right_regular (a + b)

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

theorem is_left_regular.of_mul {R : Type u_1} {a b : R} [semigroup R] (ab : is_left_regular (a * b)) :

is_left_regular b

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

theorem is_add_left_regular.of_add {R : Type u_1} {a b : R} [add_semigroup R] (ab : is_add_left_regular (a + b)) :

is_add_left_regular 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.

@[simp]

theorem mul_is_left_regular_iff {R : Type u_1} {a : R} [semigroup R] (b : R) (ha : is_left_regular a) :

is_left_regular (a * b) ↔ is_left_regular b

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

@[simp]

theorem add_is_add_left_regular_iff {R : Type u_1} {a : R} [add_semigroup R] (b : R) (ha : is_add_left_regular a) :

is_add_left_regular (a + b) ↔ is_add_left_regular 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.

theorem is_add_right_regular.of_add {R : Type u_1} {a b : R} [add_semigroup R] (ab : is_add_right_regular (b + a)) :

is_add_right_regular 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 is_right_regular.of_mul {R : Type u_1} {a b : R} [semigroup R] (ab : is_right_regular (b * a)) :

is_right_regular 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 mul_is_right_regular_iff {R : Type u_1} {a : R} [semigroup R] (b : R) (ha : is_right_regular a) :

is_right_regular (b * a) ↔ is_right_regular b

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

@[simp]

theorem add_is_add_right_regular_iff {R : Type u_1} {a : R} [add_semigroup R] (b : R) (ha : is_add_right_regular a) :

is_add_right_regular (b + a) ↔ is_add_right_regular 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.

theorem is_add_regular_add_and_add_iff {R : Type u_1} {a b : R} [add_semigroup R] :

is_add_regular (a + b) ∧ is_add_regular (b + a) ↔ is_add_regular a ∧ is_add_regular b

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

theorem is_regular_mul_and_mul_iff {R : Type u_1} {a b : R} [semigroup R] :

is_regular (a * b) ∧ is_regular (b * a) ↔ is_regular a ∧ is_regular b

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

theorem is_add_regular.and_of_add_of_add {R : Type u_1} {a b : R} [add_semigroup R] (ab : is_add_regular (a + b)) (ba : is_add_regular (b + a)) :

is_add_regular a ∧ is_add_regular b

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

theorem is_regular.and_of_mul_of_mul {R : Type u_1} {a b : R} [semigroup R] (ab : is_regular (a * b)) (ba : is_regular (b * a)) :

is_regular a ∧ is_regular b

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

theorem is_left_regular.subsingleton {R : Type u_1} [mul_zero_class R] (h : is_left_regular 0) :

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

theorem is_right_regular.subsingleton {R : Type u_1} [mul_zero_class R] (h : is_right_regular 0) :

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

theorem is_regular.subsingleton {R : Type u_1} [mul_zero_class R] (h : is_regular 0) :

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

theorem is_left_regular_zero_iff_subsingleton {R : Type u_1} [mul_zero_class R] :

is_left_regular 0 ↔ subsingleton R

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

theorem not_is_left_regular_zero_iff {R : Type u_1} [mul_zero_class R] :

¬is_left_regular 0 ↔ nontrivial R

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

theorem is_right_regular_zero_iff_subsingleton {R : Type u_1} [mul_zero_class R] :

is_right_regular 0 ↔ subsingleton R

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

theorem not_is_right_regular_zero_iff {R : Type u_1} [mul_zero_class R] :

¬is_right_regular 0 ↔ nontrivial R

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

theorem is_regular_iff_subsingleton {R : Type u_1} [mul_zero_class R] :

is_regular 0 ↔ subsingleton R

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

theorem is_left_regular.ne_zero {R : Type u_1} {a : R} [mul_zero_class R] [nontrivial R] (la : is_left_regular a) :

a ≠ 0

A left-regular element of a nontrivial mul_zero_class is non-zero.

theorem is_right_regular.ne_zero {R : Type u_1} {a : R} [mul_zero_class R] [nontrivial R] (ra : is_right_regular a) :

a ≠ 0

A right-regular element of a nontrivial mul_zero_class is non-zero.

theorem is_regular.ne_zero {R : Type u_1} {a : R} [mul_zero_class R] [nontrivial R] (la : is_regular a) :

a ≠ 0

A regular element of a nontrivial mul_zero_class is non-zero.

theorem not_is_left_regular_zero {R : Type u_1} [mul_zero_class R] [nR : nontrivial R] :

¬is_left_regular 0

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

theorem not_is_right_regular_zero {R : Type u_1} [mul_zero_class R] [nR : nontrivial R] :

¬is_right_regular 0

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

theorem not_is_regular_zero {R : Type u_1} [mul_zero_class R] [nontrivial R] :

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

theorem is_regular_mul_iff {R : Type u_1} {a b : R} [comm_semigroup R] :

is_regular (a * b) ↔ is_regular a ∧ is_regular b

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

theorem is_add_regular_add_iff {R : Type u_1} {a b : R} [add_comm_semigroup R] :

is_add_regular (a + b) ↔ is_add_regular a ∧ is_add_regular b

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

theorem is_regular_one {R : Type u_1} [monoid R] :

In a monoid, 1 is regular.

theorem is_add_regular_zero {R : Type u_1} [add_monoid R] :

is_add_regular 0

In an additive monoid, 0 is regular.

theorem is_left_regular_of_mul_eq_one {R : Type u_1} {a b : R} [monoid R] (h : b * a = 1) :

is_left_regular a

An element admitting a left inverse is left-regular.

theorem is_add_left_regular_of_add_eq_zero {R : Type u_1} {a b : R} [add_monoid R] (h : b + a = 0) :

is_add_left_regular a

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

theorem is_add_right_regular_of_add_eq_zero {R : Type u_1} {a b : R} [add_monoid R] (h : a + b = 0) :

is_add_right_regular a

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

theorem is_right_regular_of_mul_eq_one {R : Type u_1} {a b : R} [monoid R] (h : a * b = 1) :

is_right_regular a

An element admitting a right inverse is right-regular.

theorem add_units.is_add_regular {R : Type u_1} [add_monoid R] (a : add_units R) :

is_add_regular ↑a

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

theorem units.is_regular {R : Type u_1} [monoid R] (a : Rˣ) :

is_regular ↑a

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

theorem is_unit.is_regular {R : Type u_1} {a : R} [monoid R] (ua : is_unit a) :

A unit in a monoid is regular.

theorem is_add_unit.is_add_regular {R : Type u_1} {a : R} [add_monoid R] (ua : is_add_unit a) :

is_add_regular a

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

def add_left_embedding {G : Type u_1} [add_left_cancel_semigroup G] (g : G) :

G ↪ G

The embedding of a left cancellative additive semigroup into itself by left translation by a fixed element.

Equations

add_left_embedding g = {to_fun := λ (h : G), g + h, inj' := _}

def mul_left_embedding {G : Type u_1} [left_cancel_semigroup G] (g : G) :

G ↪ G

The embedding of a left cancellative semigroup into itself by left multiplication by a fixed element.

Equations

mul_left_embedding g = {to_fun := λ (h : G), g * h, inj' := _}

@[simp]

theorem add_left_embedding_apply {G : Type u_1} [add_left_cancel_semigroup G] (g h : G) :

⇑(add_left_embedding g) h = g + h

@[simp]

theorem mul_left_embedding_apply {G : Type u_1} [left_cancel_semigroup G] (g h : G) :

⇑(mul_left_embedding g) h = g * h

@[simp]

theorem add_right_embedding_apply {G : Type u_1} [add_right_cancel_semigroup G] (g h : G) :

⇑(add_right_embedding g) h = h + g

def mul_right_embedding {G : Type u_1} [right_cancel_semigroup G] (g : G) :

G ↪ G

The embedding of a right cancellative semigroup into itself by right multiplication by a fixed element.

Equations

mul_right_embedding g = {to_fun := λ (h : G), h * g, inj' := _}

def add_right_embedding {G : Type u_1} [add_right_cancel_semigroup G] (g : G) :

G ↪ G

The embedding of a right cancellative additive semigroup into itself by right translation by a fixed element.

Equations

add_right_embedding g = {to_fun := λ (h : G), h + g, inj' := _}

@[simp]

theorem mul_right_embedding_apply {G : Type u_1} [right_cancel_semigroup G] (g h : G) :

⇑(mul_right_embedding g) h = h * g

theorem mul_left_embedding_eq_mul_right_embedding {G : Type u_1} [cancel_comm_monoid G] (g : G) :

mul_left_embedding g = mul_right_embedding g

theorem add_left_embedding_eq_add_right_embedding {G : Type u_1} [add_cancel_comm_monoid G] (g : G) :

add_left_embedding g = add_right_embedding g

theorem is_left_regular_of_left_cancel_semigroup {R : Type u_1} [left_cancel_semigroup R] (g : R) :

is_left_regular g

Elements of a left cancel semigroup are left regular.

theorem is_add_left_regular_of_left_cancel_add_semigroup {R : Type u_1} [add_left_cancel_semigroup R] (g : R) :

is_add_left_regular g

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

theorem is_right_regular_of_right_cancel_semigroup {R : Type u_1} [right_cancel_semigroup R] (g : R) :

is_right_regular g

Elements of a right cancel semigroup are right regular.

theorem is_add_right_regular_of_right_cancel_add_semigroup {R : Type u_1} [add_right_cancel_semigroup R] (g : R) :

is_add_right_regular g

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

theorem is_regular_of_cancel_monoid {R : Type u_1} [cancel_monoid R] (g : R) :

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

theorem is_add_regular_of_cancel_add_monoid {R : Type u_1} [add_cancel_monoid R] (g : R) :

is_add_regular g

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

theorem is_regular_of_ne_zero {R : Type u_1} {a : R} [cancel_monoid_with_zero R] (a0 : a ≠ 0) :

Non-zero elements of an integral domain are regular.

theorem is_regular_iff_ne_zero {R : Type u_1} {a : R} [cancel_monoid_with_zero R] [nontrivial R] :

is_regular a ↔ a ≠ 0

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