David Corfield sandbox

$\newcommand{\Q}{\mathcal{Q}}$ $\newcommand{\Sup}{\mathbf{Sup}}$ $\newcommand{\Rel}{\mathbf{Rel}}$

A quantaloid is a many-object version of a quantale?.

Equivalently, it is a category enriched over? the category $\Sup$ of sup-lattice?s and supremum-preserving maps. Thus a quantaloid is an ordinary category in which, for each pair of objects $A,B$, the collection of arrows $A \to B$ is not merely a set but a complete join-semilattice, and composition preserves arbitrary joins in each variable.

The basic example to keep in mind is the category $\Rel$ of sets and relations. For sets $X,Y$, the arrows $X \to Y$ are relations $R \subseteq X \times Y$, ordered by inclusion. Arbitrary joins are unions of relations, and relational composition distributes over unions.

Hence a quantaloid may be thought of as a category of generalized relations, generalized predicates, generalized transitions, or typed truth values, closed under arbitrary disjunctions.

h1. Idea

A quantale? is a complete lattice equipped with a multiplication distributing over arbitrary joins. A quantaloid is the corresponding many-object structure: instead of a single complete lattice of elements, there is a complete lattice $\Q(A,B)$ of arrows from $A$ to $B$ for every ordered pair of objects $A,B$.

Thus:

• a one-object quantaloid is the same thing as a unital quantale;
• a quantaloid is a category whose homs have arbitrary joins;
• composition in a quantaloid is compatible with arbitrary joins.

The slogan is:

a quantaloid is a quantale with many objects.

But the most useful intuition is often:

a quantaloid is a typed calculus of generalized relations.

For example, if $R_i : X \to Y$ is a family of relations, their join is the union

$$\bigvee_i R_i = \bigcup_i R_i ,$$

and for any relation $S : Y \to Z$ one has

$$S \circ \left(\bigvee_i R_i\right) = \bigvee_i (S \circ R_i).$$

A quantaloid axiomatizes exactly this kind of behaviour.

h1. Definition

There are several equivalent definitions.

h2. Enriched definition

A quantaloid is a category enriched in $\Sup$, the symmetric monoidal closed category of sup-lattices and supremum-preserving maps.

Thus, for every pair of objects $A,B$, there is a sup-lattice

$$\Q(A,B),$$

and for every triple $A,B,C$ there is a supremum-preserving composition map

$$\Q(B,C) \times \Q(A,B) \longrightarrow \Q(A,C), \qquad (g,f) \mapsto g \circ f ,$$

which is associative and unital.

More explicitly, composition preserves arbitrary joins in each variable:

$$g \circ \bigvee_i f_i = \bigvee_i (g \circ f_i),$$

and

$$\left(\bigvee_j g_j\right) \circ f = \bigvee_j (g_j \circ f).$$

h2. Elementary definition

Equivalently, a quantaloid consists of:

• a class of objects;
• for each pair of objects $A,B$, a complete join-semilattice $\Q(A,B)$ of arrows $A \to B$;
• for each object $A$, an identity arrow $1_A \in \Q(A,A)$;
• for each triple $A,B,C$, an associative composition operation
  $$\Q(B,C) \times \Q(A,B) \to \Q(A,C)$$

  preserving arbitrary joins in each variable.

The order on $\Q(A,B)$ is usually written

$$f \leq g .$$

This may be read as saying that $f$ is a subarrow, approximation, refinement, or implication-below $g$, depending on the intended example.

h2. 2-categorical definition

Equivalently, a quantaloid is a locally posetal 2-category? such that:

• each hom-poset is cocomplete;
• horizontal composition preserves all joins separately in each variable.

Since a join-preserving map between complete lattices has a right adjoint, composition in a quantaloid has right residuals. Thus for arrows

$$f : A \to B, \qquad g : B \to C, \qquad h : A \to C,$$

one may define arrows

$$h / f : B \to C, \qquad g \backslash h : A \to B$$

by the adjunction conditions

$$g \circ f \leq h \quad\Longleftrightarrow\quad g \leq h/f \quad\Longleftrightarrow\quad f \leq g\backslash h .$$

This is the sense in which a quantaloid is a closed locally ordered 2-category.

h1. Examples

h2. Quantales

Every unital quantale? $Q$ is a one-object quantaloid. The unique hom-object is $Q$ itself, and composition is the quantale multiplication.

Conversely, every one-object quantaloid is a unital quantale.

h2. Relations

The category $\Rel$ of sets and relations is a quantaloid.

For sets $X,Y$, let

$$\Rel(X,Y) = \mathcal{P}(X \times Y),$$

ordered by inclusion. Joins are unions, and composition is ordinary relational composition:

$$S \circ R = \{(x,z) \mid \exists y,\; xRy \text{ and } ySz\}.$$

Composition distributes over arbitrary unions, so $\Rel$ is a quantaloid.

This example is often the best guide to the general theory.

h2. Sup-lattices

The category $\Sup$ of sup-lattices and sup-preserving maps is a quantaloid.

For sup-lattices $L,M$, the hom-set $\Sup(L,M)$ is ordered pointwise:

$$f \leq g \quad\Longleftrightarrow\quad \forall x \in L,\; f(x) \leq g(x).$$

Pointwise joins of sup-preserving maps are again sup-preserving, and composition preserves these joins.

h2. Quantale-valued relations

Let $Q$ be a unital quantale. There is a quantaloid $Q\text{-}\Rel$ whose objects are sets and whose arrows $X \to Y$ are $Q$-valued relations, that is, functions

$$R : X \times Y \to Q .$$

The order and joins are computed pointwise. Composition is given by

$$(S \circ R)(x,z) = \bigvee_{y \in Y} S(y,z) \otimes R(x,y).$$

For $Q = 2$, this recovers the ordinary quantaloid $\Rel$.

h2. Distributors

For a suitable base of enrichment $V$, the V-distributor?s between $V$-categories form a quantaloid. In particular, the bicategory of enriched profunctors often becomes locally ordered, with joins computed pointwise.

This example explains why quantaloids occur naturally in enriched category theory: they provide bases over which one can do enriched category theory with many types of truth values or distances.

h1. Involutive quantaloids

A -quantaloid, or involutive quantaloid, is a quantaloid $\Q$ equipped with an involution

$$(-)^* : \Q^{op} \to \Q$$

which is the identity on objects, reverses arrows, preserves the local order, and satisfies

$$(g \circ f)^* = f^* \circ g^*, \qquad (f^*)^* = f .$$

The guiding example is again $\Rel$, where the involution sends a relation to its converse:

$$R^* = \{(y,x) \mid (x,y) \in R\}.$$

Thus a -quantaloid is a quantaloid equipped with an abstract operation of taking converse, adjoint, or reversal of generalized relations.

h1. Categories enriched in a quantaloid

Let $\Q$ be a quantaloid. A category enriched in $\Q$ is like an enriched category whose objects may have different extents or types.

One common presentation is as follows. A $\Q$-category $X$ consists of:

• a set $X_0$ of objects;
• a function assigning to each $x \in X_0$ an object
  $$|x| \in \Q$$

  called its extent or type;

• for each pair $x,y \in X_0$, an arrow
  $$X(x,y) : |x| \to |y|$$

  in $\Q$;

such that

$$1_{|x|} \leq X(x,x)$$

and

$$X(y,z) \circ X(x,y) \leq X(x,z).$$

Thus a $\Q$-category is a category whose hom-values are arrows of the quantaloid $\Q$, and where the source and target types of these hom-values are controlled by the extents of the objects.

When $\Q$ has one object, this reduces to enrichment over a quantale.

h1. Motivation

Quantaloids are useful when one wants to combine:

• categorical composition;
• order-enrichment;
• arbitrary joins, interpreted as disjunctions, unions, or nondeterministic choices;
• residuals, interpreted as implication-like operations;
• many object-types.

They therefore appear in the study of:

• enriched categories;
• generalized metric spaces;
• fuzzy sets and fuzzy relations;
• distributors and profunctors;
• ordered and relational structures;
• categorical logic;
• automata and transition systems;
• quantale-valued sheaves and modules.

h1. Related concepts

• quantale?
• sup-lattice?
• enriched category?
• locally posetal 2-category?
• relation?
• allegory?
• profunctor?
• distributor?
• V-category?
• module over a quantale?

h1. References

• K. I. Rosenthal, The Theory of Quantaloids, Longman Scientific and Technical, 1996.

• R. F. C. Walters, Sheaves and Cauchy-complete categories.

• R. Betti, A. Carboni, R. Street and R. Walters, Variation through enrichment.

• I. Stubbe, Categorical structures enriched in a quantaloid: categories, distributors and functors.

• U. Höhle, Many-valued topology and its applications.

• F. Borceux and G. Cruciani, Sheaves on a quantale.

$\searrow \swarrow$

$$\mathbf{N} \colon \text{If}\;\; P \;\;\text{is a theorem, then so is}\;\; K P$$

$$w: W \vdash A(w): Type$$

$$w: W \vdash x(w): A(w)$$

$$w: W, x(w): A(w) \vdash (x(w) = x(w)): Prop$$

$$\vdash a: W$$

$$w: W \vdash A(w): Type$$

$$\vdash a^{\ast} A(w) \coloneqq A(a): Type$$

$$w: W \vdash A(w): Type$$

$$\vdash \sum_{w: W} A(w): Type$$

$$w: W \vdash \lozenge_W A(w) \coloneqq W^{\ast} (\sum_{w: W} A(w)): Type$$

1diff structure on S3 ? diff structures on S4 1 diff structures on S5 1 diff structures on S6 28 diff structures on S7, 8.7/2 2 diff structures on S8 8 diff structures on S9 6 diff structures on S10 992 diff structures on S11 32.31 1 diff structures on S12 3 diff structures on S13 2 diff structures on S14 16256 diff structures on S15 128.127

24, 120, 504, 960

$16256 = 128 \cdot 127$,

78, 133, 248

4k+3 ?

$\alpha^{rev}_{X,Y,Z} = \alpha^{-1}_{Z,Y,X}$

Ganesalingam in The Language of Mathematics uses Discourse Representation Theory (DRT) where Ranta uses Dependent Type Theory (DTT). My money is still on DTT. Does anyone using DRT in computerised mathematics?

According to Ganesalingam

DRT was developed to handle Geach’s ‘donkey sentences’ (Geach, 1980) and, as we will show in §3.3.1, there are similar sentences in real mathematical texts. We will also be able to adapt DRT to overcome deficiencies noted by Ranta in his own work; see §3.3.2 for details. (p. 15, n6)

DTT claims to do well with donkey sentences too, as I said in the post.

As far as I can see from the preview, one supposed deficiency of DTT is treated in §3.3.6:

Our approach also correctly handles an area which Ranta highlights as a deficiency of his own analysis. He notes that the plural pronoun ‘they’ is sometimes given a distributive reading and sometimes a collective reading; cf.

Nor do we quite understand the use of the plural pronoun They, which is sometimes distributive, paraphrasable by the term conjunction e.g.

If $A$ and $B$ do not lie outside the line $a$, they are incident on it

but sometimes used on the place of the “surface term conjunction”, so that it fuses together the arguments of the predicate, e.g.

If $a$ and $b$ do not converge, they are parallel.

(Ranta, 1994, p. 12)

Our analysis correctly distinguishes distributive and collective readings. ‘they’ is always taken to be a pronoun introducing an underlined plural discourse referent, requiring a plural antecedent. The difference in the readings of the two sentences given above is accounted for by the fact that ‘incident on it’ is distributive (as a single point is incident on a single line) and the adjective ‘parallel’ is collective (a single line cannot be parallel, but a collection of lines can). (p. 64)

How very odd. I wonder why Ranta believed this to be difficult for DTT? Suppose we have $x, y: A \vdash P(x), Q(x, y): Prop$ and suppose we have $a, b: A$ and $P(a), P(b), Q(a, b)$ all true. Then we would say ‘$a$ and $b$ are $A$s. They are $P$. They are $Q$.’ if sugared versions allow this, such as when $Q$ says of two lines that they’re parallel.

Maybe it’s not clear when such a $Q(a, b)$ affords the sugaring, ‘They are $Q$’. We wouldn’t do this for an asymmetric relation, such as less than. Certainly many symmetric relations are fine, ‘They are parallel/equal/isometric/homeomorphic’.

$Mod(-)$ and $Set^{(-)}$

$$\int_G (f_1 + f_2) = \int_G f_1 + \int_G f_2$$

$$\forall f_1, f_2 \in [G, \mathbb{C}]_{\text{Top}}$$

$(\mathbb{R}^3)^{cpt} \wedge (\mathbb{R}^1)_+ \union (\mathbb{R}^3)_+ \wedge (\mathbb{R}^1)^{cpt}$ different from $(\mathbb{R}^1)^{cpt} \wedge (\mathbb{R}^3)_+ \union (\mathbb{R}^1)_+ \wedge (\mathbb{R}^3)^{cpt}$

$$\array{ \hat E &\stackrel{}{\longrightarrow}& \flat_{dR} \hat E \\ \downarrow &{}^{(pb)}& \downarrow \\ \Pi(\hat E) &\stackrel{ch_E}{\longrightarrow}& \Pi \flat_{dR} \hat E }$$

$$\array{ \hat E &\stackrel{}{\longrightarrow}& \subset_{dR} \hat E \\ \downarrow &{}^{(pb)}& \downarrow \\ \lt(\hat E) &\stackrel{}{\longrightarrow}& \lt \subset_{dR} \hat E }$$

/!!/

$/\!\!/$

$$\array{ T^\infty X &\stackrel{p_1}{\longrightarrow}& X \\ \downarrow^{\mathrlap{p_2}} &(pb)& \downarrow^{\mathrlap{i_X}} \\ X &\stackrel{i_X}{\longrightarrow}& \Im X }$$

$A_\ast B$, $A \star B$, $A * B$

If $\Im(C_2\to C_1\to C_0) = C_2 \to C_0\to C_0$, then base change and adjoints.

$(A_2 \to A_1 \to A_0) \to (C_2 \to C_0\to C_0) \mapsto (A_2 \to A_1 \times_{C_0} C_1 \to A_0) \to (C_2\to C_1\to C_0)$

$$\array{ B_1 \leftarrow A_1 \times_{C_0} C_1 & \to & A_1\\ \downarrow & & \downarrow \\ C_1 & \to & C_0 }$$

So right adjoint to base change:

$(B_2 \to B_1 \to B_0) \to (C_2 \to C_1\to C_0) \mapsto (B_2 \to ?? \to B_0) \to (C_2\to C_0\to C_0)$

Is it just to make $Hom_{H/C_1}(A_1 \times_{C_0} C_1, B_1)$ be equivalent to $Hom_{H/C_0}(A_1, ??)$?

$\displaystyle \int$, $\textstyle \int$, $\textsize \int$, $\scriptsize \int$, $\scriptscriptsize \int$

probability, Probability?

Dynkin diagram?/ Dynkin quiver?	Platonic solid?	finite subgroups of SO(3)?	finite subgroups of SU(2)?	simple Lie group?
$A_{n \geq 1}$		cyclic group? $\mathbb{Z}_{n+1}$	cyclic group? $\mathbb{Z}_{n+1}$	special unitary group? $SU(n+1)$
D4?		Klein four-group? $D_4 \simeq \mathbb{Z}_2 \times \mathbb{Z}_2$	quaternion group? $2 D_4 \simeq$ Q8?	SO(8)?
${\bgcolor{red} D_{n \geq 4}}$	dihedron?, hosohedron?	dihedral group? $D_{2(n-2)}$	binary dihedral group? $2 D_{2(n-2)}$	special orthogonal group? $SO(2n)$
$E_6$	tetrahedron?	tetrahedral group? $T$	binary tetrahedral group? $2T$	E6?
$E_7$	cube?, octahedron?	octahedral group? $O$	binary octahedral group? $2O$	E7?
$E_8$	dodecahedron?, icosahedron?	icosahedral group? $I$	binary icosahedral group? {\bgcolor{red}$2I$}	E8?

\begin{table} \begin{tabular}{l | a | b | a | b} \hline \rowcolor{LightCyan} \mc{1}{} & \mc{1}{x} & \mc{1}{y} & \mc{1}{w} & \mc{1}{z} \ \hline variable 1 & a & b & c & d \ variable 2 & a & b & c & d \ \hline \end{tabular} \end{table}

{ b \color{red} c \color d } e

${\bgcolor{red} a b} c {\bgcolor{#0F0}d e}$

${\bgcolor{red} a}$

${\color{green} b}$

${\bgcolor{green} \color{red} c}$