feat: quantales

Mathlib.lean

@@ -272,6 +272,7 @@ import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.Group.Invertible.Basic
 import Mathlib.Algebra.Group.Invertible.Defs
+import Mathlib.Algebra.Group.IsIdem
 import Mathlib.Algebra.Group.MinimalAxioms
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.Group.NatPowAssoc
@@ -692,6 +693,7 @@ import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Algebra.Order.Positive.Field
 import Mathlib.Algebra.Order.Positive.Ring
+import Mathlib.Algebra.Order.Quantale
 import Mathlib.Algebra.Order.Rearrangement
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Order.Ring.Basic

Mathlib/Algebra/Group/IsIdem.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2024 Pieter Cuijpers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Pieter Cuijpers
+-/
+import Mathlib.Algebra.Group.Defs
+
+/-!
+# Mixing for Idempotent Semigroups
+
+An idempotent semigroup is a semigroup that satisfies `x * x = x`.
+
+## Main definitions
+
+* `IsIdemSemigroup`: Typeclass mixin for a semigroup respecting `x * x = x`.
+* `IsAddIdemSemigroup`: Typeclass mixin for a semigroup respecting `x + x = x`.
+-/
+
+/-- An idempotent additive semigroup is a type with an associative idempotent addition. -/
+class IsIdemAddSemigroup (G : Type _) [AddSemigroup G] : Prop where
+  /-- Idempotence: `x + x = x` -/
+  protected add_idem (x : G) : x + x = x
+
+/-- An idempotent semigroup is a type with an associative idempotent `(*)`. -/
+@[to_additive]
+class IsIdemSemigroup (G : Type _) [Semigroup G] : Prop where
+  /-- Idempotence: `x * x = x` -/
+  protected mul_idem (x : G) : x * x = x
+
+section IsIdem
+
+variable (G : Type _)
+variable [Semigroup G] [IsIdemSemigroup G]
+
+@[to_additive]
+theorem mul_idem (x : G) : x * x = x := IsIdemSemigroup.mul_idem _
+
+end IsIdem

Mathlib/Algebra/Order/Kleene.lean

@@ -3,12 +3,14 @@ Copyright (c) 2022 Siddhartha Prasad, Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Prasad, Yaël Dillies
 -/
+import Mathlib.Algebra.Group.IsIdem
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Ring.InjSurj
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.Algebra.Ring.Prod
 import Mathlib.Tactic.Monotonicity.Attr
 
+
 /-!
 # Kleene Algebras
 
@@ -58,6 +60,7 @@ variable {α β ι : Type*} {π : ι → Type*}
 /-- An idempotent semiring is a semiring with the additional property that addition is idempotent.
 -/
 class IdemSemiring (α : Type u) extends Semiring α, SemilatticeSup α where
+  protected le a b := a + b = b
   protected sup := (· + ·)
   protected add_eq_sup : ∀ a b : α, a + b = a ⊔ b := by
     intros
@@ -131,7 +134,8 @@ theorem add_eq_sup (a b : α) : a + b = a ⊔ b :=
 --               So, this theorem should be scoped.
 scoped[Computability] attribute [simp] add_eq_sup
 
-theorem add_idem (a : α) : a + a = a := by simp
+/-- As explained in the definition, an idempotent semiring has an idempotent addition -/
+instance : IsIdemAddSemigroup α where add_idem := by simp
 
 theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a
   | 0, h => (h rfl).elim

Mathlib/Algebra/Order/Quantale.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2024 Pieter Cuijpers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Pieter Cuijpers
+-/
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Order.CompleteLattice
+
+/-!
+# 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-semlattice 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 definitions set out on the wikipedia page on quantales,
+which also distinguish unital, commutative, idempotent, integral and involutive quantales.
+A unital quantale is simply a quantale over a monoid, a commutative quantale is a quantale
+over a commutative semigroup, and an idempotent quantale is a quantale over an idempotent
+semigroup. As we define quantales relative to their semigroup, these do not need to be defined
+explicitly here. An integral (or strictly two-sided) quantale is a unital quantale in which
+the top element of the lattice and the unit of the semigroup coincide. We give a mix-in class
+definition for this.
+
+The involutive quantale (which is necessary to discuss regularity properties) we do not cover
+in this file. Also the proof that every frame is a commutative quantale, and that a quantale is
+a frame if and only if it is integral and idempotent are developed separately in order to reduce
+overhead if a user does not need them.
+
+## Main definitions
+
+* class `Quantale`: a semigroup distributing over a complete lattice, i.e satisfying
+  `x * (sSup s) = ⨆ y ∈ s, x * y` and `(sSup s) * y = ⨆ x ∈ s, x * y`;
+
+* `IsIntegralQuantale`: Typeclass mixin for a unital quantale (i.e. a quantale in which the
+  semigroup is a monoid) respecting `⊤ = 1` (also called a two-sided quantale);
+
+* next to these classes, we define the additive versions `AddQuantale`, `IsAddIntegral` in
+  which the semigroup operation is denoted by addition instead of multiplication;
+
+## Naming conventions
+
+## Notation
+
+* `x ⇨ₗ y` : `sSup { z | z * x ≤ y }`, the leftResiduation of `y` over `x`;
+
+* `x ⇨ᵣ y` : `sSup { z | x * z ≤ y }`, the rightResiduation of `y` over `x`;
+
+## References
+
+<https://en.wikipedia.org/wiki/Quantale>
+<https://encyclopediaofmath.org/wiki/Quantale>
+<https://ncatlab.org/nlab/show/quantale>
+
+-/
+
+/-- An additive quantale is an additive semigroup distributing over a complete lattice. -/
+class AddQuantale (α : Type _) [AddSemigroup α] extends CompleteLattice α where
+  /-- Addition is distributive over join in a quantale -/
+  protected add_sSup_eq_iSup_add (x : α) (s : Set α) : x + sSup s = ⨆ y ∈ s, x + y
+  /-- Addition is distributive over join in a quantale -/
+  protected sSup_add_eq_iSup_add (s : Set α) (y : α) : sSup s + y = ⨆ x ∈ s, x + y
+
+/-- A quantale is a semigroup distributing over a complete lattice. -/
+@[to_additive]
+class Quantale (α : Type _) [Semigroup α] extends CompleteLattice α where
+  /-- Multiplication is distributive over join in a quantale -/
+  protected mul_sSup_eq_iSup_mul (x : α) (s : Set α) : x * sSup s = ⨆ y ∈ s, x * y
+  /-- Multiplication is distributive over join in a quantale -/
+  protected sSup_mul_eq_iSup_mul (s : Set α) (y : α) : sSup s * y = ⨆ x ∈ s, x * y
+
+/-- An integral (or strictly two-sided) additive quantale is a quantale over an additive monoid
+    where top and unit coincide. -/
+class IsIntegralAddQuantale (α : Type _) [AddMonoid α] [AddQuantale α] : Prop where
+  /-- Top and unit coincide in an integral (or strictly two-sided) quantale -/
+  protected top_eq_zero : (⊤ : α) = 0
+
+/-- An integral (or strictly two-sided) quantale is a quantale over a monoid where
+    top and unit coincide. -/
+@[to_additive]
+class IsIntegralQuantale (α : Type _) [Monoid α] [Quantale α] : Prop where
+  /-- Top and unit coincide in an integral (or strictly two-sided) quantale -/
+  protected top_eq_one : (⊤ : α) = 1
+
+section Quantale
+
+variable (α : Type _)
+variable [Semigroup α] [Quantale α]
+
+@[to_additive]
+theorem mul_sSup_eq_iSup_mul : ∀ x : α, ∀ s : Set α, x * sSup s = ⨆ y ∈ s, x * y :=
+  Quantale.mul_sSup_eq_iSup_mul
+
+@[to_additive]
+theorem sSup_mul_eq_iSup_mul : ∀ s : Set α, ∀ y : α, sSup s * y = ⨆ x ∈ s, x * y :=
+  Quantale.sSup_mul_eq_iSup_mul
+
+end Quantale
+
+section IsIntegral
+open Quantale
+
+variable (α : Type _)
+variable [Monoid α] [Quantale α] [IsIntegralQuantale α]
+
+@[to_additive]
+theorem top_eq_one : (⊤ : α) = 1 := IsIntegralQuantale.top_eq_one
+
+end IsIntegral
+
+namespace Quantale
+
+variable {α : Type _}
+variable [Semigroup α] [Quantale α]
+
+/-- 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 = sSup { z | z * x ≤ y }`.
+-/
+@[to_additive "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 = sSup { z | z + x ≤ y }`.
+"]
+def leftResiduation (x y : α) := sSup { z | z * 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 = sSup { z | x * z ≤ y }`.
+-/
+@[to_additive "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 = sSup { z | x + z ≤ y }`.
+"]
+def rightResiduation (x y : α) := sSup { z | x * z ≤ y }
+
+@[inherit_doc]
+scoped infixr:60 " ⇨ₗ " => leftResiduation
+
+@[inherit_doc]
+scoped infixr:60 " ⇨ᵣ " => rightResiduation
+
+end Quantale
+
+namespace AddQuantale
+
+@[inherit_doc]
+scoped infixr:60 " ⇨ₗ " => leftResiduation
+
+@[inherit_doc]
+scoped infixr:60 " ⇨ᵣ " => rightResiduation
+
+end AddQuantale

Mathlib/Tactic/ToAdditive/Frontend.lean

@@ -966,6 +966,7 @@ def nameDict : String → List String
   | "powers"      => ["multiples"]
   | "multipliable"=> ["summable"]
   | "gpfree"      => ["apfree"]
+  | "quantale"    => ["add", "Quantale"]
   | x             => [x]
 
 /--

docs/references.bib

@@ -2701,6 +2701,22 @@ @Article{         MR577178
   url           = {https://doi.org/10.1007/BF00417500}
 }
 
+@Article{         Mulvey1986,
+  author        = {Mulvey, Christopher J.},
+  title         = {\&},
+  fjournal      = {Supplemento ai Rendiconti del Circolo Matem{\`a}tico di
+                  Palermo. Serie II},
+  journal       = {Suppl. Rend. Circ. Mat. Palermo (2)},
+  issn          = {1592-9531},
+  volume        = {12},
+  pages         = {99--104},
+  year          = {1986},
+  language      = {English},
+  keywords      = {46L60,46L05,81Q10},
+  zbmath        = {4030272},
+  zbl           = {0633.46065}
+}
+
 @Unpublished{     Naor-2015,
   author        = {Assaf Naor},
   title         = {Metric Embeddings and Lipschitz Extensions},
@@ -3301,6 +3317,15 @@ @Book{            verdier1996
   mrnumber      = {1453167}
 }
 
+@Book{            Vickers1989,
+  author        = {Vickers, Steven},
+  title         = {Topology via Logic},
+  isbn          = {0-521-57651-2},
+  year          = {1989},
+  publisher     = {University of Cambridge},
+  language      = {English}
+}
+
 @Misc{            vistoli2004,
   author        = {Vistoli, Angelo},
   title         = {Notes on {Grothendieck} topologies, fibered categories and