# mathlibdocumentation

algebra.ring.boolean_ring

# Boolean rings #

A Boolean ring is a ring where multiplication is idempotent. They are equivalent to Boolean algebras.

## Main declarations #

• boolean_ring: a typeclass for rings where multiplication is idempotent.
• boolean_ring.to_boolean_algebra: Turn a Boolean ring into a Boolean algebra.
• boolean_algebra.to_boolean_ring: Turn a Boolean algebra into a Boolean ring.
• as_boolalg: Type-synonym for the Boolean algebra associated to a Boolean ring.
• as_boolring: Type-synonym for the Boolean ring associated to a Boolean algebra.

## Implementation notes #

We provide two ways of turning a Boolean algebra/ring into a Boolean ring/algebra:

• Instances on the same type accessible in locales boolean_algebra_of_boolean_ring and boolean_ring_of_boolean_algebra.
• Type-synonyms as_boolalg and as_boolring.

At this point in time, it is not clear the first way is useful, but we keep it for educational purposes and because it is easier than dealing with of_boolalg/to_boolalg/of_boolring/to_boolring explicitly.

## Tags #

boolean ring, boolean algebra

@[class]
structure boolean_ring (α : Type u_4) :
Type u_4
• to_ring : ring α
• mul_self : ∀ (a : α), a * a = a

A Boolean ring is a ring where multiplication is idempotent.

Instances of this typeclass
Instances of other typeclasses for boolean_ring
• boolean_ring.has_sizeof_inst
@[protected, instance]
def has_mul.mul.is_idempotent {α : Type u_1} [boolean_ring α] :
@[simp]
theorem mul_self {α : Type u_1} [boolean_ring α] (a : α) :
a * a = a
@[simp]
theorem add_self {α : Type u_1} [boolean_ring α] (a : α) :
a + a = 0
@[simp]
theorem neg_eq {α : Type u_1} [boolean_ring α] (a : α) :
-a = a
theorem add_eq_zero {α : Type u_1} [boolean_ring α] (a b : α) :
a + b = 0 a = b
@[simp]
theorem mul_add_mul {α : Type u_1} [boolean_ring α] (a b : α) :
a * b + b * a = 0
@[simp]
theorem sub_eq_add {α : Type u_1} [boolean_ring α] (a b : α) :
a - b = a + b
@[simp]
theorem mul_one_add_self {α : Type u_1} [boolean_ring α] (a : α) :
a * (1 + a) = 0
@[protected, instance]
def boolean_ring.to_comm_ring {α : Type u_1} [boolean_ring α] :
Equations
Instances for boolean_ring.to_comm_ring
@[protected, instance]
Equations

### Turning a Boolean ring into a Boolean algebra #

def as_boolalg (α : Type u_1) :
Type u_1

Type synonym to view a Boolean ring as a Boolean algebra.

Equations
• = α
Instances for as_boolalg
def to_boolalg {α : Type u_1} :
α

The "identity" equivalence between as_boolalg α and α.

Equations
def of_boolalg {α : Type u_1} :
α

The "identity" equivalence between α and as_boolalg α.

Equations
@[simp]
theorem to_boolalg_symm_eq {α : Type u_1} :
@[simp]
theorem of_boolalg_symm_eq {α : Type u_1} :
@[simp]
theorem to_boolalg_of_boolalg {α : Type u_1} (a : as_boolalg α) :
= a
@[simp]
theorem of_boolalg_to_boolalg {α : Type u_1} (a : α) :
= a
@[simp]
theorem to_boolalg_inj {α : Type u_1} {a b : α} :
a = b
@[simp]
theorem of_boolalg_inj {α : Type u_1} {a b : as_boolalg α} :
a = b
@[protected, instance]
def as_boolalg.inhabited {α : Type u_1} [inhabited α] :
Equations
def boolean_ring.has_sup {α : Type u_1} [boolean_ring α] :

The join operation in a Boolean ring is x + y + x * y.

Equations
def boolean_ring.has_inf {α : Type u_1} [boolean_ring α] :

The meet operation in a Boolean ring is x * y.

Equations
theorem boolean_ring.sup_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a b = b a
theorem boolean_ring.inf_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a b = b a
theorem boolean_ring.sup_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a b c = a (b c)
theorem boolean_ring.inf_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a b c = a (b c)
theorem boolean_ring.sup_inf_self {α : Type u_1} [boolean_ring α] (a b : α) :
a a b = a
theorem boolean_ring.inf_sup_self {α : Type u_1} [boolean_ring α] (a b : α) :
a (a b) = a
theorem boolean_ring.le_sup_inf_aux {α : Type u_1} [boolean_ring α] (a b c : α) :
(a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c)
theorem boolean_ring.le_sup_inf {α : Type u_1} [boolean_ring α] (a b c : α) :
(a b) (a c) (a b c) = a b c
def boolean_ring.to_boolean_algebra {α : Type u_1} [boolean_ring α] :

The Boolean algebra structure on a Boolean ring.

The data is defined so that:

• a ⊔ b unfolds to a + b + a * b
• a ⊓ b unfolds to a * b
• a ≤ b unfolds to a + b + a * b = b
• ⊥ unfolds to 0
• ⊤ unfolds to 1
• aᶜ unfolds to 1 + a
• a \ b unfolds to a * (1 + b)
Equations
@[protected, instance]
def as_boolalg.boolean_algebra {α : Type u_1} [boolean_ring α] :
Equations
@[simp]
theorem of_boolalg_top {α : Type u_1} [boolean_ring α] :
@[simp]
theorem of_boolalg_bot {α : Type u_1} [boolean_ring α] :
@[simp]
theorem of_boolalg_sup {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
@[simp]
theorem of_boolalg_inf {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
@[simp]
theorem of_boolalg_compl {α : Type u_1} [boolean_ring α] (a : as_boolalg α) :
= 1 +
@[simp]
theorem of_boolalg_sdiff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
of_boolalg (a \ b) = * (1 +
@[simp]
theorem of_boolalg_symm_diff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
@[simp]
theorem of_boolalg_mul_of_boolalg_eq_left_iff {α : Type u_1} [boolean_ring α] {a b : as_boolalg α} :
a b
@[simp]
theorem to_boolalg_zero {α : Type u_1} [boolean_ring α] :
@[simp]
theorem to_boolalg_one {α : Type u_1} [boolean_ring α] :
@[simp]
theorem to_boolalg_mul {α : Type u_1} [boolean_ring α] (a b : α) :
@[simp, nolint]
theorem to_boolalg_add_add_mul {α : Type u_1} [boolean_ring α] (a b : α) :
to_boolalg (a + b + a * b) =
@[simp]
theorem to_boolalg_add {α : Type u_1} [boolean_ring α] (a b : α) :
@[protected]
def ring_hom.as_boolalg {α : Type u_1} {β : Type u_2} [boolean_ring α] [boolean_ring β] (f : α →+* β) :

Turn a ring homomorphism from Boolean rings α to β into a bounded lattice homomorphism from α to β considered as Boolean algebras.

Equations
@[simp]
theorem ring_hom.as_boolalg_to_lattice_hom_to_sup_hom_to_fun {α : Type u_1} {β : Type u_2} [boolean_ring α] [boolean_ring β] (f : α →+* β) (ᾰ : as_boolalg α) :
=
@[simp]
theorem ring_hom.as_boolalg_id {α : Type u_1} [boolean_ring α] :
@[simp]
theorem ring_hom.as_boolalg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [boolean_ring α] [boolean_ring β] [boolean_ring γ] (g : β →+* γ) (f : α →+* β) :

### Turning a Boolean algebra into a Boolean ring #

def as_boolring (α : Type u_1) :
Type u_1

Type synonym to view a Boolean ring as a Boolean algebra.

Equations
• = α
Instances for as_boolring
def to_boolring {α : Type u_1} :
α

The "identity" equivalence between as_boolring α and α.

Equations
def of_boolring {α : Type u_1} :
α

The "identity" equivalence between α and as_boolring α.

Equations
@[simp]
theorem to_boolring_symm_eq {α : Type u_1} :
@[simp]
theorem of_boolring_symm_eq {α : Type u_1} :
@[simp]
theorem to_boolring_of_boolring {α : Type u_1} (a : as_boolring α) :
@[simp]
theorem of_boolring_to_boolring {α : Type u_1} (a : α) :
@[simp]
theorem to_boolring_inj {α : Type u_1} {a b : α} :
a = b
@[simp]
theorem of_boolring_inj {α : Type u_1} {a b : as_boolring α} :
a = b
@[protected, instance]
def as_boolring.inhabited {α : Type u_1} [inhabited α] :
Equations
@[reducible]

Every generalized Boolean algebra has the structure of a non unital commutative ring with the following data:

• a + b unfolds to a ∆ b (symmetric difference)
• a * b unfolds to a ⊓ b
• -a unfolds to a
• 0 unfolds to ⊥
Equations
@[protected, instance]
def as_boolring.non_unital_comm_ring {α : Type u_1}  :
Equations
@[reducible]
def boolean_algebra.to_boolean_ring {α : Type u_1}  :

Every Boolean algebra has the structure of a Boolean ring with the following data:

• a + b unfolds to a ∆ b (symmetric difference)
• a * b unfolds to a ⊓ b
• -a unfolds to a
• 0 unfolds to ⊥
• 1 unfolds to ⊤
Equations
@[protected, instance]
def as_boolring.boolean_ring {α : Type u_1}  :
Equations
@[simp]
theorem of_boolring_zero {α : Type u_1}  :
@[simp]
theorem of_boolring_one {α : Type u_1}  :
@[simp, nolint]
theorem of_boolring_neg {α : Type u_1} (a : as_boolring α) :
@[simp]
theorem of_boolring_add {α : Type u_1} (a b : as_boolring α) :
@[simp, nolint]
theorem of_boolring_sub {α : Type u_1} (a b : as_boolring α) :
@[simp]
theorem of_boolring_mul {α : Type u_1} (a b : as_boolring α) :
@[simp]
theorem of_boolring_le_of_boolring_iff {α : Type u_1} {a b : as_boolring α} :
a * b = a
@[simp]
theorem to_boolring_bot {α : Type u_1}  :
@[simp]
theorem to_boolring_top {α : Type u_1}  :
@[simp]
theorem to_boolring_inf {α : Type u_1} (a b : α) :
@[simp]
theorem to_boolring_symm_diff {α : Type u_1} (a b : α) :
@[protected]
def bounded_lattice_hom.as_boolring {α : Type u_1} {β : Type u_2} (f : β) :

Turn a bounded lattice homomorphism from Boolean algebras α to β into a ring homomorphism from α to β considered as Boolean rings.

Equations
@[simp]
theorem bounded_lattice_hom.as_boolring_apply {α : Type u_1} {β : Type u_2} (f : β) (ᾰ : as_boolring α) :
(f.as_boolring) ᾰ =
@[simp]
theorem bounded_lattice_hom.as_boolring_id {α : Type u_1}  :
@[simp]
theorem bounded_lattice_hom.as_boolring_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : γ) (f : β) :

### Equivalence between Boolean rings and Boolean algebras #

@[simp]
theorem order_iso.as_boolalg_as_boolring_symm_apply (α : Type u_1) (ᾰ : α) :
@[simp]
theorem order_iso.as_boolalg_as_boolring_apply (α : Type u_1) (ᾰ : as_boolalg (as_boolring α)) :
def order_iso.as_boolalg_as_boolring (α : Type u_1)  :
≃o α

Order isomorphism between α considered as a Boolean ring considered as a Boolean algebra and α.

Equations
@[simp]
theorem ring_equiv.as_boolring_as_boolalg_symm_apply (α : Type u_1) [boolean_ring α] (ᾰ : α) :
@[simp]
theorem ring_equiv.as_boolring_as_boolalg_apply (α : Type u_1) [boolean_ring α] (ᾰ : as_boolring (as_boolalg α)) :
def ring_equiv.as_boolring_as_boolalg (α : Type u_1) [boolean_ring α] :
≃+* α

Ring isomorphism between α considered as a Boolean algebra considered as a Boolean ring and α.

Equations
@[protected, instance]
Equations