Adding complements to a generalized Boolean algebra

This file embeds any generalized Boolean algebra into a Boolean algebra.

This concretely proves that any equation holding true in the theory of Boolean algebras that does not reference ᶜ also holds true in the theory of generalized Boolean algebras. Put another way, one does not need the existence of complements to prove something which does not talk about complements.

Main declarations

• Booleanisation: Boolean algebra containing a given generalised Boolean algebra as a sublattice.
• Booleanisation.liftLatticeHom: Boolean algebra containing a given generalised Boolean algebra as a sublattice.

Future work

If mathlib ever acquires GenBoolAlg, the category of generalised Boolean algebras, then one could show that Booleanisation is the free functor from GenBoolAlg to BoolAlg.

def Booleanisation (α : Type u_2) : Type u_2

Boolean algebra containing a given generalised Boolean algebra α as a sublattice.

This should be thought of as made of a copy of α (representing elements of α) living under another copy of α (representing complements of elements of α).

Equations

• Booleanisation α = (α ⊕ α)

Instances For

• Booleanisation.instBooleanAlgebra
• Booleanisation.instBot
• Booleanisation.instBoundedOrder
• Booleanisation.instCompl
• Booleanisation.instDistribLattice
• Booleanisation.instInf
• Booleanisation.instLE
• Booleanisation.instLT
• Booleanisation.instPartialOrder
• Booleanisation.instPreorder
• Booleanisation.instSDiff
• Booleanisation.instSemilatticeInf
• Booleanisation.instSemilatticeSup
• Booleanisation.instSup
• Booleanisation.instTop

instance Booleanisation.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Booleanisation α)

Equations

• Booleanisation.instDecidableEq = inferInstanceAs (DecidableEq (α ⊕ α))

@[match_pattern]

def Booleanisation.lift {α : Type u_1} : α → Booleanisation α

The natural inclusion a ↦ a from a generalized Boolean algebra to its generated Boolean algebra.

Equations

• Booleanisation.lift = Sum.inl

@[match_pattern]

def Booleanisation.comp {α : Type u_1} : α → Booleanisation α

The inclusion `a ↦ aᶜ from a generalized Boolean algebra to its generated Boolean algebra.

Equations

• Booleanisation.comp = Sum.inr

instance Booleanisation.instCompl {α : Type u_1} : HasCompl (Booleanisation α)

The complement operator on Booleanisation α sends a to aᶜ and aᶜ to a, for a : α.

Equations

• Booleanisation.instCompl = { compl := fun (x : Booleanisation α) => match x with | Sum.inl a => Booleanisation.comp a | Sum.inr a => Booleanisation.lift a }

@[simp]

theorem Booleanisation.compl_lift {α : Type u_1} (a : α) : (Booleanisation.lift a)ᶜ = Booleanisation.comp a

@[simp]

theorem Booleanisation.compl_comp {α : Type u_1} (a : α) : (Booleanisation.comp a)ᶜ = Booleanisation.lift a

inductive Booleanisation.LE {α : Type u_1} [GeneralizedBooleanAlgebra α] : Booleanisation α → Booleanisation α → Prop

The order on Booleanisation α is as follows: For a b : α,

• a ≤ b iff a ≤ b in α
• a ≤ bᶜ iff a and b are disjoint in α
• aᶜ ≤ bᶜ iff b ≤ a in α
• ¬ aᶜ ≤ b

• lift: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, a ≤ b → (Booleanisation.lift a).LE (Booleanisation.lift b)
• comp: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, a ≤ b → (Booleanisation.comp b).LE (Booleanisation.comp a)
• sep: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Disjoint a b → (Booleanisation.lift a).LE (Booleanisation.comp b)

inductive Booleanisation.LT {α : Type u_1} [GeneralizedBooleanAlgebra α] : Booleanisation α → Booleanisation α → Prop

The order on Booleanisation α is as follows: For a b : α,

• a < b iff a < b in α
• a < bᶜ iff a and b are disjoint in α
• aᶜ < bᶜ iff b < a in α
• ¬ aᶜ < b

• lift: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, a < b → (Booleanisation.lift a).LT (Booleanisation.lift b)
• comp: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, a < b → (Booleanisation.comp b).LT (Booleanisation.comp a)
• sep: ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Disjoint a b → (Booleanisation.lift a).LT (Booleanisation.comp b)

instance Booleanisation.instLE {α : Type u_1} [GeneralizedBooleanAlgebra α] : LE (Booleanisation α)

The order on Booleanisation α is as follows: For a b : α,

• a ≤ b iff a ≤ b in α
• a ≤ bᶜ iff a and b are disjoint in α
• aᶜ ≤ bᶜ iff b ≤ a in α
• ¬ aᶜ ≤ b

Equations

• Booleanisation.instLE = { le := Booleanisation.LE }

instance Booleanisation.instLT {α : Type u_1} [GeneralizedBooleanAlgebra α] : LT (Booleanisation α)

The order on Booleanisation α is as follows: For a b : α,

• a < b iff a < b in α
• a < bᶜ iff a and b are disjoint in α
• aᶜ < bᶜ iff b < a in α
• ¬ aᶜ < b

Equations

• Booleanisation.instLT = { lt := Booleanisation.LT }

instance Booleanisation.instSup {α : Type u_1} [GeneralizedBooleanAlgebra α] : Sup (Booleanisation α)

The supremum on Booleanisation α is as follows: For a b : α,

• a ⊔ b is a ⊔ b
• a ⊔ bᶜ is (b \ a)ᶜ
• aᶜ ⊔ b is (a \ b)ᶜ
• aᶜ ⊔ bᶜ is (a ⊓ b)ᶜ

Equations

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

instance Booleanisation.instInf {α : Type u_1} [GeneralizedBooleanAlgebra α] : Inf (Booleanisation α)

The infimum on Booleanisation α is as follows: For a b : α,

• a ⊓ b is a ⊓ b
• a ⊓ bᶜ is a \ b
• aᶜ ⊓ b is b \ a
• aᶜ ⊓ bᶜ is (a ⊔ b)ᶜ

Equations

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

instance Booleanisation.instBot {α : Type u_1} [GeneralizedBooleanAlgebra α] : Bot (Booleanisation α)

The bottom element of Booleanisation α is the bottom element of α.

Equations

• Booleanisation.instBot = { bot := Booleanisation.lift ⊥ }

instance Booleanisation.instTop {α : Type u_1} [GeneralizedBooleanAlgebra α] : Top (Booleanisation α)

The top element of Booleanisation α is the complement of the bottom element of α.

Equations

• Booleanisation.instTop = { top := Booleanisation.comp ⊥ }

instance Booleanisation.instSDiff {α : Type u_1} [GeneralizedBooleanAlgebra α] : SDiff (Booleanisation α)

The difference operator on Booleanisation α is as follows: For a b : α,

• a \ b is a \ b
• a \ bᶜ is a ⊓ b
• aᶜ \ b is (a ⊔ b)ᶜ
• aᶜ \ bᶜ is b \ a

Equations

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

@[simp]

theorem Booleanisation.lift_le_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.lift a ≤ Booleanisation.lift b ↔ a ≤ b

@[simp]

theorem Booleanisation.comp_le_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.comp a ≤ Booleanisation.comp b ↔ b ≤ a

@[simp]

theorem Booleanisation.lift_le_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.lift a ≤ Booleanisation.comp b ↔ Disjoint a b

@[simp]

theorem Booleanisation.not_comp_le_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : ¬Booleanisation.comp a ≤ Booleanisation.lift b

@[simp]

theorem Booleanisation.lift_lt_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.lift a < Booleanisation.lift b ↔ a < b

@[simp]

theorem Booleanisation.comp_lt_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.comp a < Booleanisation.comp b ↔ b < a

@[simp]

theorem Booleanisation.lift_lt_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : Booleanisation.lift a < Booleanisation.comp b ↔ Disjoint a b

@[simp]

theorem Booleanisation.not_comp_lt_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : ¬Booleanisation.comp a < Booleanisation.lift b

@[simp]

theorem Booleanisation.lift_sup_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a ⊔ Booleanisation.lift b = Booleanisation.lift (a ⊔ b)

@[simp]

theorem Booleanisation.lift_sup_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a ⊔ Booleanisation.comp b = Booleanisation.comp (b \ a)

@[simp]

theorem Booleanisation.comp_sup_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a ⊔ Booleanisation.lift b = Booleanisation.comp (a \ b)

@[simp]

theorem Booleanisation.comp_sup_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a ⊔ Booleanisation.comp b = Booleanisation.comp (a ⊓ b)

@[simp]

theorem Booleanisation.lift_inf_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a ⊓ Booleanisation.lift b = Booleanisation.lift (a ⊓ b)

@[simp]

theorem Booleanisation.lift_inf_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a ⊓ Booleanisation.comp b = Booleanisation.lift (a \ b)

@[simp]

theorem Booleanisation.comp_inf_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a ⊓ Booleanisation.lift b = Booleanisation.lift (b \ a)

@[simp]

theorem Booleanisation.comp_inf_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a ⊓ Booleanisation.comp b = Booleanisation.comp (a ⊔ b)

@[simp]

theorem Booleanisation.lift_bot {α : Type u_1} [GeneralizedBooleanAlgebra α] : Booleanisation.lift ⊥ = ⊥

@[simp]

theorem Booleanisation.comp_bot {α : Type u_1} [GeneralizedBooleanAlgebra α] : Booleanisation.comp ⊥ = ⊤

@[simp]

theorem Booleanisation.lift_sdiff_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a \ Booleanisation.lift b = Booleanisation.lift (a \ b)

@[simp]

theorem Booleanisation.lift_sdiff_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.lift a \ Booleanisation.comp b = Booleanisation.lift (a ⊓ b)

@[simp]

theorem Booleanisation.comp_sdiff_lift {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a \ Booleanisation.lift b = Booleanisation.comp (a ⊔ b)

@[simp]

theorem Booleanisation.comp_sdiff_comp {α : Type u_1} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Booleanisation.comp a \ Booleanisation.comp b = Booleanisation.lift (b \ a)

instance Booleanisation.instPreorder {α : Type u_1} [GeneralizedBooleanAlgebra α] : Preorder (Booleanisation α)

Equations

• Booleanisation.instPreorder = Preorder.mk ⋯ ⋯ ⋯

instance Booleanisation.instPartialOrder {α : Type u_1} [GeneralizedBooleanAlgebra α] : PartialOrder (Booleanisation α)

Equations

• Booleanisation.instPartialOrder = PartialOrder.mk ⋯

instance Booleanisation.instSemilatticeSup {α : Type u_1} [GeneralizedBooleanAlgebra α] : SemilatticeSup (Booleanisation α)

Equations

• Booleanisation.instSemilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

instance Booleanisation.instSemilatticeInf {α : Type u_1} [GeneralizedBooleanAlgebra α] : SemilatticeInf (Booleanisation α)

Equations

• Booleanisation.instSemilatticeInf = SemilatticeInf.mk ⋯ ⋯ ⋯

instance Booleanisation.instDistribLattice {α : Type u_1} [GeneralizedBooleanAlgebra α] : DistribLattice (Booleanisation α)

Equations

• Booleanisation.instDistribLattice = DistribLattice.mk ⋯

instance Booleanisation.instBoundedOrder {α : Type u_1} [GeneralizedBooleanAlgebra α] : BoundedOrder (Booleanisation α)

Equations

• Booleanisation.instBoundedOrder = BoundedOrder.mk

instance Booleanisation.instBooleanAlgebra {α : Type u_1} [GeneralizedBooleanAlgebra α] : BooleanAlgebra (Booleanisation α)

Equations

• Booleanisation.instBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Booleanisation.liftLatticeHom {α : Type u_1} [GeneralizedBooleanAlgebra α] : LatticeHom α (Booleanisation α)

The embedding from a generalised Boolean algebra to its generated Boolean algebra.

Equations

• Booleanisation.liftLatticeHom = { toFun := Booleanisation.lift, map_sup' := ⋯, map_inf' := ⋯ }

theorem Booleanisation.liftLatticeHom_injective {α : Type u_1} [GeneralizedBooleanAlgebra α] : Function.Injective ⇑Booleanisation.liftLatticeHom