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

source

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)

Instances For

source

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

IsIdempotentElem a

source

theorem IsIdempotentElem.eq {M : Type u_1} [Mul M] {p : M} (h : IsIdempotentElem p) :

p * p = p

source

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

IsIdempotentElem (p * q)

source

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

IsIdempotentElem 0

source

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

IsIdempotentElem 1

source

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

IsIdempotentElem (1 - p)

source

@[simp]

theorem IsIdempotentElem.one_sub_iff {R : Type u_6} [NonAssocRing R] {p : R} :

IsIdempotentElem (1 - p) ↔ IsIdempotentElem p

source

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

IsIdempotentElem (p ^ n)

source

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

p ^ (n + 1) = p

source

@[simp]

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

IsIdempotentElem p ↔ p = 1

source

@[simp]

theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_8} [CancelMonoidWithZero G₀] {p : G₀} :

IsIdempotentElem p ↔ p = 0 ∨ p = 1

Instances on `Subtype IsIdempotentElem` #

source

instance IsIdempotentElem.instZeroSubtypeIsIdempotentElemToMul {M₀ : Type u_4} [MulZeroClass M₀] :

Zero { p : M₀ // IsIdempotentElem p }

Equations

IsIdempotentElem.instZeroSubtypeIsIdempotentElemToMul = { zero := { val := 0, property := ⋯ } }

source

@[simp]

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

↑0 = 0

source

instance IsIdempotentElem.instOneSubtypeIsIdempotentElemToMul {M₁ : Type u_5} [MulOneClass M₁] :

One { p : M₁ // IsIdempotentElem p }

Equations

IsIdempotentElem.instOneSubtypeIsIdempotentElemToMul = { one := { val := 1, property := ⋯ } }

source

@[simp]

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

↑1 = 1

source

instance IsIdempotentElem.instHasComplSubtypeIsIdempotentElemToMulToNonUnitalNonAssocRing {R : Type u_6} [NonAssocRing R] :

HasCompl { p : R // IsIdempotentElem p }

Equations

IsIdempotentElem.instHasComplSubtypeIsIdempotentElemToMulToNonUnitalNonAssocRing = { compl := fun (p : { p : R // IsIdempotentElem p }) => { val := 1 - ↑p, property := ⋯ } }