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. [Vickers1989] and [Mulvey1986]).

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;

• Quantale and AddQuantale : Structures serving as a typeclass alias, so one can write variable? [Quantale α] instead of variable [Semigroup α] [CompleteLattice α] [IsQuantale α], and similarly for the additive variant.

• 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

structure AddQuantale (α : Type u_1) [AddSemigroup α] [CompleteLattice α] [IsAddQuantale α] : Type

A quantale is a semigroup distributing over a complete lattice.

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

structure Quantale (α : Type u_1) [Semigroup α] [CompleteLattice α] [IsQuantale α] : Type

A quantale is a semigroup distributing over a complete lattice.

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 AddQuantale.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

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

def AddQuantale.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

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

def AddQuantale.«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

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

def AddQuantale.«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

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

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

Left- and right-residuation operators on a 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

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

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

Left- and right- residuation operators on a 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

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

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

Left- and right-residuation operators on a 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

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

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

Left- and right- residuation operators on a 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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