mathlib3 documentation

algebra.ring.idempotents

Idempotents #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

is_idempotent_elem.mul_of_commute: In a semigroup, the product of two commuting idempotents is an idempotent;
is_idempotent_elem.one_sub_iff: In a (non-associative) ring, p is an idempotent if and only if 1-p is an idempotent.
is_idempotent_elem.pow_succ_eq: In a monoid p ^ (n+1) = p for p an idempotent and n a natural number.

Tags #

projection, idempotent

def is_idempotent_elem {M : Type u_1} [has_mul M] (p : M) :

Prop

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

Equations

is_idempotent_elem p = (p * p = p)

theorem is_idempotent_elem.of_is_idempotent {M : Type u_1} [has_mul M] [is_idempotent M has_mul.mul] (a : M) :

is_idempotent_elem a

theorem is_idempotent_elem.eq {M : Type u_1} [has_mul M] {p : M} (h : is_idempotent_elem p) :

p * p = p

theorem is_idempotent_elem.mul_of_commute {S : Type u_3} [semigroup S] {p q : S} (h : commute p q) (h₁ : is_idempotent_elem p) (h₂ : is_idempotent_elem q) :

is_idempotent_elem (p * q)

theorem is_idempotent_elem.zero {M₀ : Type u_4} [mul_zero_class M₀] :

is_idempotent_elem 0

theorem is_idempotent_elem.one {M₁ : Type u_5} [mul_one_class M₁] :

is_idempotent_elem 1

theorem is_idempotent_elem.one_sub {R : Type u_6} [non_assoc_ring R] {p : R} (h : is_idempotent_elem p) :

is_idempotent_elem (1 - p)

@[simp]

theorem is_idempotent_elem.one_sub_iff {R : Type u_6} [non_assoc_ring R] {p : R} :

is_idempotent_elem (1 - p) ↔ is_idempotent_elem p

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

is_idempotent_elem (p ^ n)

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

p ^ (n + 1) = p

@[simp]

theorem is_idempotent_elem.iff_eq_one {G : Type u_7} [group G] {p : G} :

is_idempotent_elem p ↔ p = 1

@[simp]

theorem is_idempotent_elem.iff_eq_zero_or_one {G₀ : Type u_8} [cancel_monoid_with_zero G₀] {p : G₀} :

is_idempotent_elem p ↔ p = 0 ∨ p = 1

Instances on `subtype is_idempotent_elem` #

@[protected, instance]

def is_idempotent_elem.subtype.has_zero {M₀ : Type u_4} [mul_zero_class M₀] :

has_zero {p // is_idempotent_elem p}

Equations

is_idempotent_elem.subtype.has_zero = {zero := ⟨0, _⟩}

@[simp]

theorem is_idempotent_elem.coe_zero {M₀ : Type u_4} [mul_zero_class M₀] :

↑0 = 0

@[protected, instance]

def is_idempotent_elem.subtype.has_one {M₁ : Type u_5} [mul_one_class M₁] :

has_one {p // is_idempotent_elem p}

Equations

is_idempotent_elem.subtype.has_one = {one := ⟨1, _⟩}

@[simp]

theorem is_idempotent_elem.coe_one {M₁ : Type u_5} [mul_one_class M₁] :

↑1 = 1

@[protected, instance]

def is_idempotent_elem.subtype.has_compl {R : Type u_6} [non_assoc_ring R] :

has_compl {p // is_idempotent_elem p}

Equations

is_idempotent_elem.subtype.has_compl = {compl := λ (p : {p // is_idempotent_elem p}), ⟨1 - ↑p, _⟩}

@[simp]

theorem is_idempotent_elem.coe_compl {R : Type u_6} [non_assoc_ring R] (p : {p // is_idempotent_elem p}) :

↑pᶜ = 1 - ↑p

@[simp]

theorem is_idempotent_elem.compl_compl {R : Type u_6} [non_assoc_ring R] (p : {p // is_idempotent_elem p}) :

@[simp]

theorem is_idempotent_elem.zero_compl {R : Type u_6} [non_assoc_ring R] :

0ᶜ = 1

@[simp]

theorem is_idempotent_elem.one_compl {R : Type u_6} [non_assoc_ring R] :

1ᶜ = 0