Quantale

Stream: maths

[Pieter Cuijpers]

Quantales are a non-commutative generalization of frames (an order-theoretic view on topology). I.e. a quantale is an ordered semigroup distributing over a complete (sup)lattice. A frame is then an integral quantale with a commutative and idempotent monoid as semigroup.

I've personally started to study quantales out of an interest in their application in theoretical computer science, but as they have a broad applicability in physics and math as well (the word quantale already shows up in some discussions on Zulip), I figured adding the definition to Mathlib also makes sense. I'm working now on the branch PieterCuijpers_Quantales of Mathlib to get my first PR.

Here, I would like to start a discussion and invite anyone who is interested in quantales to contribute. Have a look at the initial definitions if you like and comment whether you think they are going in the right direction. Also, let's discuss which definitions and theorems would be interesting/necessary to have as part of the library.

[Eric Wieser]

(branch#PieterCuijpers_Quantales / #17289)

[Pieter Cuijpers]

The first PR, giving the definition of Quantale in the form of an IsQuantale mixin, has now been merged :-)
Thanks to Yaël and Jireh for their patient reviewing.
Comments and suggestions for further PRs are very welcome.
On my current list are:

• a variable_alias Quantale
• definitions of homomorphism and lax/oplax homomorphism
• theorem that frames are commutative quantales, and a quantale is a frame iff it is an idempotent and integral monoid.

[Bas Spitters]

It's great to see more interest in quantales/locales in Lean. Are you also planning to make the connection to C*-algebras?

[Pieter Cuijpers]

To be honest, I'm doing the formalization partly also simply to learn more about Quantales and have a fun project that encourages me to do so. In that sense, yes it may make sense to make the connection, since quite a few papers seem to mention the connection to C-algebras. Frankly, I don't know yet what C-algebras are ;-)

I'm mainly a theoretical computer-scientists, interested in quantales as a model of observation of dynamic behavior (I have a background in process algebra - so the work of Abramsky, Vickers, and Resende is high on my list). If it is relevant for that, then sure I'll probably try myself at somepoint, but also if not, I would like to see other directions. At the moment, I'm in the "gathering ideas" phase, so thanks a lot for suggesting this!

[Bas Spitters]

(Sorry for the late reply, apparently this wasn't posted due to network problems...)

@Pieter Cuijpers Quantales where introduced to generalize Gelfand duality between commutative C-algebras and Compact Hausdorff spaces to the non-commutative C-algebras.
A first observation, is that Gelfand duality factors via a duality with Compact regular locales. Quantales can then be seen as non-commutative locales.
https://www.maths.sussex.ac.uk/Staff/CJM/research/pdf/&.pdf
https://ncatlab.org/nlab/show/quantale

[Pieter Cuijpers]

That makes sense, and I can relate some of it to what I know from theoretical computer science. Formalizing this as one of the first things within the Mathlib library seems like a good idea to me. Not sure when/if I'll get to it myself on short notice though, since teaching load will increase the coming months.