Idempotents

This file defines idempotents for an arbitrary multiplication and proves some basic results, including:

• IsIdempotentElem.mul_of_commute: In a semigroup, the product of two commuting idempotents is an idempotent;
• IsIdempotentElem.pow_succ_eq: In a monoid a ^ (n+1) = a for a an idempotent and n a natural number.

Tags

projection, idempotent

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

An element a is said to be idempotent if a * a = a.

Equations

• IsIdempotentElem a = (a * a = a)

theorem isIdempotentElem_iff {M : Type u_1} [Mul M] {a : M} : IsIdempotentElem a ↔ a * a = a

theorem IsIdempotentElem.of_isIdempotent {M : Type u_1} [Mul M] [Std.IdempotentOp fun (x1 x2 : M) => x1 * x2] (a : M) : IsIdempotentElem a

theorem IsIdempotentElem.eq {M : Type u_1} [Mul M] {a : M} (ha : IsIdempotentElem a) : a * a = a

theorem IsIdempotentElem.mul_of_commute {S : Type u_3} [Semigroup S] {a b : S} (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b)

theorem IsIdempotentElem.mul {S : Type u_3} [CommSemigroup S] {a b : S} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b)

theorem IsIdempotentElem.one {M : Type u_1} [MulOneClass M] : IsIdempotentElem 1

@[instance_reducible]

instance IsIdempotentElem.instOneSubtype {M : Type u_1} [MulOneClass M] : One { a : M // IsIdempotentElem a }

Equations

• IsIdempotentElem.instOneSubtype = { one := ⟨1, ⋯⟩ }

@[simp]

theorem IsIdempotentElem.coe_one {M : Type u_1} [MulOneClass M] : ↑1 = 1

theorem IsIdempotentElem.pow {M : Type u_1} [Monoid M] {a : M} (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n)

theorem IsIdempotentElem.pow_succ_eq {M : Type u_1} [Monoid M] {a : M} (n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a

theorem IsIdempotentElem.pow_eq {M : Type u_1} [Monoid M] {a : M} (h : IsIdempotentElem a) {n : ℕ} (hn : n ≠ 0) : a ^ n = a

theorem IsIdempotentElem.iff_eq_one_of_isUnit {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : IsIdempotentElem a ↔ a = 1

@[simp]

theorem IsIdempotentElem.iff_eq_one {M : Type u_1} [CancelMonoid M] {a : M} : IsIdempotentElem a ↔ a = 1

theorem IsIdempotentElem.map {M : Type u_4} {N : Type u_5} {F : Type u_6} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M} (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e)

theorem IsIdempotentElem.mul_mul_self {M : Type u_4} [Semigroup M] {x : M} (hx : IsIdempotentElem x) (y : M) : y * x * x = y * x

theorem IsIdempotentElem.mul_self_mul {M : Type u_4} [Semigroup M] {x : M} (hx : IsIdempotentElem x) (y : M) : x * (x * y) = x * y