mathlib documentation

algebra.ring.boolean_ring

Boolean rings #

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

Main declarations #

Implementation notes #

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

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]
@[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]
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 α) :
@[simp]
theorem of_boolalg_to_boolalg {α : Type u_1} (a : α) :
@[simp]
theorem to_boolalg_inj {α : Type u_1} {a b : α} :
@[simp]
theorem of_boolalg_inj {α : Type u_1} {a b : as_boolalg α} :
@[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

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
@[simp]
theorem of_boolalg_top {α : Type u_1} [boolean_ring α] :
@[simp]
theorem of_boolalg_bot {α : Type u_1} [boolean_ring α] :
@[simp]
@[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 α) :
@[simp]
theorem of_boolalg_sdiff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
@[simp]
theorem of_boolalg_symm_diff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
@[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 : α) :
@[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]
@[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 : α} :
@[simp]
theorem of_boolring_inj {α : Type u_1} {a b : as_boolring α} :
@[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
@[reducible]

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
@[simp]
theorem of_boolring_zero {α : Type u_1} [boolean_algebra α] :
@[simp]
theorem of_boolring_one {α : Type u_1} [boolean_algebra α] :
@[simp, nolint]
theorem of_boolring_neg {α : Type u_1} [boolean_algebra α] (a : as_boolring α) :
@[simp]
theorem of_boolring_add {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
@[simp, nolint]
theorem of_boolring_sub {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
@[simp]
theorem of_boolring_mul {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
@[simp]
theorem of_boolring_le_of_boolring_iff {α : Type u_1} [boolean_algebra α] {a b : as_boolring α} :
@[simp]
theorem to_boolring_bot {α : Type u_1} [boolean_algebra α] :
@[simp]
theorem to_boolring_top {α : Type u_1} [boolean_algebra α] :
@[simp]
theorem to_boolring_inf {α : Type u_1} [boolean_algebra α] (a b : α) :
@[simp]
theorem to_boolring_symm_diff {α : Type u_1} [boolean_algebra α] (a b : α) :
@[protected]
def bounded_lattice_hom.as_boolring {α : Type u_1} {β : Type u_2} [boolean_algebra α] [boolean_algebra β] (f : bounded_lattice_hom α β) :

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} [boolean_algebra α] [boolean_algebra β] (f : bounded_lattice_hom α β) (ᾰ : as_boolring α) :
@[simp]
theorem bounded_lattice_hom.as_boolring_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [boolean_algebra α] [boolean_algebra β] [boolean_algebra γ] (g : bounded_lattice_hom β γ) (f : bounded_lattice_hom α β) :

Equivalence between Boolean rings and Boolean algebras #

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

Equations

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

Equations
@[protected, instance]
Equations