English
There is an order isomorphism between the set of idempotent elements and the pair-set E given by a ↦ (a, 1−a) with inverse (x,y) ↦ x and y derived from the idempotent condition.
Русский
Существует изоморфизм порядков между множеством идемпотентных элементов и множеством пар E, задаваемый отображением a ↦ (a, 1−a) с обратным отображением из пары.
LaTeX
$$$\phi: {a\in R\mid a^2=a} \to E, \; \phi(a) = (a,1-a)$, and its inverse, giving an order isomorphism.$$
Lean4
/-- In a commutative ring, the idempotents are in 1-1 correspondence with pairs of elements
whose product is 0 and whose sum is 1. The correspondence is given by `a ↔ (a, 1 - a)`. -/
def isIdempotentElemMulZeroAddOne : { a : R // IsIdempotentElem a } ≃o { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
where
toFun a := ⟨(a, 1 - a), by simp_rw [mul_sub, mul_one, a.2.eq, sub_self], by rw [add_sub_cancel]⟩
invFun a := ⟨a.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1⟩
right_inv a := Subtype.ext <| Prod.ext rfl <| sub_eq_of_eq_add <| a.2.2.symm.trans (add_comm ..)
map_rel_iff' := Iff.rfl
