Theory of quantales

Quantales are the non-commutative generalization of locales/frames and as such are linked to point-free topology and order theory. Applications are found throughout logic, quantum mechanics, and computer science (see e.g. [Vic89] and [Mul86]).

The most general definition of quantale occurring in literature, is that a quantale is a semigroup distributing over a complete sup-semilattice. In our definition below, we use the fact that every complete sup-semilattice is in fact a complete lattice, and make constructs defined for those immediately available. Another view could be to define a quantale as a complete idempotent semiring, i.e. a complete semiring in which + and sup coincide. However, we will often encounter additive quantales, i.e. quantales in which the semigroup operator is thought of as addition, in which case the link with semirings will lead to confusion notationally.

In this file, we follow the basic definition set out on the wikipedia page on quantales, using a mixin typeclass to make the special cases of unital, commutative, idempotent, integral, and involutive quantales easier to add on later.

Main definitions

• IsQuantale and IsAddQuantale : Typeclass mixin for a (additive) semigroup distributing over a complete lattice, i.e satisfying x * (sSup s) = ⨆ y ∈ s, x * y and (sSup s) * y = ⨆ x ∈ s, x * y;

• leftMulResiduation, rightMulResiduation, leftAddResiduation, rightAddResiduation : Defining the left- and right- residuations of the semigroup (see notation below).

• Finally, we provide basic distributivity laws for sSup into iSup and sup, monotonicity of the semigroup operator, and basic equivalences for left- and right-residuation.

Notation

• x ⇨ₗ y : sSup {z | z * x ≤ y}, the leftMulResiduation of y over x;

• x ⇨ᵣ y : sSup {z | x * z ≤ y}, the rightMulResiduation of y over x;

References

https://en.wikipedia.org/wiki/Quantale https://encyclopediaofmath.org/wiki/Quantale https://ncatlab.org/nlab/show/quantale

class IsAddQuantale (α : Type u_1) [AddSemigroup α] [CompleteLattice α] : Prop

An additive quantale is an additive semigroup distributing over a complete lattice.

• add_sSup_distrib (x : α) (s : Set α) : x + sSup s = ⨆ y ∈ s, x + y

  Addition is distributive over join in a quantale

• sSup_add_distrib (s : Set α) (y : α) : sSup s + y = ⨆ x ∈ s, x + y

  Addition is distributive over join in a quantale

class IsQuantale (α : Type u_1) [Semigroup α] [CompleteLattice α] : Prop

A quantale is a semigroup distributing over a complete lattice.

• mul_sSup_distrib (x : α) (s : Set α) : x * sSup s = ⨆ y ∈ s, x * y

  Multiplication is distributive over join in a quantale

• sSup_mul_distrib (s : Set α) (y : α) : sSup s * y = ⨆ x ∈ s, x * y

  Multiplication is distributive over join in a quantale

theorem mul_sSup_distrib {α : Type u_1} {x : α} {s : Set α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : x * sSup s = ⨆ y ∈ s, x * y

theorem add_sSup_distrib {α : Type u_1} {x : α} {s : Set α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x + sSup s = ⨆ y ∈ s, x + y

theorem sSup_mul_distrib {α : Type u_1} {x : α} {s : Set α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : sSup s * x = ⨆ y ∈ s, y * x

theorem sSup_add_distrib {α : Type u_1} {x : α} {s : Set α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : sSup s + x = ⨆ y ∈ s, y + x

def IsAddQuantale.leftAddResiduation {α : Type u_1} [AddSemigroup α] [CompleteLattice α] (x y : α) : α

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ₗ z ↔ x + y ≤ z or alternatively x ⇨ₗ y = sSup { z | z + x ≤ y }.

Equations

• IsAddQuantale.leftAddResiduation x y = sSup {z : α | z + x ≤ y}

def IsAddQuantale.rightAddResiduation {α : Type u_1} [AddSemigroup α] [CompleteLattice α] (x y : α) : α

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ᵣ z ↔ y + x ≤ z or alternatively x ⇨ₗ y = sSup { z | x + z ≤ y }."

Equations

• IsAddQuantale.rightAddResiduation x y = sSup {z : α | x + z ≤ y}

def IsAddQuantale.«term_⇨ₗ_» : Lean.TrailingParserDescr

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ₗ z ↔ x + y ≤ z or alternatively x ⇨ₗ y = sSup { z | z + x ≤ y }.

Equations

• IsAddQuantale.«term_⇨ₗ_» = Lean.ParserDescr.trailingNode `IsAddQuantale.«term_⇨ₗ_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ₗ ") (Lean.ParserDescr.cat `term 60))

def IsAddQuantale.«term_⇨ᵣ_» : Lean.TrailingParserDescr

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ᵣ z ↔ y + x ≤ z or alternatively x ⇨ₗ y = sSup { z | x + z ≤ y }."

Equations

• IsAddQuantale.«term_⇨ᵣ_» = Lean.ParserDescr.trailingNode `IsAddQuantale.«term_⇨ᵣ_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ᵣ ") (Lean.ParserDescr.cat `term 60))

def IsQuantale.leftMulResiduation {α : Type u_1} [Semigroup α] [CompleteLattice α] (x y : α) : α

Left- and right-residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ₗ z ↔ x * y ≤ z or alternatively x ⇨ₗ y = sSup { z | z * x ≤ y }.

Equations

• IsQuantale.leftMulResiduation x y = sSup {z : α | z * x ≤ y}

def IsQuantale.rightMulResiduation {α : Type u_1} [Semigroup α] [CompleteLattice α] (x y : α) : α

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ᵣ z ↔ y * x ≤ z or alternatively x ⇨ₗ y = sSup { z | x * z ≤ y }.

Equations

• IsQuantale.rightMulResiduation x y = sSup {z : α | x * z ≤ y}

def IsQuantale.«term_⇨ₗ_» : Lean.TrailingParserDescr

Left- and right-residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ₗ z ↔ x * y ≤ z or alternatively x ⇨ₗ y = sSup { z | z * x ≤ y }.

Equations

• IsQuantale.«term_⇨ₗ_» = Lean.ParserDescr.trailingNode `IsQuantale.«term_⇨ₗ_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ₗ ") (Lean.ParserDescr.cat `term 60))

def IsQuantale.«term_⇨ᵣ_» : Lean.TrailingParserDescr

Left- and right- residuation operators on an additive quantale are similar to the Heyting operator on complete lattices, but for a non-commutative logic. I.e. x ≤ y ⇨ᵣ z ↔ y * x ≤ z or alternatively x ⇨ₗ y = sSup { z | x * z ≤ y }.

Equations

• IsQuantale.«term_⇨ᵣ_» = Lean.ParserDescr.trailingNode `IsQuantale.«term_⇨ᵣ_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ᵣ ") (Lean.ParserDescr.cat `term 60))

theorem IsQuantale.mul_iSup_distrib {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : x * ⨆ (i : ι), f i = ⨆ (i : ι), x * f i

theorem IsAddQuantale.add_iSup_distrib {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x + ⨆ (i : ι), f i = ⨆ (i : ι), x + f i

theorem IsQuantale.iSup_mul_distrib {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : (⨆ (i : ι), f i) * x = ⨆ (i : ι), f i * x

theorem IsAddQuantale.iSup_add_distrib {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : (⨆ (i : ι), f i) + x = ⨆ (i : ι), f i + x

theorem IsQuantale.mul_sup_distrib {α : Type u_1} {x y z : α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : x * (y ⊔ z) = x * y ⊔ x * z

theorem IsAddQuantale.add_sup_distrib {α : Type u_1} {x y z : α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x + y ⊔ z = (x + y) ⊔ (x + z)

theorem IsQuantale.sup_mul_distrib {α : Type u_1} {x y z : α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : (x ⊔ y) * z = x * z ⊔ y * z

theorem IsAddQuantale.sup_add_distrib {α : Type u_1} {x y z : α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x ⊔ y + z = (x + z) ⊔ (y + z)

instance IsQuantale.instMulLeftMono {α : Type u_1} [Semigroup α] [CompleteLattice α] [IsQuantale α] : MulLeftMono α

instance IsAddQuantale.instAddLeftMono {α : Type u_1} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : AddLeftMono α

instance IsQuantale.instMulRightMono {α : Type u_1} [Semigroup α] [CompleteLattice α] [IsQuantale α] : MulRightMono α

instance IsAddQuantale.instAddRightMono {α : Type u_1} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : AddRightMono α

theorem IsQuantale.leftMulResiduation_le_iff_mul_le {α : Type u_1} {x y z : α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : x ≤ IsQuantale.leftMulResiduation y z ↔ x * y ≤ z

theorem IsAddQuantale.leftAddResiduation_le_iff_add_le {α : Type u_1} {x y z : α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x ≤ IsAddQuantale.leftAddResiduation y z ↔ x + y ≤ z

theorem IsQuantale.rightMulResiduation_le_iff_mul_le {α : Type u_1} {x y z : α} [Semigroup α] [CompleteLattice α] [IsQuantale α] : x ≤ IsQuantale.rightMulResiduation y z ↔ y * x ≤ z

theorem IsAddQuantale.rightAddResiduation_le_iff_add_le {α : Type u_1} {x y z : α} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : x ≤ IsAddQuantale.rightAddResiduation y z ↔ y + x ≤ z

@[simp]

theorem IsQuantale.bot_mul {α : Type u_3} [Semigroup α] [CompleteLattice α] [IsQuantale α] {x : α} : ⊥ * x = ⊥

@[simp]

theorem IsAddQuantale.bot_add {α : Type u_3} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] {x : α} : ⊥ + x = ⊥

@[simp]

theorem IsQuantale.mul_bot {α : Type u_3} [Semigroup α] [CompleteLattice α] [IsQuantale α] {x : α} : x * ⊥ = ⊥

@[simp]

theorem IsAddQuantale.add_bot {α : Type u_3} [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] {x : α} : x + ⊥ = ⊥