Idempotent elements of a ring

This file proves result about idempotent elements of a ring, like:

• IsIdempotentElem.one_sub_iff: In a (non-associative) ring, a is an idempotent if and only if 1 - a is an idempotent.

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

@[simp]

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

@[simp]

theorem IsIdempotentElem.mul_one_sub_self {R : Type u_1} [NonAssocRing R] {a : R} (h : IsIdempotentElem a) : a * (1 - a) = 0

@[simp]

theorem IsIdempotentElem.one_sub_mul_self {R : Type u_1} [NonAssocRing R] {a : R} (h : IsIdempotentElem a) : (1 - a) * a = 0

theorem isIdempotentElem_iff_mul_one_sub_self {R : Type u_1} [NonAssocRing R] {a : R} : IsIdempotentElem a ↔ a * (1 - a) = 0

theorem isIdempotentElem_iff_one_sub_mul_self {R : Type u_1} [NonAssocRing R] {a : R} : IsIdempotentElem a ↔ (1 - a) * a = 0

@[instance_reducible]

instance IsIdempotentElem.instComplSubtype {R : Type u_1} [NonAssocRing R] : Compl { a : R // IsIdempotentElem a }

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem IsIdempotentElem.of_mul_add {R : Type u_1} [Semiring R] {a b : R} (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b

theorem IsIdempotentElem.add_sub_mul_of_commute {R : Type u_1} [NonUnitalRing R] {a b : R} (h : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b)

theorem IsIdempotentElem.add_sub_mul {R : Type u_1} [CommRing R] {a b : R} (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b)

theorem IsIdempotentElem.add {R : Type u_1} [NonUnitalNonAssocSemiring R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hab : a * b + b * a = 0) : IsIdempotentElem (a + b)

a + b is idempotent when a and b anti-commute.

theorem IsIdempotentElem.add_iff {R : Type u_1} [NonUnitalNonAssocSemiring R] [IsCancelAdd R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a + b) ↔ a * b + b * a = 0

a + b is idempotent if and only if a and b anti-commute.

theorem IsIdempotentElem.sub {R : Type u_1} [NonUnitalNonAssocRing R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a)

b - a is idempotent when a * b = a and b * a = a.

theorem IsIdempotentElem.mul_eq_zero_of_anticommute {R : Type u_1} {a b : R} [NonUnitalSemiring R] [HasUniqueDiv R] (ha : IsIdempotentElem a) (hab : a * b + b * a = 0) : a * b = 0

If idempotent a and element b anti-commute, then their product is zero.

theorem IsIdempotentElem.commute_of_anticommute {R : Type u_1} {a b : R} [NonUnitalSemiring R] [HasUniqueDiv R] (ha : IsIdempotentElem a) (hab : a * b + b * a = 0) : Commute a b

If idempotent a and element b anti-commute, then they commute. So anti-commutativity implies commutativity when one of them is idempotent.

theorem IsIdempotentElem.sub_iff {R : Type u_1} [NonUnitalRing R] [HasUniqueDiv R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p