\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{Quantales}
\author{Georg Struth}
\maketitle

\begin{abstract}
  These mathematical components formalise basic properties of
  quantales, together with some important models, constructions, and
  concepts, including quantic nuclei and conuclei.
\end{abstract}

\tableofcontents

\section{Introductory Remarks}

Quantales are complete lattices equipped with an associative
composition that preserves suprema in both arguments.  They have been
used---under various names and in various guises---in mathematics for
almost a century. One important context is the structure of ideals in
rings and $C^\ast$-algebras, another one the foundations of quantum
mechanics, a third one lies in approaches to generalised metric
spaces. In computing, quantales occur naturally in program
semantics---algebras of predicate transformers, for instance, form
quantales, the semantics of linear logic, the foundations of fuzzy
systems and program construction; but also languages or binary
relations form quantales.

These components formalise the basic concepts and properties of
quantales, following by and large Rosenthal's
monograph~\cite{Rosenthal90}.  Because of applications to predicate
transformer semantics, families of quantales are considered in which
certain Sup-preservation laws are absent (nomenclature diverges from
Rosenthal, but is consistent with AFP entries for dioids and Kleene
algebras~\cite{ArmstrongSW13}).  Beyond basic equational reasoning,
some models of quantales are presented, though those that arise from
ring theory or $C^\ast$-algebras are currently not supported.

Nuclei and conuclei of quantales are also investigated, and some
important relationships with quotients and subalgebras of quantales
are formalised, following Rosenthal. In particular, I (re)prove his
representation theorem that every quantale is isomorphic to a nucleus
of a powerset quantale over some semigroup. Beyond that it is shown
how left-sided elements give rise to nuclei and conuclei.

Another subject of study are quantale-modules, which have been
introduced by Abramsky and Vickers~\cite{AbramskyV93} and widely used
since, with some original results on semidirect products over
these~\cite{DongolHS17} and some new results on the Kleene star in
this setting.

Quantales draw heavily on lattice and order theory, Galois connections
and the associated monads and comonads. They are also strongly related
to complete Heyting algebras, frames and locales~\cite{Johnstone82},
for which future AFP entries might be worth creating.  Further
variants, such as Girard quantales, might also be worth exploring.

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
