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

instance instHasComplSubtypeProdAndEqHMulFstSndOfNatHAdd {α : Type u_1} [CommMonoid α] [AddCommMonoid α] : HasCompl { a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }

Equations

• instHasComplSubtypeProdAndEqHMulFstSndOfNatHAdd = { compl := fun (a : { a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }) => ⟨((↑a).2, (↑a).1), ⋯⟩ }

theorem eq_of_mul_eq_add_eq_one {α : Type u_1} [Semiring α] (a : α) {b c : α} (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 {α : Type u_1} [CommSemiring α] {a b : { a : α × α // 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 {α : Type u_1} [CommSemiring α] {a b : { a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }} (eq : (↑a).2 = (↑b).2) : a = b

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

Equations

• instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd = PartialOrder.mk ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• instBooleanAlgebraSubtypeProdAndEqHMulFstSndOfNatHAdd = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance instSemilatticeInfSubtypeIsIdempotentElem {α : Type u_1} [CommSemigroup α] : SemilatticeInf { a : α // IsIdempotentElem a }

Equations

• instSemilatticeInfSubtypeIsIdempotentElem = SemilatticeInf.mk (fun (a b : { a : α // IsIdempotentElem a }) => ⟨↑a * ↑b, ⋯⟩) ⋯ ⋯ ⋯

instance instOrderTopSubtypeIsIdempotentElem {α : Type u_1} [CommMonoid α] : OrderTop { a : α // IsIdempotentElem a }

Equations

• instOrderTopSubtypeIsIdempotentElem = OrderTop.mk ⋯

instance instOrderBotSubtypeIsIdempotentElem {α : Type u_1} [CommMonoidWithZero α] : OrderBot { a : α // IsIdempotentElem a }

Equations

• instOrderBotSubtypeIsIdempotentElem = OrderBot.mk ⋯

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

Equations

• instLatticeSubtypeIsIdempotentElem = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

Equations

• instBooleanAlgebraSubtypeIsIdempotentElem = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def OrderIso.isIdempotentElemMulZeroAddOne {α : Type u_1} [CommRing α] : { a : α // IsIdempotentElem a } ≃o { a : α × α // 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).

Equations

• One or more equations did not get rendered due to their size.