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.

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

  Multiplication in a boolean ring is idempotent.

instance instIdempotentOpHMulInstHMulToMulToNonUnitalNonAssocRingToNonAssocRingToRing {α : Type u_1} [BooleanRing α] : Std.IdempotentOp fun (x x_1 : α) => x * x_1

Equations

• (_ : Std.IdempotentOp fun (x x_1 : α) => x * x_1) = (_ : Std.IdempotentOp fun (x x_1 : α) => x * x_1)

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• BooleanRing.toCommRing = let src := inferInstance; CommRing.mk (_ : ∀ (a b : α), a * b = b * a)

instance instBooleanRingPUnit : BooleanRing PUnit.{u_4 + 1}

Equations

• instBooleanRingPUnit = BooleanRing.mk 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 : AsBoolAlg α} {b : AsBoolAlg α} : ofBoolAlg a = ofBoolAlg b ↔ a = b

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

Equations

• instInhabitedAsBoolAlg = inst

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

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

Equations

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

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

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

Equations

• BooleanRing.inf = { inf := fun (x x_1 : α) => x * x_1 }

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

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 instBooleanAlgebraAsBoolAlg {α : Type u_1} [BooleanRing α] : BooleanAlgebra (AsBoolAlg α)

Equations

• instBooleanAlgebraAsBoolAlg = BooleanRing.toBooleanAlgebra

@[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 : AsBoolAlg α) (b : AsBoolAlg α) : ofBoolAlg (a ⊔ b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b

@[simp]

theorem ofBoolAlg_inf {α : Type u_1} [BooleanRing α] (a : AsBoolAlg α) (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 : AsBoolAlg α) (b : AsBoolAlg α) : ofBoolAlg (a \ b) = ofBoolAlg a * (1 + ofBoolAlg b)

@[simp]

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

@[simp]

theorem ofBoolAlg_mul_ofBoolAlg_eq_left_iff {α : Type u_1} [BooleanRing α] {a : AsBoolAlg α} {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)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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 : AsBoolRing α} {b : AsBoolRing α} : ofBoolRing a = ofBoolRing b ↔ a = b

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

Equations

• instInhabitedAsBoolRing = inst

@[reducible]

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

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

• GeneralizedBooleanAlgebra.toNonUnitalCommRing = NonUnitalCommRing.mk (_ : ∀ (x x_1 : α), x ⊓ x_1 = x_1 ⊓ x)

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

Equations

• instNonUnitalCommRingAsBoolRing = GeneralizedBooleanAlgebra.toNonUnitalCommRing

@[reducible]

def 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

• BooleanAlgebra.toBooleanRing = let src := GeneralizedBooleanAlgebra.toNonUnitalCommRing; BooleanRing.mk (_ : ∀ (b : α), b ⊓ b = b)

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

Equations

• instBooleanRingAsBoolRing = BooleanAlgebra.toBooleanRing

@[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 : AsBoolRing α) (b : AsBoolRing α) : ofBoolRing (a + b) = symmDiff (ofBoolRing a) (ofBoolRing b)

@[simp]

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

@[simp]

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

@[simp]

theorem ofBoolRing_le_ofBoolRing_iff {α : Type u_1} [BooleanAlgebra α] {a : AsBoolRing α} {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 BoundedLatticeHom.asBoolRing_apply {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : ∀ (a : AsBoolRing α), (BoundedLatticeHom.asBoolRing f) a = (⇑toBoolRing ∘ ⇑f ∘ ⇑ofBoolRing) a

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

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

@[simp]

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

@[simp]

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

Equivalence between Boolean rings and Boolean algebras

@[simp]

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

@[simp]

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

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' := (_ : ∀ {a b : AsBoolAlg (AsBoolRing α)}, ofBoolRing a ≤ ofBoolRing b ↔ a ≤ b) }

@[simp]

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

@[simp]

theorem RingEquiv.asBoolRingAsBoolAlg_symm_apply (α : Type u_4) [BooleanRing α] : ∀ (a : α), (RingEquiv.symm (RingEquiv.asBoolRingAsBoolAlg α)) a = toBoolRing (toBoolAlg 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

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

instance instBooleanRingBool : BooleanRing Bool

Equations

• instBooleanRingBool = BooleanRing.mk Bool.and_self