Left and right zeros

An element a of a magma is a left zero when a * b = a for every b, and a right zero when b * a = a for every b. A one-sided zero is idempotent, and MulOpposite exchanges the two notions. In a semigroup the left zeros form a left ideal and the right zeros a right ideal.

Main definitions

• IsLeftZero, IsRightZero: the left and right zeros.

Main results

• IsLeftZero.mul_left, IsRightZero.mul_right: the ideal property.
• IsLeftZero.map_of_surjective, IsLeftZero.of_map and their mirrors: transport along surjective and injective homomorphisms.

References

• [Pin]

def IsLeftZero {M : Type u_1} [Mul M] (a : M) : Prop

An element a is a left zero if a * b = a for every b.

Equations

• IsLeftZero a = ∀ (b : M), a * b = a

def IsRightZero {M : Type u_1} [Mul M] (a : M) : Prop

An element a is a right zero if b * a = a for every b.

Equations

• IsRightZero a = ∀ (b : M), b * a = a

theorem isLeftZero_iff {M : Type u_1} [Mul M] {a : M} : IsLeftZero a ↔ ∀ (b : M), a * b = a

theorem isRightZero_iff {M : Type u_1} [Mul M] {a : M} : IsRightZero a ↔ ∀ (b : M), b * a = a

@[simp]

theorem isLeftZero_op {M : Type u_1} [Mul M] {a : M} : IsLeftZero (MulOpposite.op a) ↔ IsRightZero a

@[simp]

theorem isRightZero_op {M : Type u_1} [Mul M] {a : M} : IsRightZero (MulOpposite.op a) ↔ IsLeftZero a

theorem IsLeftZero.isIdempotentElem {M : Type u_1} [Mul M] {a : M} (h : IsLeftZero a) : IsIdempotentElem a

A left zero is idempotent.

theorem IsRightZero.isIdempotentElem {M : Type u_1} [Mul M] {a : M} (h : IsRightZero a) : IsIdempotentElem a

A right zero is idempotent.

theorem IsLeftZero.map_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_3} [Mul M] {a : M} [Mul N] [FunLike F M N] [MulHomClass F M N] {f : F} (h : IsLeftZero a) (hf : Function.Surjective ⇑f) : IsLeftZero (f a)

A surjective homomorphism sends left zeros to left zeros.

theorem IsRightZero.map_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_3} [Mul M] {a : M} [Mul N] [FunLike F M N] [MulHomClass F M N] {f : F} (h : IsRightZero a) (hf : Function.Surjective ⇑f) : IsRightZero (f a)

A surjective homomorphism sends right zeros to right zeros.

theorem IsLeftZero.of_map {M : Type u_1} {N : Type u_2} {F : Type u_3} [Mul M] {a : M} [Mul N] [FunLike F M N] [MulHomClass F M N] {f : F} (h : IsLeftZero (f a)) (hf : Function.Injective ⇑f) : IsLeftZero a

An element sent to a left zero by an injective homomorphism is a left zero.

theorem IsRightZero.of_map {M : Type u_1} {N : Type u_2} {F : Type u_3} [Mul M] {a : M} [Mul N] [FunLike F M N] [MulHomClass F M N] {f : F} (h : IsRightZero (f a)) (hf : Function.Injective ⇑f) : IsRightZero a

An element sent to a right zero by an injective homomorphism is a right zero.

theorem IsLeftZero.mul_left {M : Type u_1} [Semigroup M] {a : M} (h : IsLeftZero a) (b : M) : IsLeftZero (b * a)

In a semigroup, multiplying a left zero on the left gives a left zero.

theorem IsRightZero.mul_right {M : Type u_1} [Semigroup M] {a : M} (h : IsRightZero a) (b : M) : IsRightZero (a * b)

In a semigroup, multiplying a right zero on the right gives a right zero.

@[simp]

theorem isLeftZero_zero {M : Type u_1} [MulZeroClass M] : IsLeftZero 0

@[simp]

theorem isRightZero_zero {M : Type u_1} [MulZeroClass M] : IsRightZero 0