Boolean rings

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

Main declarations

• BooleanRing: a typeclass for rings where multiplication is idempotent.
• BooleanRing.toBooleanAlgebra: Turn a Boolean ring into a Boolean algebra.
• BooleanAlgebra.toBooleanRing: Turn a Boolean algebra into a Boolean ring.
• AsBoolAlg: Type-synonym for the Boolean algebra associated to a Boolean ring.
• AsBoolRing: 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 BooleanAlgebraOfBooleanRing and BooleanRingOfBooleanAlgebra.
• Type-synonyms AsBoolAlg and AsBoolRing.

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 ofBoolAlg/toBoolAlg/ofBoolRing/toBoolRing explicitly.

Tags

boolean ring, boolean algebra

class BooleanRing (α : Type u_4) extends Ring α : Type u_4

A Boolean ring is a ring where multiplication is idempotent.

• zero : α
• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : α) : (n + 1) • x = n • x + x
• add_comm (a b : α) : a + b = b + a
• one : α
• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : α) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• neg : α → α
• sub : α → α → α
• zsmul : ℤ → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul_zero' (a : α) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : α) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : α) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• isIdempotentElem (a : α) : IsIdempotentElem a

  Multiplication in a Boolean ring is idempotent.

theorem BooleanRing.mul_self {α : Type u_1} [BooleanRing α] (a : α) : a * a = a

instance BooleanRing.instIdempotentOpHMul {α : Type u_1} [BooleanRing α] : Std.IdempotentOp fun (x1 x2 : α) => x1 * x2

theorem BooleanRing.add_self {α : Type u_1} [BooleanRing α] (a : α) : a + a = 0

theorem BooleanRing.neg_eq {α : Type u_1} [BooleanRing α] (a : α) : -a = a

theorem BooleanRing.add_eq_zero' {α : Type u_1} [BooleanRing α] (a b : α) : a + b = 0 ↔ a = b

@[simp]

theorem BooleanRing.mul_add_mul {α : Type u_1} [BooleanRing α] (a b : α) : a * b + b * a = 0

theorem BooleanRing.sub_eq_add {α : Type u_1} [BooleanRing α] (a b : α) : a - b = a + b

@[simp]

theorem BooleanRing.mul_one_add_self {α : Type u_1} [BooleanRing α] (a : α) : a * (1 + a) = 0

@[instance_reducible, instance 100]

instance BooleanRing.toCommRing {α : Type u_1} [BooleanRing α] : CommRing α

Equations

• BooleanRing.toCommRing = { toRing := inferInstance.toRing, mul_comm := ⋯ }

@[instance_reducible]

instance instBooleanRingPUnit : BooleanRing PUnit.{u_4 + 1}

Equations

• instBooleanRingPUnit = { toRing := PUnit.commRing.toRing, isIdempotentElem := instBooleanRingPUnit._proof_1 }

Turning a Boolean ring into a Boolean algebra

def AsBoolAlg (α : Type u_4) : Type u_4

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

Equations

• AsBoolAlg α = α

def toBoolAlg {α : Type u_1} : α ≃ AsBoolAlg α

The "identity" equivalence between AsBoolAlg α and α.

Equations

• toBoolAlg = Equiv.refl α

def ofBoolAlg {α : Type u_1} : AsBoolAlg α ≃ α

The "identity" equivalence between α and AsBoolAlg α.

Equations

• ofBoolAlg = Equiv.refl (AsBoolAlg α)

@[simp]

theorem toBoolAlg_symm_eq {α : Type u_1} : toBoolAlg.symm = ofBoolAlg

@[simp]

theorem ofBoolAlg_symm_eq {α : Type u_1} : ofBoolAlg.symm = toBoolAlg

@[simp]

theorem toBoolAlg_ofBoolAlg {α : Type u_1} (a : AsBoolAlg α) : toBoolAlg (ofBoolAlg a) = a

@[simp]

theorem ofBoolAlg_toBoolAlg {α : Type u_1} (a : α) : ofBoolAlg (toBoolAlg a) = a

theorem toBoolAlg_inj {α : Type u_1} {a b : α} : toBoolAlg a = toBoolAlg b ↔ a = b

theorem ofBoolAlg_inj {α : Type u_1} {a b : AsBoolAlg α} : ofBoolAlg a = ofBoolAlg b ↔ a = b

def AsBoolAlg.rec {α : Type u_1} {motive : AsBoolAlg α → Sort u_4} (toBoolAlg : (a : α) → motive (toBoolAlg a)) (a : AsBoolAlg α) : motive a

A recursor for AsBoolAlg. Use as induction x.

Equations

• AsBoolAlg.rec toBoolAlg a = toBoolAlg (ofBoolAlg a)

@[instance_reducible]

instance instInhabitedAsBoolAlg {α : Type u_1} [Inhabited α] : Inhabited (AsBoolAlg α)

Equations

• instInhabitedAsBoolAlg = inst✝

@[instance_reducible]

def BooleanRing.sup {α : Type u_1} [BooleanRing α] : Max α

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

Equations

• BooleanRing.sup = { max := fun (x y : α) => x + y + x * y }

@[instance_reducible]

def BooleanRing.inf {α : Type u_1} [BooleanRing α] : Min α

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

Equations

• BooleanRing.inf = { min := fun (x1 x2 : α) => x1 * x2 }

theorem BooleanRing.sup_comm {α : Type u_1} [BooleanRing α] (a b : α) : a ⊔ b = b ⊔ a

theorem BooleanRing.inf_comm {α : Type u_1} [BooleanRing α] (a b : α) : a ⊓ b = b ⊓ a

theorem BooleanRing.sup_assoc {α : Type u_1} [BooleanRing α] (a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

theorem BooleanRing.inf_assoc {α : Type u_1} [BooleanRing α] (a b c : α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

theorem BooleanRing.sup_inf_self {α : Type u_1} [BooleanRing α] (a b : α) : a ⊔ a ⊓ b = a

theorem BooleanRing.inf_sup_self {α : Type u_1} [BooleanRing α] (a b : α) : a ⊓ (a ⊔ b) = a

theorem BooleanRing.le_sup_inf_aux {α : Type u_1} [BooleanRing α] (a b c : α) : (a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c)

theorem BooleanRing.le_sup_inf {α : Type u_1} [BooleanRing α] (a b c : α) : (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c

theorem BooleanRing.sup_def {α : Type u_1} [BooleanRing α] (a b : α) : a ⊔ b = a + b + a * b

theorem BooleanRing.inf_def {α : Type u_1} [BooleanRing α] (a b : α) : a ⊓ b = a * b

@[instance_reducible]

def BooleanRing.toBooleanAlgebra {α : Type u_1} [BooleanRing α] : BooleanAlgebra α

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

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

@[instance_reducible]

instance instBooleanAlgebraAsBoolAlg {α : Type u_1} [BooleanRing α] : BooleanAlgebra (AsBoolAlg α)

Equations

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

@[simp]

theorem ofBoolAlg_top {α : Type u_1} [BooleanRing α] : ofBoolAlg ⊤ = 1

@[simp]

theorem ofBoolAlg_bot {α : Type u_1} [BooleanRing α] : ofBoolAlg ⊥ = 0

@[simp]

theorem ofBoolAlg_sup {α : Type u_1} [BooleanRing α] (a b : AsBoolAlg α) : ofBoolAlg (a ⊔ b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b

@[simp]

theorem ofBoolAlg_inf {α : Type u_1} [BooleanRing α] (a b : AsBoolAlg α) : ofBoolAlg (a ⊓ b) = ofBoolAlg a * ofBoolAlg b

@[simp]

theorem ofBoolAlg_compl {α : Type u_1} [BooleanRing α] (a : AsBoolAlg α) : ofBoolAlg aᶜ = 1 + ofBoolAlg a

@[simp]

theorem ofBoolAlg_sdiff {α : Type u_1} [BooleanRing α] (a b : AsBoolAlg α) : ofBoolAlg (a \ b) = ofBoolAlg a * (1 + ofBoolAlg b)

@[simp]

theorem ofBoolAlg_symmDiff {α : Type u_1} [BooleanRing α] (a b : AsBoolAlg α) : ofBoolAlg (symmDiff a b) = ofBoolAlg a + ofBoolAlg b

@[simp]

theorem ofBoolAlg_mul_ofBoolAlg_eq_left_iff {α : Type u_1} [BooleanRing α] {a b : AsBoolAlg α} : ofBoolAlg a * ofBoolAlg b = ofBoolAlg a ↔ a ≤ b

@[simp]

theorem toBoolAlg_zero {α : Type u_1} [BooleanRing α] : toBoolAlg 0 = ⊥

@[simp]

theorem toBoolAlg_one {α : Type u_1} [BooleanRing α] : toBoolAlg 1 = ⊤

@[simp]

theorem toBoolAlg_mul {α : Type u_1} [BooleanRing α] (a b : α) : toBoolAlg (a * b) = toBoolAlg a ⊓ toBoolAlg b

@[simp]

theorem toBoolAlg_add_add_mul {α : Type u_1} [BooleanRing α] (a b : α) : toBoolAlg (a + b + a * b) = toBoolAlg a ⊔ toBoolAlg b

@[simp]

theorem toBoolAlg_add {α : Type u_1} [BooleanRing α] (a b : α) : toBoolAlg (a + b) = symmDiff (toBoolAlg a) (toBoolAlg b)

def RingHom.asBoolAlg {α : Type u_1} {β : Type u_2} [BooleanRing α] [BooleanRing β] (f : α →+* β) : BoundedLatticeHom (AsBoolAlg α) (AsBoolAlg β)

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

Equations

• f.asBoolAlg = { toFun := ⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

theorem RingHom.asBoolAlg_toFun {α : Type u_1} {β : Type u_2} [BooleanRing α] [BooleanRing β] (f : α →+* β) (a✝ : AsBoolAlg α) : f.asBoolAlg a✝ = (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) a✝

@[simp]

theorem RingHom.asBoolAlg_id {α : Type u_1} [BooleanRing α] : (id α).asBoolAlg = BoundedLatticeHom.id (AsBoolAlg α)

@[simp]

theorem RingHom.asBoolAlg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BooleanRing α] [BooleanRing β] [BooleanRing γ] (g : β →+* γ) (f : α →+* β) : (g.comp f).asBoolAlg = g.asBoolAlg.comp f.asBoolAlg

Turning a Boolean algebra into a Boolean ring

def AsBoolRing (α : Type u_4) : Type u_4

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

Equations

• AsBoolRing α = α

def toBoolRing {α : Type u_1} : α ≃ AsBoolRing α

The "identity" equivalence between AsBoolRing α and α.

Equations

• toBoolRing = Equiv.refl α

def ofBoolRing {α : Type u_1} : AsBoolRing α ≃ α

The "identity" equivalence between α and AsBoolRing α.

Equations

• ofBoolRing = Equiv.refl (AsBoolRing α)

@[simp]

theorem toBoolRing_symm_eq {α : Type u_1} : toBoolRing.symm = ofBoolRing

@[simp]

theorem ofBoolRing_symm_eq {α : Type u_1} : ofBoolRing.symm = toBoolRing

@[simp]

theorem toBoolRing_ofBoolRing {α : Type u_1} (a : AsBoolRing α) : toBoolRing (ofBoolRing a) = a

@[simp]

theorem ofBoolRing_toBoolRing {α : Type u_1} (a : α) : ofBoolRing (toBoolRing a) = a

theorem toBoolRing_inj {α : Type u_1} {a b : α} : toBoolRing a = toBoolRing b ↔ a = b

theorem ofBoolRing_inj {α : Type u_1} {a b : AsBoolRing α} : ofBoolRing a = ofBoolRing b ↔ a = b

def AsBoolRing.rec {α : Type u_1} {motive : AsBoolRing α → Sort u_4} (toBoolRing : (a : α) → motive (toBoolRing a)) (a : AsBoolRing α) : motive a

A recursor for AsBoolRing. Use as induction x.

Equations

• AsBoolRing.rec toBoolRing a = toBoolRing (ofBoolRing a)

@[instance_reducible]

instance instInhabitedAsBoolRing {α : Type u_1} [Inhabited α] : Inhabited (AsBoolRing α)

Equations

• instInhabitedAsBoolRing = { default := default }

@[reducible, inline]

abbrev GeneralizedBooleanAlgebra.toNonUnitalCommRing {α : Type u_1} [GeneralizedBooleanAlgebra α] : NonUnitalCommRing α

Every generalized Boolean algebra has the structure of a nonunital 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

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

@[instance_reducible]

instance instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra {α : Type u_1} [GeneralizedBooleanAlgebra α] : NonUnitalCommRing (AsBoolRing α)

Equations

• instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra = GeneralizedBooleanAlgebra.toNonUnitalCommRing

@[reducible, inline]

abbrev BooleanAlgebra.toBooleanRing {α : Type u_1} [BooleanAlgebra α] : BooleanRing α

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

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

@[instance_reducible]

instance instBooleanRingAsBoolRing {α : Type u_1} [BooleanAlgebra α] : BooleanRing (AsBoolRing α)

Equations

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

@[simp]

theorem ofBoolRing_zero {α : Type u_1} [BooleanAlgebra α] : ofBoolRing 0 = ⊥

@[simp]

theorem ofBoolRing_one {α : Type u_1} [BooleanAlgebra α] : ofBoolRing 1 = ⊤

@[simp]

theorem ofBoolRing_neg {α : Type u_1} [BooleanAlgebra α] (a : AsBoolRing α) : ofBoolRing (-a) = ofBoolRing a

@[simp]

theorem ofBoolRing_add {α : Type u_1} [BooleanAlgebra α] (a b : AsBoolRing α) : ofBoolRing (a + b) = symmDiff (ofBoolRing a) (ofBoolRing b)

@[simp]

theorem ofBoolRing_sub {α : Type u_1} [BooleanAlgebra α] (a b : AsBoolRing α) : ofBoolRing (a - b) = symmDiff (ofBoolRing a) (ofBoolRing b)

@[simp]

theorem ofBoolRing_mul {α : Type u_1} [BooleanAlgebra α] (a b : AsBoolRing α) : ofBoolRing (a * b) = ofBoolRing a ⊓ ofBoolRing b

@[simp]

theorem ofBoolRing_le_ofBoolRing_iff {α : Type u_1} [BooleanAlgebra α] {a b : AsBoolRing α} : ofBoolRing a ≤ ofBoolRing b ↔ a * b = a

@[simp]

theorem toBoolRing_bot {α : Type u_1} [BooleanAlgebra α] : toBoolRing ⊥ = 0

@[simp]

theorem toBoolRing_top {α : Type u_1} [BooleanAlgebra α] : toBoolRing ⊤ = 1

@[simp]

theorem toBoolRing_inf {α : Type u_1} [BooleanAlgebra α] (a b : α) : toBoolRing (a ⊓ b) = toBoolRing a * toBoolRing b

@[simp]

theorem toBoolRing_symmDiff {α : Type u_1} [BooleanAlgebra α] (a b : α) : toBoolRing (symmDiff a b) = toBoolRing a + toBoolRing b

@[simp]

theorem toBoolRing_compl {α : Type u_1} [BooleanAlgebra α] (a : α) : toBoolRing aᶜ = 1 + toBoolRing a

@[simp]

theorem toBoolRing_sup {α : Type u_1} [BooleanAlgebra α] (a b : α) : toBoolRing (a ⊔ b) = toBoolRing a + toBoolRing b + toBoolRing a * toBoolRing b

@[simp]

theorem toBoolRing_sdiff {α : Type u_1} [BooleanAlgebra α] (a b : α) : toBoolRing (a \ b) = toBoolRing a * (1 + toBoolRing b)

def BoundedLatticeHom.asBoolRing {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : AsBoolRing α →+* AsBoolRing β

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

Equations

• f.asBoolRing = { toFun := ⇑toBoolRing ∘ ⇑f ∘ ⇑ofBoolRing, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem BoundedLatticeHom.asBoolRing_apply {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (a✝ : AsBoolRing α) : f.asBoolRing a✝ = (⇑toBoolRing ∘ ⇑f ∘ ⇑ofBoolRing) a✝

@[simp]

theorem BoundedLatticeHom.asBoolRing_id {α : Type u_1} [BooleanAlgebra α] : (BoundedLatticeHom.id α).asBoolRing = RingHom.id (AsBoolRing α)

@[simp]

theorem BoundedLatticeHom.asBoolRing_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ] (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) : (g.comp f).asBoolRing = g.asBoolRing.comp f.asBoolRing

Equivalence between Boolean rings and Boolean algebras

def OrderIso.asBoolAlgAsBoolRing (α : Type u_4) [BooleanAlgebra α] : AsBoolAlg (AsBoolRing α) ≃o α

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

Equations

• OrderIso.asBoolAlgAsBoolRing α = { toEquiv := ofBoolAlg.trans ofBoolRing, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.asBoolAlgAsBoolRing_apply (α : Type u_4) [BooleanAlgebra α] (a✝ : AsBoolAlg (AsBoolRing α)) : (asBoolAlgAsBoolRing α) a✝ = ofBoolRing (ofBoolAlg a✝)

@[simp]

theorem OrderIso.asBoolAlgAsBoolRing_symm_apply (α : Type u_4) [BooleanAlgebra α] (a✝ : α) : (RelIso.symm (asBoolAlgAsBoolRing α)) a✝ = toBoolAlg (toBoolRing a✝)

def RingEquiv.asBoolRingAsBoolAlg (α : Type u_4) [BooleanRing α] : AsBoolRing (AsBoolAlg α) ≃+* α

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

Equations

• RingEquiv.asBoolRingAsBoolAlg α = { toEquiv := ofBoolRing.trans ofBoolAlg, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingEquiv.asBoolRingAsBoolAlg_apply (α : Type u_4) [BooleanRing α] (a✝ : AsBoolRing (AsBoolAlg α)) : (asBoolRingAsBoolAlg α) a✝ = ofBoolAlg (ofBoolRing a✝)

@[simp]

theorem RingEquiv.asBoolRingAsBoolAlg_symm_apply (α : Type u_4) [BooleanRing α] (a✝ : α) : (asBoolRingAsBoolAlg α).symm a✝ = toBoolRing (toBoolAlg a✝)

@[instance_reducible]

instance instZeroBool_mathlib : Zero Bool

Equations

• instZeroBool_mathlib = { zero := false }

@[instance_reducible]

instance instOneBool_mathlib : One Bool

Equations

• instOneBool_mathlib = { one := true }

@[instance_reducible]

instance instAddBool_mathlib : Add Bool

Equations

• instAddBool_mathlib = { add := xor }

@[instance_reducible]

instance instNegBool_mathlib : Neg Bool

Equations

• instNegBool_mathlib = { neg := id }

@[instance_reducible]

instance instSubBool_mathlib : Sub Bool

Equations

• instSubBool_mathlib = { sub := xor }

@[instance_reducible]

instance instMulBool_mathlib : Mul Bool

Equations

• instMulBool_mathlib = { mul := and }

@[instance_reducible]

instance instBooleanRingBool : BooleanRing Bool

Equations

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

theorem Bool.zero_eq_false : 0 = false

theorem Bool.one_eq_true : 1 = true

theorem Bool.add_eq_xor (b c : Bool) : b + c = (b ^^ c)

theorem Bool.neg_eq_id (b : Bool) : -b = b

theorem Bool.sub_eq_xor (b c : Bool) : b - c = (b ^^ c)

theorem Bool.mul_eq_and (b c : Bool) : b * c = (b && c)