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.one_sub_iff: In a (non-associative) ring, p is an idempotent if and only if 1-p is an idempotent.
• IsIdempotentElem.pow_succ_eq: In a monoid p ^ (n+1) = p for p an idempotent and n a natural number.

Tags

projection, idempotent

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

An element p is said to be idempotent if p * p = p

Equations

• IsIdempotentElem p = (p * p = p)

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] {p : M} (h : IsIdempotentElem p) : p * p = p

theorem IsIdempotentElem.mul_of_commute {S : Type u_3} [Semigroup S] {p q : S} (h : Commute p q) (h₁ : IsIdempotentElem p) (h₂ : IsIdempotentElem q) : IsIdempotentElem (p * q)

theorem IsIdempotentElem.mul {M : Type u_9} [CommSemigroup M] {e₁ e₂ : M} (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) : IsIdempotentElem (e₁ * e₂)

theorem IsIdempotentElem.zero {M₀ : Type u_4} [MulZeroClass M₀] : IsIdempotentElem 0

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

theorem IsIdempotentElem.one_sub {R : Type u_6} [NonAssocRing R] {p : R} (h : IsIdempotentElem p) : IsIdempotentElem (1 - p)

@[simp]

theorem IsIdempotentElem.one_sub_iff {R : Type u_6} [NonAssocRing R] {p : R} : IsIdempotentElem (1 - p) ↔ IsIdempotentElem p

theorem IsIdempotentElem.add_sub_mul_of_commute {R : Type u_9} [Ring R] {p q : R} (h : Commute p q) (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (p + q - p * q)

theorem IsIdempotentElem.add_sub_mul {R : Type u_9} [CommRing R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (p + q - p * q)

theorem IsIdempotentElem.pow {N : Type u_2} [Monoid N] {p : N} (n : ℕ) (h : IsIdempotentElem p) : IsIdempotentElem (p ^ n)

theorem IsIdempotentElem.pow_succ_eq {N : Type u_2} [Monoid N] {p : N} (n : ℕ) (h : IsIdempotentElem p) : p ^ (n + 1) = p

@[simp]

theorem IsIdempotentElem.iff_eq_one {G : Type u_7} [Group G] {p : G} : IsIdempotentElem p ↔ p = 1

@[simp]

theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_8} [CancelMonoidWithZero G₀] {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1

theorem IsIdempotentElem.map {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M} (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e)

Instances on Subtype IsIdempotentElem

instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_4} [MulZeroClass M₀] : Zero { p : M₀ // IsIdempotentElem p }

Equations

• IsIdempotentElem.instZeroSubtype = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem IsIdempotentElem.coe_zero {M₀ : Type u_4} [MulZeroClass M₀] : ↑0 = 0

instance IsIdempotentElem.instOneSubtype {M₁ : Type u_5} [MulOneClass M₁] : One { p : M₁ // IsIdempotentElem p }

Equations

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

@[simp]

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

instance IsIdempotentElem.instHasComplSubtype {R : Type u_6} [NonAssocRing R] : HasCompl { p : R // IsIdempotentElem p }

Equations

• IsIdempotentElem.instHasComplSubtype = { compl := fun (p : { p : R // IsIdempotentElem p }) => ⟨1 - ↑p, ⋯⟩ }

@[simp]

theorem IsIdempotentElem.coe_compl {R : Type u_6} [NonAssocRing R] (p : { p : R // IsIdempotentElem p }) : ↑pᶜ = 1 - ↑p

@[simp]

theorem IsIdempotentElem.compl_compl {R : Type u_6} [NonAssocRing R] (p : { p : R // IsIdempotentElem p }) : pᶜᶜ = p

@[simp]

theorem IsIdempotentElem.zero_compl {R : Type u_6} [NonAssocRing R] : 0ᶜ = 1

@[simp]

theorem IsIdempotentElem.one_compl {R : Type u_6} [NonAssocRing R] : 1ᶜ = 0