mathlib3 documentation

algebra.ring.boolean_ring

Boolean rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[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
source
@[protected, instance]
def has_mul.mul.is_idempotent {α : Type u_1} [boolean_ring α] :
is_idempotent α has_mul.mul
source
@[simp]
theorem mul_self {α : Type u_1} [boolean_ring α] (a : α) :
a * a = a
source
@[simp]
theorem add_self {α : Type u_1} [boolean_ring α] (a : α) :
a + a = 0
source
@[simp]
theorem neg_eq {α : Type u_1} [boolean_ring α] (a : α) :
-a = a
source
theorem add_eq_zero' {α : Type u_1} [boolean_ring α] (a b : α) :
a + b = 0 ↔ a = b
source
@[simp]
theorem mul_add_mul {α : Type u_1} [boolean_ring α] (a b : α) :
a * b + b * a = 0
source
@[simp]
theorem sub_eq_add {α : Type u_1} [boolean_ring α] (a b : α) :
a - b = a + b
source
@[simp]
theorem mul_one_add_self {α : Type u_1} [boolean_ring α] (a : α) :
a * (1 + a) = 0
source
@[protected, instance]
def boolean_ring.to_comm_ring {α : Type u_1} [boolean_ring α] :
comm_ring α
Equations
Instances for boolean_ring.to_comm_ring
source
@[protected, instance]
def punit.boolean_ring  :
boolean_ring punit
Equations

Turning a Boolean ring into a Boolean algebra #

source
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
source
def to_boolalg {α : Type u_1} :
α ≃ as_boolalg α

The "identity" equivalence between as_boolalg α and α.

Equations
source
def of_boolalg {α : Type u_1} :
as_boolalg α ≃ α

The "identity" equivalence between α and as_boolalg α.

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

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

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

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

Equations
source
theorem boolean_ring.sup_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊔ b = b ⊔ a
source
theorem boolean_ring.inf_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ b = b ⊓ a
source
theorem boolean_ring.sup_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
source
theorem boolean_ring.inf_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
source
theorem boolean_ring.sup_inf_self {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊔ a ⊓ b = a
source
theorem boolean_ring.inf_sup_self {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ (a ⊔ b) = a
source
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)
source
theorem boolean_ring.le_sup_inf {α : Type u_1} [boolean_ring α] (a b c : α) :
(a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
source
def boolean_ring.to_boolean_algebra {α : Type u_1} [boolean_ring α] :
boolean_algebra α

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
source
@[protected, instance]
def as_boolalg.boolean_algebra {α : Type u_1} [boolean_ring α] :
boolean_algebra (as_boolalg α)
Equations
source
@[simp]
theorem of_boolalg_top {α : Type u_1} [boolean_ring α] :
⇑of_boolalg ⊤ = 1
source
@[simp]
theorem of_boolalg_bot {α : Type u_1} [boolean_ring α] :
⇑of_boolalg ⊥ = 0
source
@[simp]
theorem of_boolalg_sup {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
⇑of_boolalg (a ⊔ b) = ⇑of_boolalg a + ⇑of_boolalg b + ⇑of_boolalg a * ⇑of_boolalg b
source
@[simp]
theorem of_boolalg_inf {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
⇑of_boolalg (a ⊓ b) = ⇑of_boolalg a * ⇑of_boolalg b
source
@[simp]
theorem of_boolalg_compl {α : Type u_1} [boolean_ring α] (a : as_boolalg α) :
⇑of_boolalg aᶜ = 1 + ⇑of_boolalg a
source
@[simp]
theorem of_boolalg_sdiff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
⇑of_boolalg (a \ b) = ⇑of_boolalg a * (1 + ⇑of_boolalg b)
source
@[simp]
theorem of_boolalg_symm_diff {α : Type u_1} [boolean_ring α] (a b : as_boolalg α) :
⇑of_boolalg (a ∆ b) = ⇑of_boolalg a + ⇑of_boolalg b
source
@[simp]
theorem of_boolalg_mul_of_boolalg_eq_left_iff {α : Type u_1} [boolean_ring α] {a b : as_boolalg α} :
⇑of_boolalg a * ⇑of_boolalg b = ⇑of_boolalg a ↔ a ≤ b
source
@[simp]
theorem to_boolalg_zero {α : Type u_1} [boolean_ring α] :
⇑to_boolalg 0 = ⊥
source
@[simp]
theorem to_boolalg_one {α : Type u_1} [boolean_ring α] :
⇑to_boolalg 1 = ⊤
source
@[simp]
theorem to_boolalg_mul {α : Type u_1} [boolean_ring α] (a b : α) :
⇑to_boolalg (a * b) = ⇑to_boolalg a ⊓ ⇑to_boolalg b
source
@[simp, nolint]
theorem to_boolalg_add_add_mul {α : Type u_1} [boolean_ring α] (a b : α) :
⇑to_boolalg (a + b + a * b) = ⇑to_boolalg a ⊔ ⇑to_boolalg b
source
@[simp]
theorem to_boolalg_add {α : Type u_1} [boolean_ring α] (a b : α) :
⇑to_boolalg (a + b) = ⇑to_boolalg a ∆ ⇑to_boolalg b
source
@[protected]
def ring_hom.as_boolalg {α : Type u_1} {β : Type u_2} [boolean_ring α] [boolean_ring β] (f : α →+* β) :
bounded_lattice_hom (as_boolalg α) (as_boolalg β)

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

Equations
source
@[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 α) :
⇑(f.as_boolalg.to_lattice_hom.to_sup_hom) ᾰ = (⇑to_boolalg ∘ ⇑f ∘ ⇑of_boolalg) ᾰ
source
@[simp]
theorem ring_hom.as_boolalg_id {α : Type u_1} [boolean_ring α] :
(ring_hom.id α).as_boolalg = bounded_lattice_hom.id (as_boolalg α)
source
@[simp]
theorem ring_hom.as_boolalg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [boolean_ring α] [boolean_ring β] [boolean_ring γ] (g : β →+* γ) (f : α →+* β) :
(g.comp f).as_boolalg = g.as_boolalg.comp f.as_boolalg

Turning a Boolean algebra into a Boolean ring #

source
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
source
def to_boolring {α : Type u_1} :
α ≃ as_boolring α

The "identity" equivalence between as_boolring α and α.

Equations
source
def of_boolring {α : Type u_1} :
as_boolring α ≃ α

The "identity" equivalence between α and as_boolring α.

Equations
source
@[simp]
theorem to_boolring_symm_eq {α : Type u_1} :
to_boolring.symm = of_boolring
source
@[simp]
theorem of_boolring_symm_eq {α : Type u_1} :
of_boolring.symm = to_boolring
source
@[simp]
theorem to_boolring_of_boolring {α : Type u_1} (a : as_boolring α) :
⇑to_boolring (⇑of_boolring a) = a
source
@[simp]
theorem of_boolring_to_boolring {α : Type u_1} (a : α) :
⇑of_boolring (⇑to_boolring a) = a
source
@[simp]
theorem to_boolring_inj {α : Type u_1} {a b : α} :
⇑to_boolring a = ⇑to_boolring b ↔ a = b
source
@[simp]
theorem of_boolring_inj {α : Type u_1} {a b : as_boolring α} :
⇑of_boolring a = ⇑of_boolring b ↔ a = b
source
@[protected, instance]
def as_boolring.inhabited {α : Type u_1} [inhabited α] :
inhabited (as_boolring α)
Equations
source
@[reducible]
def generalized_boolean_algebra.to_non_unital_comm_ring {α : Type u_1} [generalized_boolean_algebra α] :
non_unital_comm_ring α

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
source
@[protected, instance]
def as_boolring.non_unital_comm_ring {α : Type u_1} [generalized_boolean_algebra α] :
non_unital_comm_ring (as_boolring α)
Equations
source
@[reducible]
def boolean_algebra.to_boolean_ring {α : Type u_1} [boolean_algebra α] :
boolean_ring α

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
source
@[protected, instance]
def as_boolring.boolean_ring {α : Type u_1} [boolean_algebra α] :
boolean_ring (as_boolring α)
Equations
source
@[simp]
theorem of_boolring_zero {α : Type u_1} [boolean_algebra α] :
⇑of_boolring 0 = ⊥
source
@[simp]
theorem of_boolring_one {α : Type u_1} [boolean_algebra α] :
⇑of_boolring 1 = ⊤
source
@[simp, nolint]
theorem of_boolring_neg {α : Type u_1} [boolean_algebra α] (a : as_boolring α) :
⇑of_boolring (-a) = ⇑of_boolring a
source
@[simp]
theorem of_boolring_add {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
⇑of_boolring (a + b) = ⇑of_boolring a ∆ ⇑of_boolring b
source
@[simp, nolint]
theorem of_boolring_sub {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
⇑of_boolring (a - b) = ⇑of_boolring a ∆ ⇑of_boolring b
source
@[simp]
theorem of_boolring_mul {α : Type u_1} [boolean_algebra α] (a b : as_boolring α) :
⇑of_boolring (a * b) = ⇑of_boolring a ⊓ ⇑of_boolring b
source
@[simp]
theorem of_boolring_le_of_boolring_iff {α : Type u_1} [boolean_algebra α] {a b : as_boolring α} :
⇑of_boolring a ≤ ⇑of_boolring b ↔ a * b = a
source
@[simp]
theorem to_boolring_bot {α : Type u_1} [boolean_algebra α] :
⇑to_boolring ⊥ = 0
source
@[simp]
theorem to_boolring_top {α : Type u_1} [boolean_algebra α] :
⇑to_boolring ⊤ = 1
source
@[simp]
theorem to_boolring_inf {α : Type u_1} [boolean_algebra α] (a b : α) :
⇑to_boolring (a ⊓ b) = ⇑to_boolring a * ⇑to_boolring b
source
@[simp]
theorem to_boolring_symm_diff {α : Type u_1} [boolean_algebra α] (a b : α) :
⇑to_boolring (a ∆ b) = ⇑to_boolring a + ⇑to_boolring b
source
@[protected]
def bounded_lattice_hom.as_boolring {α : Type u_1} {β : Type u_2} [boolean_algebra α] [boolean_algebra β] (f : bounded_lattice_hom α β) :
as_boolring α →+* as_boolring β

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

Equations
source
@[simp]
theorem bounded_lattice_hom.as_boolring_apply {α : Type u_1} {β : Type u_2} [boolean_algebra α] [boolean_algebra β] (f : bounded_lattice_hom α β) (ᾰ : as_boolring α) :
⇑(f.as_boolring) ᾰ = (⇑to_boolring ∘ ⇑f ∘ ⇑of_boolring) ᾰ
source
@[simp]
theorem bounded_lattice_hom.as_boolring_id {α : Type u_1} [boolean_algebra α] :
(bounded_lattice_hom.id α).as_boolring = ring_hom.id (as_boolring α)
source
@[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 α β) :
(g.comp f).as_boolring = g.as_boolring.comp f.as_boolring

Equivalence between Boolean rings and Boolean algebras #

source
@[simp]
theorem order_iso.as_boolalg_as_boolring_symm_apply (α : Type u_1) [boolean_algebra α] (ᾰ : α) :
⇑(rel_iso.symm (order_iso.as_boolalg_as_boolring α)) ᾰ = ⇑to_boolalg (⇑to_boolring ᾰ)
source
@[simp]
theorem order_iso.as_boolalg_as_boolring_apply (α : Type u_1) [boolean_algebra α] (ᾰ : as_boolalg (as_boolring α)) :
⇑(order_iso.as_boolalg_as_boolring α) ᾰ = ⇑of_boolring (⇑of_boolalg ᾰ)
source
def order_iso.as_boolalg_as_boolring (α : Type u_1) [boolean_algebra α] :
as_boolalg (as_boolring α) ≃o α

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

Equations
source
@[simp]
theorem ring_equiv.as_boolring_as_boolalg_symm_apply (α : Type u_1) [boolean_ring α] (ᾰ : α) :
⇑((ring_equiv.as_boolring_as_boolalg α).symm) ᾰ = (of_boolring.trans of_boolalg).inv_fun ᾰ
source
@[simp]
theorem ring_equiv.as_boolring_as_boolalg_apply (α : Type u_1) [boolean_ring α] (ᾰ : as_boolring (as_boolalg α)) :
⇑(ring_equiv.as_boolring_as_boolalg α) ᾰ = (of_boolring.trans of_boolalg).to_fun ᾰ
source
def ring_equiv.as_boolring_as_boolalg (α : Type u_1) [boolean_ring α] :
as_boolring (as_boolalg α) ≃+* α

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

Equations
source
@[protected, instance]
def bool.boolean_ring  :
boolean_ring bool
Equations