Mathlib.Algebra.Ring.Idempotent

IsIdempotentElem.one_sub theorem

(h : IsIdempotentElem a) : IsIdempotentElem (1 - a)

Full source

lemma one_sub (h : IsIdempotentElem a) : IsIdempotentElem (1 - a) := by
  rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]

Idempotent Complement: $1 - a$ is idempotent when $a$ is idempotent

Informal description

For any idempotent element $a$ in a ring (i.e., $a \cdot a = a$), the element $1 - a$ is also idempotent.

IsIdempotentElem.one_sub_iff theorem

: IsIdempotentElem (1 - a) ↔ IsIdempotentElem a

Full source

@[simp]
lemma one_sub_iff : IsIdempotentElemIsIdempotentElem (1 - a) ↔ IsIdempotentElem a :=
  ⟨fun h => sub_sub_cancel 1 a ▸ h.one_sub, IsIdempotentElem.one_sub⟩

Characterization of Idempotent Elements via Complement: $(1 - a)^2 = 1 - a \leftrightarrow a^2 = a$

Informal description

For any element $a$ in a ring, $1 - a$ is idempotent (i.e., $(1 - a)^2 = 1 - a$) if and only if $a$ is idempotent (i.e., $a^2 = a$).

IsIdempotentElem.mul_one_sub_self theorem

(h : IsIdempotentElem a) : a * (1 - a) = 0

Full source

@[simp]
lemma mul_one_sub_self (h : IsIdempotentElem a) : a * (1 - a) = 0 := by
  rw [mul_sub, mul_one, h.eq, sub_self]

Product of Idempotent and Its Complement is Zero

Informal description

For any idempotent element $a$ in a ring (i.e., satisfying $a \cdot a = a$), we have $a \cdot (1 - a) = 0$.

IsIdempotentElem.one_sub_mul_self theorem

(h : IsIdempotentElem a) : (1 - a) * a = 0

Full source

@[simp]
lemma one_sub_mul_self (h : IsIdempotentElem a) : (1 - a) * a = 0 := by
  rw [sub_mul, one_mul, h.eq, sub_self]

Annihilation property of $(1 - a) \cdot a$ for idempotent elements

Informal description

For any idempotent element $a$ in a ring (i.e., $a^2 = a$), we have $(1 - a) \cdot a = 0$.

IsIdempotentElem.instHasComplSubtype instance

: HasCompl { a : R // IsIdempotentElem a }

Full source

instance : HasCompl {a : R // IsIdempotentElem a} where compl a := ⟨1 - a, a.prop.one_sub⟩

Complement Operation on Idempotent Elements

Informal description

The set of idempotent elements in a ring $R$ (i.e., elements $a \in R$ satisfying $a^2 = a$) has a complement operation defined by $a^\complement = 1 - a$.

IsIdempotentElem.coe_compl theorem

(a : { a : R // IsIdempotentElem a }) : ↑aᶜ = (1 : R) - ↑a

Full source

@[simp] lemma coe_compl (a : {a : R // IsIdempotentElem a}) : ↑aᶜ = (1 : R) - ↑a := rfl

Complement of Idempotent Element: $a^\complement = 1 - a$

Informal description

For any idempotent element $a$ in a ring $R$ (i.e., $a^2 = a$), the complement of $a$ is given by $1 - a$.

IsIdempotentElem.compl_compl theorem

(a : { a : R // IsIdempotentElem a }) : aᶜᶜ = a

Full source

@[simp] lemma compl_compl (a : {a : R // IsIdempotentElem a}) : aᶜaᶜᶜ = a := by ext; simp

Double Complement of Idempotent Element Equals Itself

Informal description

For any idempotent element $a$ in a ring $R$ (i.e., $a^2 = a$), the double complement of $a$ equals $a$ itself, i.e., $(1 - (1 - a)) = a$.

IsIdempotentElem.zero_compl theorem

: (0 : { a : R // IsIdempotentElem a })ᶜ = 1

Full source

@[simp] lemma zero_compl : (0 : {a : R // IsIdempotentElem a})ᶜ = 1 := by ext; simp

Complement of Zero in Idempotent Elements is One

Informal description

The complement of the zero element in the set of idempotent elements of a ring $R$ is equal to the multiplicative identity $1$, i.e., $0^\complement = 1$.

IsIdempotentElem.one_compl theorem

: (1 : { a : R // IsIdempotentElem a })ᶜ = 0

Full source

@[simp] lemma one_compl : (1 : {a : R // IsIdempotentElem a})ᶜ = 0 := by ext; simp

Complement of One in Idempotent Elements is Zero

Informal description

For the multiplicative identity element $1$ in the set of idempotent elements of a ring $R$, its complement is equal to the additive identity $0$, i.e., $1^\complement = 0$.

IsIdempotentElem.of_mul_add theorem

(mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b

Full source

lemma of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElemIsIdempotentElem a ∧ IsIdempotentElem b := by
  simp_rw [IsIdempotentElem]; constructor
  · conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
  · conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

Idempotent Elements from Complementary Pair

Informal description

Let $a$ and $b$ be elements of a ring such that $a \cdot b = 0$ and $a + b = 1$. Then $a$ and $b$ are both idempotent elements, i.e., $a \cdot a = a$ and $b \cdot b = b$.

IsIdempotentElem.add_sub_mul_of_commute theorem

(h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b)

Full source

lemma add_sub_mul_of_commute (h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
    IsIdempotentElem (a + b - a * b) := by
  convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1
  · simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm]
  · simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq]

Idempotence of $a + b - ab$ for commuting idempotents

Informal description

Let $a$ and $b$ be commuting elements in a ring (i.e., $a \cdot b = b \cdot a$). If both $a$ and $b$ are idempotent (i.e., $a^2 = a$ and $b^2 = b$), then the element $a + b - a \cdot b$ is also idempotent.

IsIdempotentElem.add_sub_mul theorem

(hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b)

Full source

lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
    IsIdempotentElem (a + b - a * b) := add_sub_mul_of_commute (.all ..) hp hq

Idempotence of $a + b - ab$ for idempotent elements

Informal description

Let $a$ and $b$ be elements of a ring. If both $a$ and $b$ are idempotent (i.e., $a^2 = a$ and $b^2 = b$), then the element $a + b - a b$ is also idempotent.