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

@[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)