Relation algebras

A relation algebra in the sense of Tarski (not to be confused with a relational algebra) is an extension of Boolean algebras that are designed to form an algebraic analysis of relations, α → α → Prop in Lean. They have applications in computer science such as the theory of constraint satisfaction as well as mathematical connections such as combinatorics.

References

• R. Maddux, Relation Algebras

class Cslib.RelationAlgebra (α : Type u_1) extends BooleanAlgebra α, Monoid α, StarMul α : Type u_1

The class of relation algebras. Note the notational differences from the literature. In addition to inheriting Mathlib's notations for Boolean algebras, star is used for converse, and the monoid reduct for composition uses multiplicative notation.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• le_top (a : α) : a ≤ ⊤
• bot_le (a : α) : ⊥ ≤ a
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ
• 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
• star : α → α
• star_involutive : Function.Involutive star
• star_mul (r s : α) : star (r * s) = star s * star r
• sup_mul (a b c : α) : (a ⊔ b) * c = a * c ⊔ b * c
• star_sup (a b : α) : star (a ⊔ b) = star a ⊔ star b
• tarski (a b : α) : star a * (a * b)ᶜ ≤ bᶜ

@[instance_reducible]

def Cslib.RelationAlgebra.ofTarski {α : Type u_1} [Max α] [Compl α] [Mul α] [One α] [Star α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a) (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (huntington : ∀ (a b : α), (aᶜ ⊔ b)ᶜ ⊔ (aᶜ ⊔ bᶜ)ᶜ = a) (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) (mul_one : ∀ (a : α), a * 1 = a) (star_involutive : ∀ (a : α), star (star a) = a) (star_mul : ∀ (a b : α), star (a * b) = star b * star a) (sup_mul : ∀ (a b c : α), (a ⊔ b) * c = a * c ⊔ b * c) (star_sup : ∀ (a b : α), star (a ⊔ b) = star a ⊔ star b) (tarski : ∀ (a b : α), star a * (a * b)ᶜ ⊔ bᶜ = bᶜ) : RelationAlgebra α

A RelationAlgebra can be constructed using Tarski's original ten axioms.

Equations

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

theorem Cslib.RelationAlgebra.star_mono {α : Type u_1} [RelationAlgebra α] : Monotone star

theorem Cslib.RelationAlgebra.mul_sup {α : Type u_1} [RelationAlgebra α] (a b c : α) : a * (b ⊔ c) = a * b ⊔ a * c

theorem Cslib.RelationAlgebra.left_modular {α : Type u_1} [RelationAlgebra α] (a b c : α) : a * b ⊓ c ≤ a * (b ⊓ star a * c)

def Cslib.RelationAlgebra.Integral {α : Type u_1} [RelationAlgebra α] : Prop

A relation algebra is integral when its identity is an atom.

Equations

• Cslib.RelationAlgebra.Integral = IsAtom 1

def Cslib.RelationAlgebra.IdentityAtoms {α : Type u_1} [RelationAlgebra α] : Set α

The set of identity atoms.

Equations

• Cslib.RelationAlgebra.IdentityAtoms = {a : α | IsAtom a ∧ a ≤ 1}

def Cslib.RelationAlgebra.SymmetricDiversityAtoms {α : Type u_1} [RelationAlgebra α] : Set α

The set of symmetric diversity atoms, those below the complement of identity.

Equations

• Cslib.RelationAlgebra.SymmetricDiversityAtoms = {a : α | IsAtom a ∧ a ≤ 1ᶜ ∧ star a = a}

def Cslib.RelationAlgebra.NonsymmetricDiversityAtoms {α : Type u_1} [RelationAlgebra α] : Set α

The set of nonsymmetric diversity atoms. The diversity condition follows from le_compl_one_of_mem_nonsymmetricDiversityAtoms.

Equations

• Cslib.RelationAlgebra.NonsymmetricDiversityAtoms = {a : α | IsAtom a ∧ star a ≠ a}

theorem Cslib.RelationAlgebra.le_compl_one_of_mem_nonsymmetricDiversityAtoms {α : Type u_1} [RelationAlgebra α] {a : α} (h : a ∈ NonsymmetricDiversityAtoms) : a ≤ 1ᶜ

Every nonsymmetric atom lies below the complement of identity.