Boolean algebra structure on idempotents in a commutative (semi)ring

We show that the idempotent in a commutative ring form a Boolean algebra, with complement given by a ↦ 1 - a and infimum given by multiplication. In a commutative semiring where subtraction is not available, it is still true that pairs of elements (a, b) satisfying a * b = 0 and a + b = 1 form a Boolean algebra (such elements are automatically idempotents, and such a pair is uniquely determined by either a or b).

@[implicit_reducible]

instance instComplSubtypeProdAndEqHMulFstSndOfNatHAdd {R : Type u_1} [CommMonoid R] [AddCommMonoid R] : Compl { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

theorem eq_of_mul_eq_add_eq_one {R : Type u_1} [NonAssocSemiring R] (a : R) {b c : R} (mul : a * b = c * a) (add_ab : a + b = 1) (add_ac : a + c = 1) : b = c

theorem mul_eq_zero_add_eq_one_ext_left {R : Type u_1} [CommSemiring R] {a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }} (eq : (↑a).1 = (↑b).1) : a = b

theorem mul_eq_zero_add_eq_one_ext_right {R : Type u_1} [CommSemiring R] {a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }} (eq : (↑a).2 = (↑b).2) : a = b

@[implicit_reducible]

instance instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd {R : Type u_1} [CommSemiring R] : PartialOrder { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

@[implicit_reducible]

instance instSemilatticeSupSubtypeProdAndEqHMulFstSndOfNatHAdd {R : Type u_1} [CommSemiring R] : SemilatticeSup { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

@[implicit_reducible]

instance instBooleanAlgebraSubtypeProdAndEqHMulFstSndOfNatHAdd {R : Type u_1} [CommSemiring R] : BooleanAlgebra { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

@[implicit_reducible]

instance instSemilatticeInfSubtypeIsIdempotentElem {S : Type u_2} [CommSemigroup S] : SemilatticeInf { a : S // IsIdempotentElem a }

@[implicit_reducible]

instance instOrderTopSubtypeIsIdempotentElem {M : Type u_2} [CommMonoid M] : OrderTop { a : M // IsIdempotentElem a }

@[implicit_reducible]

instance instOrderBotSubtypeIsIdempotentElem {M₀ : Type u_2} [CommMonoidWithZero M₀] : OrderBot { a : M₀ // IsIdempotentElem a }

@[implicit_reducible]

instance instLatticeSubtypeIsIdempotentElem {R : Type u_1} [CommRing R] : Lattice { a : R // IsIdempotentElem a }

@[implicit_reducible]

instance instBooleanAlgebraSubtypeIsIdempotentElem {R : Type u_1} [CommRing R] : BooleanAlgebra { a : R // IsIdempotentElem a }

def OrderIso.isIdempotentElemMulZeroAddOne {R : Type u_1} [CommRing R] : { a : R // IsIdempotentElem a } ≃o { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

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).