Mathlib.Algebra.Group.Idempotent

Module docstring

{"# 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.pow_succ_eq: In a monoid a ^ (n+1) = a for a an idempotent and n a natural number.

Tags

projection, idempotent "}

IsIdempotentElem definition

[Mul M] (a : M) : Prop

Full source

/-- An element `a` is said to be idempotent if `a * a = a`. -/
def IsIdempotentElem [Mul M] (a : M) : Prop := a * a = a

Idempotent element

Informal description

An element $ a $ of a multiplicative structure $ M $ is called *idempotent* if it satisfies $ a \cdot a = a $.

IsIdempotentElem.of_isIdempotent theorem

[Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a

Full source

lemma of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
  Std.IdempotentOp.idempotent a

Idempotent Elements in an Idempotent Multiplicative Structure

Informal description

For any element $a$ in a multiplicative structure $M$ where the multiplication operation is idempotent (i.e., $x \cdot x = x$ for all $x \in M$), the element $a$ is idempotent, meaning $a \cdot a = a$.

IsIdempotentElem.eq theorem

(ha : IsIdempotentElem a) : a * a = a

Full source

lemma eq (ha : IsIdempotentElem a) : a * a = a := ha

Idempotent Element Property: $a \cdot a = a$

Informal description

For any idempotent element $a$ in a multiplicative structure $M$, we have $a \cdot a = a$.

IsIdempotentElem.mul_of_commute theorem

(hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b)

Full source

lemma mul_of_commute (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
    IsIdempotentElem (a * b) := by rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]

Product of Commuting Idempotents is Idempotent

Informal description

Let $a$ and $b$ be commuting elements in a multiplicative structure $M$ (i.e., $a \cdot b = b \cdot a$). If both $a$ and $b$ are idempotent (i.e., $a \cdot a = a$ and $b \cdot b = b$), then their product $a \cdot b$ is also idempotent, i.e., $(a \cdot b) \cdot (a \cdot b) = a \cdot b$.

IsIdempotentElem.mul theorem

(ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b)

Full source

lemma mul (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b) :=
  ha.mul_of_commute (.all ..) hb

Product of Idempotent Elements is Idempotent

Informal description

For any two idempotent elements $a$ and $b$ in a multiplicative structure $M$ (i.e., $a \cdot a = a$ and $b \cdot b = b$), their product $a \cdot b$ is also idempotent, i.e., $(a \cdot b) \cdot (a \cdot b) = a \cdot b$.

IsIdempotentElem.one theorem

: IsIdempotentElem (1 : M)

Full source

lemma one : IsIdempotentElem (1 : M) := mul_one _

Idempotence of the Multiplicative Identity

Informal description

The multiplicative identity element $1$ in a monoid $M$ is idempotent, i.e., it satisfies $1 \cdot 1 = 1$.

IsIdempotentElem.instOneSubtype instance

: One { a : M // IsIdempotentElem a }

Full source

instance : One {a : M // IsIdempotentElem a} where one := ⟨1, one⟩

Submonoid of Idempotent Elements with Unit

Informal description

The set of idempotent elements in a monoid $M$ forms a submonoid with the multiplicative identity $1$ as its unit element.

IsIdempotentElem.coe_one theorem

: ↑(1 : { a : M // IsIdempotentElem a }) = (1 : M)

Full source

@[simp, norm_cast] lemma coe_one : ↑(1 : {a : M // IsIdempotentElem a}) = (1 : M) := rfl

Inclusion Preserves Identity in Idempotent Submonoid

Informal description

The canonical inclusion map from the submonoid of idempotent elements of $M$ to $M$ maps the multiplicative identity $1$ to itself, i.e., $1_{\{a \in M \mid a^2 = a\}} = 1_M$.

IsIdempotentElem.pow theorem

(n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n)

Full source

lemma pow (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n) :=
  Nat.recOn n ((pow_zero a).symm ▸ one) fun n _ =>
    show a ^ n.succ * a ^ n.succ = a ^ n.succ by
      conv_rhs => rw [← h.eq]
      rw [← sq, ← sq, ← pow_mul, ← pow_mul']

Idempotent Elements are Closed Under Powers: $(a^n)^2 = a^n$

Informal description

For any idempotent element $a$ in a multiplicative structure $M$ and any natural number $n$, the power $a^n$ is also idempotent, i.e., $(a^n) \cdot (a^n) = a^n$.

IsIdempotentElem.pow_succ_eq theorem

(n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a

Full source

lemma pow_succ_eq (n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a :=
  Nat.recOn n ((Nat.zero_add 1).symm ▸ pow_one a) fun n ih => by rw [pow_succ, ih, h.eq]

Power Identity for Idempotent Elements: $a^{n+1} = a$

Informal description

For any idempotent element $a$ in a multiplicative structure and any natural number $n$, we have $a^{n+1} = a$.

IsIdempotentElem.iff_eq_one_of_isUnit theorem

(h : IsUnit a) : IsIdempotentElem a ↔ a = 1

Full source

theorem iff_eq_one_of_isUnit (h : IsUnit a) : IsIdempotentElemIsIdempotentElem a ↔ a = 1 where
  mp idem := by
    have ⟨q, eq⟩ := h.exists_left_inv
    rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
  mpr := by rintro rfl; exact .one

Idempotent Units are Trivial: $a^2 = a \leftrightarrow a = 1$ for units

Informal description

For any unit $a$ in a multiplicative structure, $a$ is idempotent (i.e., $a \cdot a = a$) if and only if $a = 1$.

IsIdempotentElem.iff_eq_one theorem

: IsIdempotentElem a ↔ a = 1

Full source

@[simp] lemma iff_eq_one : IsIdempotentElemIsIdempotentElem a ↔ a = 1 := by simp [IsIdempotentElem]

Idempotent Elements are Trivial in Multiplicative Structures: $a^2 = a \leftrightarrow a = 1$

Informal description

An element $a$ in a multiplicative structure is idempotent (i.e., satisfies $a \cdot a = a$) if and only if $a = 1$.

IsIdempotentElem.map theorem

 {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M} (he : IsIdempotentElem e) (f : F) :
  IsIdempotentElem (f e)

Full source

lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M}
    (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e) := by
  rw [IsIdempotentElem, ← map_mul, he.eq]

Preservation of Idempotence under Homomorphisms: $f(e^2) = f(e)^2$ for idempotent $e$

Informal description

Let $M$ and $N$ be multiplicative structures, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve multiplication. If $e \in M$ is an idempotent element (i.e., $e \cdot e = e$) and $f \colon M \to N$ is a homomorphism in $F$, then the image $f(e)$ is also an idempotent element in $N$ (i.e., $f(e) \cdot f(e) = f(e)$).