On the linear distributive structure of Sup (first draft)

J.M. Egger^{∗} David Kruml^{†}

May 10, 2007

Abstract

1 Introduction

This should contain a case for Sup being ``better'' than Rel.  Ideally, not just
from an abstract categorical point of view, but from a concrete linear logic,
theoretical computer science point of view.  It may not be possible to do so,
but if we can then it might open up Mathematical Structures in Computer Science
as a possible destination.
   Once the case is made that Sup is better than Rel, then the need to understand
its linear-distributive and mix structures (which are trivial for Rel) should
follow automatically.  Of course, we can also re-state the concreter results below:
the lax-frobenius stuff, and the von Neumann quantale stuff.

2 Preliminaries

It is by now well-known that Sup forms a ∗-autonomous category—but our notation is sufficiently different from other sources, such as the seminal tomes [1, 5], to merit a few words of review.

We write ∩^{×} for the closed monoidal structure (or, tensor) on Sup, which is more commonly denoted ⊗. Similarly, we use ∩^{×} to denote the universal map

\xymatrix{|x| × |y| \ar[r] & |x ∩^{×} y|}

whose range consists of the so-called pure tensors.

∗Research partially supported by NSERC.

†Supported by the Ministry of Education of the Czech Republic under the project MSM143100009.

Every ϑ ∈ x ∩^{×} y has a canonical presentation as a join pure tensors:

ϑ = ⋁ {α ∩^{×} β | α ∩^{×} β ≤ γ}

but we shall generally be interested in more economical presentations than the canonical one.

If {(α_{j}, β_{j}) | j ∈ I} is cofinal in {(α, β) | α ∩^{×} β ≤ ϑ}, then we call

⋁_{j∈I} α_{j} ∩^{×} β_{j}

a pre-canonical presentation of ϑ. For instance, (⊥_{x} ∩^{×} ⊤_{y}) ∨ (⊤_{x} ∩^{×} ⊥_{y}) is a pre-canonical presentation of ⊥_{x∩^{×}y}, whereas the more obvious ⊥_{x} ∩^{×} ⊥_{y} and ⋁ ∅ are not.

On the other hand, every element of x ∩^{×} y can be written as a join of non-trivial pure tensors, where a pure tensor α ∩^{×} β is called non-trivial if it does not equal ⊥_{x∩^{×}y}—equivalently, if α > ⊥_{x} and β > ⊥_{y}. The advantage of non-trivial pure tensors is that if α ∩^{×} β ≤ γ ∩^{×} δ are non-trivial, then α ≤ γ and β ≤ δ.

Lemma 2.1 For any α ∈ x and β ∈ y,

α ∩^{×} β = (α ∩^{×} ⊤_{y}) ∧ (⊤_{x} ∩^{×} β).

Proof Suppose ζ ∩^{×} ϑ is non-trivial, then

ζ ∩^{×} ϑ ≤ (α ∩^{×} ⊤_{y}) ∧ (⊤_{x} ∩^{×} β) ⟺ ζ ∩^{×} ϑ ≤ α ∩^{×} ⊤_{y} and ζ ∩^{×} ϑ ≤ ⊤_{x} ∩^{×} β
⟺ ζ ≤ α and ϑ ≤ β
⟺ ζ ∩^{×} ϑ ≤ α ∩^{×} β

q.e.d.

Although (Sup, ∩^{×}, 2) is a symmetric monoidal category, there are similar categories— such as (Mod(q), ∩^{×}_{q}, q), for a non-commutative quantale q—which are not. So, in order to stave off any future notational inconsistencies, we shall use the symmetry of ∩^{×} only when strictly necessary.

A corollary of this discipline is that we shall sometimes write x {− \atop ∘} y and sometimes y ∘− x for the internal hom-object of sup-homomorphisms x ⟶ y; similarly, we shall sometimes write x^{∗} and sometimes ^{∗}x for the dual object x {− \atop ∘} 2 = 2 ∘− x.

There is, of course, an isomorphism

\xymatrix{x^{∗} \ar[rr] &  & x^{op} \\ ω & ↦ & _{⋁ ker ω}}

but we shall find it convenient to prefer the former over the latter. We write _{⌞}−_{⌟} for the inverse of the isomorphism above—thus for α, β ∈ x,

⌞α_{⌟}(β) = \{ \begin{matrix}⊥ & if β ≤ α \\ ⊤ & otherwise. \end{matrix}

Definition 2.2 Let x and y be complete lattices; then their par, or dual tensor, is defined by

x ∪^{×} y := (^{∗}y ∩^{×} ^{∗}x)^{∗}.

For α ∈ x and β ∈ y,

α ∪^{×} β := _{⌞}(_{⌞}β_{⌟} ∩^{×} _{⌞}α_{⌟})_{⌟}.

Such elements of x ∪^{×} y will be called pure pars.

Plainly, every element of x ∪^{×} y can be written as a meet of pure pars; we can therefore continue to speak of canonical and pre-canonical presentations of elements of x ∪^{×} y.

Useful intuitions about ∪^{×}, and its relationship to ∩^{×}, can be built from the following example.

Example 2.3 If x = P(j) and y = P(k), then there is an isomorphism

\xymatrix{x ∩^{×} y \ar[rr] &  & P(j × k) \\ α ∩^{×} β & ↦ & α × β.}

Now, since complementation defines an isomorphism P(k)^{op} ⟶^{∼} P(k), we also have

x ∪^{×} y ⟶^{∼} (P(j)^{op} ∩^{×} P(k)^{op})^{op}
⟶^{∼} (P(j) ∩^{×} P(k))^{op}
⟶^{∼} P(j × k)^{op}
⟶^{∼} P(j × k)

But, under this isomorphism, α ∪^{×} β corresponds, not to α × β = (α × y) ∩ (x × β), but rather its “de Morgan dual”

(α × y) ∪ (x × β).

In particular, the composite isomorphism x ∩^{×} y ⟶^{∼} x ∪^{×} y is given by

α ∩^{×} β ↦ (α ∪^{×} ⊥_{y}) ∧ (⊥_{x} ∪^{×} β)

and not by α ∩^{×} β ↦ α ∪^{×} β.

Note also that the coatoms of P(j × k) are pure pars.

This example can be easily extended to completely distributive (alias, totally continuous) lattices x and y—these necessarily have the form 𝔻(j, ≪) for some karrel (j, ≪), [7].

While the “geometric” intuition of α ∪^{×} β provided by the previous example can be useful, we shall not abandon its definition as a particular sup-homomorphism.

Lemma 2.4

Suppose α ∈ x, β ∈ y, ψ ∈ ^{∗}y and ω ∈ ^{∗}x; then (α ∪^{×} β)(ψ ∩^{×} ω) ≤ ω(α) ∨ ψ(β).

Proof If either ω = ⊥_{^{∗}x} or ψ = ⊥_{^{∗}y}, then ψ ∩^{×} ω = ⊥_{^{∗}x}∩^{×}_{^{∗}y}, and so the inequality holds trivially. On the other hand, if ω > ⊥_{^{∗}x} and ψ > ⊥_{^{∗}y}, then, by definition, we have

(α ∪^{×} β)(ψ ∩^{×} ω) = ⊥ ⟺ _{⌞}(_{⌞}β_{⌟} ∩^{×} _{⌞}α_{⌟})_{⌟} = ⊥
⟺ ψ ∩^{×} ω ≤ _{⌞}β_{⌟} ∩^{×} _{⌞}α_{⌟}.
⟺ ψ ≤ _{⌞}β_{⌟} and ω ≤ _{⌞}α_{⌟}
⟺ ψ(β) = ⊥, and ω(α) = ⊥
⟺ ψ(β) ∨ ω(α) = ⊥

—and so we obtain an equality

(α ∪^{×} β)(ψ ∩^{×} ω) = ω(α) ∨ ψ(β)

in this case. q.e.d.

3 Linear distributions

In an arbitrary ∗-autonomous category, the two monoidal structures, ∩^{×} and ∪^{×}, are linked by a pair of (generally non-invertible) natural transformations

[figure: x ∩^{×} (y ∪^{×} z); ^{\overrightarrow{κ}^{x,y,z}}; (x ∩^{×} y) ∪^{×} z; (x ∪^{×} y) ∩^{×} z; _{\overleftarrow{κ}_{x,y,z}}; x ∪^{×} (y ∩^{×} z)]

which are called linear distributions, [2].

The construction of \overrightarrow{κ} follows easily from the fact that

d ∘− (x ∩^{×} y) ≅ (d ∘− y) ∘− x

holds in an arbitrary right-closed monoidal category. And if we agree to denote the action of the composite

[figure: ^{∗}(x ∩^{×} y) ∩^{×} x; ∼; (^{∗}y ∘− x) ∩^{×} x; ε; ^{∗}y]

by ψ ∩^{×} α ↦ ψ(α ∩^{×} ( )), then we can describe the action of \overrightarrow{κ} as follows:

[figure: x ∩^{×} (y ∪^{×} z); ^{\overrightarrow{κ}^{x,y,z}}; (x ∩^{×} y) ∪^{×} z = (^{∗}z ∩^{×} ^{∗}(x ∩^{×} y))^{∗}; α ∩^{×} ω; ↦; [ζ ∩^{×} ψ ↦ ω[ζ ∩^{×} ψ(α ∩^{×} ( ))]].]

The objective of this section is a more malleable description of the same map.

Theorem 3.1 Let x, y, z be arbitrary sup-lattices. Then the sup-homomorphism

x ∩^{×} (y ∪^{×} z) \underrightarrow{\overrightarrow{κ}_{x,y,z}} (x ∩^{×} y) ∪^{×} z

maps

α ∩^{×} ⋀_{j∈I} (β_{j} ∪^{×} γ_{j}) ↦ ⋀_{j∈I} ((α ∩^{×} β_{j}) ∪^{×} γ_{j})

whenever ⋀_{j∈I} (β_{j} ∪^{×} γ_{j}) is a pre-canonical presentation of an element of y ∪^{×} z.

Before proving this theorem, let us present a pair of examples demonstrating the necessity of the final proviso.

Examples 3.2

1. If the formula were correct in the case I = ∅, then we would get that \overrightarrow{κ} maps α ∩^{×} ⊤_{y∪^{×}z} to ⊤_{(x∩^{×}y)∪^{×}z}. By contrast, if we pre-canonically present ⊤_{y∪^{×}z} as (⊥_{y} ∪^{×} ⊤_{z}) ∧ (⊤_{y} ∪^{×} ⊥_{z}), then the formula yields

α ∩^{×} [(⊥_{y} ∪^{×} ⊤_{z}) ∧ (⊤_{y} ∪^{×} ⊥_{z})] ↦ [(α ∩^{×} ⊥_{y}) ∪^{×} ⊤_{z}] ∧ [(α ∩^{×} ⊤_{y}) ∪^{×} ⊥_{z}]
= ⊤_{(x∩^{×}y)∪^{×}z} ∧ [(α ∩^{×} ⊤_{y}) ∪^{×} ⊥_{z}]
= (α ∩^{×} ⊤_{y}) ∪^{×} ⊥_{z}

which does not equal ⊤_{(x∩^{×}y)∪^{×}z} unless α = ⊤_{x}.

[This only proves that the formula is ill-defined, if allowed to run over arbitrary presentations of elements of y ∪^{×} z.]

2. If γ ≠ ⊥_{z} then \overrightarrow{κ} does not map ⊥_{x} ∩^{×} (β ∪^{×} γ) to (⊥_{x} ∩^{×} β) ∪^{×} γ, for the simple reason

that

⊥_{x} ∩^{×} (β ∪^{×} γ) = ⊥_{x∩^{×}(y∪^{×}z)} ↦ ⊥_{(x∩^{×}y)∪^{×}z}

whereas

(⊥_{x} ∩^{×} β) ∪^{×} γ = ⊥_{x∩^{×}y} ∪^{×} γ ≠ ⊥_{(x∩^{×}y)∪^{×}z}

unless γ = ⊥_{z}.

[This proves that the formula is incorrect if allowed to run over arbitrary presentations of elements of y ∪^{×} z.]

Proof of Theorem 3.1 Fix α ∈ x, ω ∈ y ∪^{×} z and let ⋀_{j∈I} (β_{j} ∪^{×} γ_{j}) be a pre-canonical presentation of ω. We will show, not only that ⋀_{j∈I} (α ∩^{×} β_{j}) ∪^{×} γ_{j} equals \overrightarrow{κ}_{x,y,z}(α ∩^{×} ω), but that it is also

a pre-canonical presentation of \overrightarrow{κ}_{x,y,z}(α ∩^{×} ω). To do so, we must investigate which pairs

(ϑ, γ) satisfy \overrightarrow{κ}_{x,y,z}(α ∩^{×} ω) ≤ ϑ ∪^{×} γ.

But the following argument

\overrightarrow{κ}_{x,y,z}(α ∩^{×} ω) ≤ ϑ ∪^{×} γ = _{⌞}(_{⌞}γ_{⌟} ∩^{×} _{⌞}ϑ_{⌟})_{⌟} ⟺ (\overrightarrow{κ}_{x,y,z}(α ∩^{×} ω))(_{⌞}γ_{⌟} ∩^{×} _{⌞}ϑ_{⌟}) = ⊥
⟺ ω[_{⌞}γ_{⌟} ∩^{×} _{⌞}ϑ_{⌟}(α ∩^{×} ( ))] = ⊥
⟺ _{⌞}γ_{⌟} ∩^{×} _{⌞}ϑ_{⌟}(α ∩^{×} ( )) ≤ ⋁_{j∈I} (_{⌞}γ_{j}_{⌟} ∩^{×} _{⌞}β_{j}_{⌟})
⟺ (∃j ∈ I)(_{⌞}γ_{⌟} ≤ _{⌞}γ_{j}_{⌟},_{⌞}ϑ_{⌟}(α ∩^{×} ( )) ≤ _{⌞}β_{j}_{⌟})
⟺ (∃j ∈ I)(γ ≥ γ_{j},_{⌞}ϑ_{⌟}(α ∩^{×} β_{j}) = ⊥)
⟺ (∃j ∈ I)(γ ≥ γ_{j}, ϑ ≥ α ∩^{×} β_{j})

does indeed show that \{(α ∩^{×} β_{j}, γ_{j}) | j ∈ I\} is co-cofinal in \{(ϑ, γ) | \overrightarrow{κ}_{x,y,z}(α ∩^{×} ω) ≤ ϑ ∪^{×} γ\}.

q.e.d.

Of course there is a symmetric description of \overleftarrow{κ}.

4 Lax Frobenius relations

An application of the previous theorem is a highly interesting diagrammatic description of linear distributive quantales.

Definition 4.1

A (biunital) linear distributive quantale is a complete lattice q equipped with two associative (unital) binary operations, & and ⅋, such that

1. & distributes joins (i.e., (q, &) is a quantale);

2. ⅋ distributes meets (i.e., (q, ⅋) is a coquantale); and

3. linear distributivity holds, which in the posetal case just means that

α & (β ⅋ γ) ≤ (α & β) ⅋ γ
(α ⅋ β) & γ ≤ α ⅋ (β & γ).

It is well-known that (unital) quantales are the same thing as semigroups (monoids) in (Sup, ∩^{×}, 2). It should therefore not come as much of a surprise that (counital) coquantales are the same thing as cosemigroups (comonoids) in (Sup, ∪^{×}, 2). More generally we have:

Lemma 4.2

Sup-homomorphisms x ⟶ y ∪^{×} z are in bijective correspondence with functions |z| × |y| ⟶ |x| which distribute meets.

Proof Given a sup-homomorphism x ⟶^{δ} y ∪^{×} z, the composite

[figure: ^{∗}z ∩^{×} ^{∗}y; ∼; ^{∗}(y ∪^{×} z); ^{∗}δ; ^{∗}x]

corresponds uniquely to a map

[figure: |z|^{op} × |y|^{op}; ∼; |^{∗}z| × |^{∗}y|; |^{∗}x|; ∼; |x|^{op}]

which distributes joins. But, of course, a join in x^{op} is a meet in x, etc. q.e.d.

Theorem 4.3

Let q be a complete lattice equipped with two associative binary operations, & and ⅋, which respectively distribute joins and meets. Let q ∩^{×} q ⟶^{μ} q be the sup-homomorphism corresponding to & and q ⟶^{δ} q ∪^{×} q be that corresponding to ⅋^{op} (where α ⅋^{op} β := β ⅋ α).

Then & and ⅋ satisfy linear distributivity if and only if there exist 2-cells

[figure: q ∩^{×} q; ι_{q} ∩^{×} δ; μ; ⇒; q ∩^{×} (q ∪^{×} q); _{\overrightarrow{κ}_{q,q,q}}; q ∩^{×} q; δ ∩^{×} ι_{q}; μ; ⇒; (q ∪^{×} q) ∩^{×} q; _{\overleftarrow{κ}_{q,q,q}}; (q ∩^{×} q) ∪^{×} q; μ ∪^{×} ι_{q}; q ∪^{×} (q ∩^{×} q); ι_{q} ∪^{×} μ; q; δ; q ∪^{×} q; q; δ; q ∪^{×} q]

in Sup.

Before proving this theorem, let us note that the diagrams contained therein are lax versions of the Frobenius relations, which are important in algebra and physics. Moreover, the first author has already shown that Frobenius monoids in Sup (which, as a result of this theorem, can be described as biunital linear distributive quantales where the 2-cells are invertible) are essentially the same as ∗-autonomous quantales [3]. The resulting idea that linear distributivity is a lax form of ∗-autonomy is quite unexpected, and should probably be explored in greater depth.

Proof of Theorem 4.3

We leave it to the reader as an exercise that, for ϑ ∈ q, the canonical presentation of δ(ϑ) is

⋀ {β ∪^{×} γ | β ⅋ γ ≥ ϑ}.

Thus the composite

[figure: q ∩^{×} q; μ; q; δ; q ∪^{×} q]

maps a pure tensor as follows:

α ∩^{×} ϑ ↦ α & ϑ ↦ ⋀ {ζ ∪^{×} γ | ζ ⅋ γ ≥ α & ϑ}

—whereas, by Theorem 3.1, the composite

[figure: q ∩^{×} q; ι_{q} ∩^{×} δ; q ∩^{×} (q ∪^{×} q); ^{\overrightarrow{κ}^{q,q,q}}; (q ∩^{×} q) ∪^{×} q; μ ∪^{×} ι_{q}; q ∪^{×} q]

maps a pure tensor as follows:

α ∩^{×} ϑ ↦ α ∩^{×} ⋀ {β ∪^{×} γ | β ⅋ γ ≥ ϑ}
↦ ⋀ {(α ∩^{×} β) ∪^{×} γ | β ⅋ γ ≥ ϑ}
↦ ⋀ {(α & β) ∪^{×} γ | β ⅋ γ ≥ ϑ}.

Hence the diagram

[figure: q ∩^{×} q; ι_{q} ∩^{×} δ; μ; ⇒; q ∩^{×} (q ∪^{×} q); _{\overrightarrow{κ}_{q,q,q}}; (q ∩^{×} q) ∪^{×} q; μ ∪^{×} ι_{q}; q; δ; q ∪^{×} q]

is equivalent to

⋀ {(α & β) ∪^{×} γ | β ⅋ γ ≥ ϑ} ≥ ⋀ {ζ ∪^{×} γ | ζ ⅋ γ ≥ α & ϑ}

for all α, ϑ ∈ q. But since the latter is a canonical presentation, this reduces to

{((α & β), γ) | β ⅋ γ ≥ ϑ} ⊆ {(ζ, γ) | ζ ⅋ γ ≥ α & ϑ} .

Now, on the one hand, if &, ⅋ satisfy linear distributivity, then β ⅋ γ ≥ ϑ implies

(α & β) ⅋ γ ≥ α & (β ⅋ γ)
≥ α & ϑ

and so we are done.

On the other hand, choosing ϑ = β′ ⅋ γ′ we obtain

((α & β′), γ′) ∈ {((α & β), γ) | β ⅋ γ ≥ β′ ⅋ γ′} ⊆ {ζ ∪^{×} γ | ζ ⅋ γ ≥ α & (β′ ⅋ γ′)}

and hence (α & β′) ⅋ γ′ ≥ α & (β′ ⅋ γ′).

The equivalence of the second diagram with the second half of linear distributivity follows symmetrically. q.e.d.

5 Mix maps

In Sup, ∩^{×} and ∪^{×} are further linked by the fact that they happen to have the same (isomorphic) units. This, in turn, induces the existence of a natural transformation ∩^{×}⟶^{ϕ}∪^{×}, called mix, whose components are defined as follows.

[figure: x ∩^{×} y; ϕ_{x,y}; x ∪^{×} y = ((^{∗}y ∩^{×} ^{∗}x) {− \atop ∘} 2); α ∩^{×} β; ↦; [ψ ∩^{×} ω ⤇ ω(α) ∧ ψ(β)]]

Once again, the objective of this section will be to find a more malleable description of this map.

Theorem 5.1

For arbitrary complete lattices x and y, the mix map x ∩^{×} y ⟶^{ϕ_{x,y}} x ∪^{×} y can be described by the formula

α ∩^{×} β ↦ (α ∪^{×} ⊥_{y}) ∧ (⊥_{x} ∪^{×} β)

(which appeared earlier in Example 2.3).

Proof

First, we show that ϕ_{x,y}(α ∩^{×} ⊤_{y}) = α ∪^{×} ⊥_{y}. According to the definition of ϕ_{x,y} above, the action of ϕ_{x,y}(α ∩^{×} ⊤_{y}) on non-trivial pure tensors is

ψ ∩^{×} ω ↦ ω(α) ∧ ψ(⊤_{y}) = ω(α)

since ψ(⊤_{y}) = ⊥ if and only if ψ = ⊥_{^{∗}y}—in all other cases we have ψ(⊤_{y}) = ⊤. But, according to the proof of Lemma 2.4, the action of α ∪^{×} ⊥_{y} on non-trivial pure tensors is also

ψ ∩^{×} ω ↦ ω(α) ∨ ψ(⊥_{y}) = ω(α).

It follows by a symmetric argument that ϕ_{x,y}(⊤_{x} ∩^{×} β) = ⊥_{x} ∪^{×} β. Hence, Lemma 2.1 implies

ϕ_{x,y}(α ∩^{×} β) = ϕ_{x,y}((α ∩^{×} ⊤_{y}) ∧ (⊤_{x} ∩^{×} β))
≤ ϕ_{x,y}(α ∩^{×} ⊤_{y}) ∧ ϕ_{x,y}(⊤_{x} ∩^{×} β)
= (α ∪^{×} ⊥_{y}) ∧ (⊥_{x} ∪^{×} β).

To show the converse, we use the fact that meets in z ∘− w are less than or equal to pointwise meets.

((α ∪^{×} ⊥_{y}) ∧ (⊥_{x} ∪^{×} β))(ψ ∩^{×} ω) ≤ (α ∪^{×} ⊥_{y})(ψ ∩^{×} ω) ∧ (⊥_{x} ∪^{×} β)(ψ ∩^{×} ω)
≤ (ω(α) ∨ ψ(⊥_{y})) ∧ (ω(⊥_{x}) ∨ ψ(β))
= (ω(α) ∨ ⊥) ∧ (⊥ ∨ ψ(β))
= ω(α) ∧ ψ(β)
= (ϕ_{x,y}(α ∩^{×} β))(ψ ∩^{×} ω)

holds for all ψ ∈ ^{∗}y and ω ∈ ^{∗}x. q.e.d.

6 Translations

The second author has introduced the use of mix maps, in the case when y = ^{∗}x, to solve a particular concrete problem in quantale theory: whether, given an arbitrary complete lattice x, it is possible to construct a von Neumann quantale whose sublattice of right-sided elements is isomorphic to x, [4].

In this case, we have x ∪^{×} ^{∗}x ≅ x ∘− x; and the latter is the generic example of a unital quantale, so it is unsurprising that quantale theorists have developed standard notation for its elements. This section exists to make the appropriate translations between our notation for elements x ∪^{×} y (in the case y = ^{∗}x) and the latter.

Definition 6.1 Let x be a complete lattice, and α, β ∈ x, then ρ_{α} and λ_{β} denote the composites

[figure: x; ^{^{⌞}⊥_{x}^{⌟}}; 2; ^{⌜}α^{⌝}; x; x; _{⌞}β_{⌟}; 2; _{_{⌜}⊤_{x}_{⌝}}; x]

respectively. More explicitly,

ρ_{α}(γ) = \{ \begin{matrix}⊥_{x} & if γ = ⊥_{x} \\ α & otherwise \end{matrix} and λ_{β}(γ) = \{ \begin{matrix}⊥_{x} & if γ ≤ β \\ ⊤_{x} & otherwise \end{matrix}

The previous maps have been identified as the right- and left-sided elements of x ∘− x, [6].

Lemma 6.2 The isomorphism x ∪^{×} ^{∗}x ⟶^{∼} x ∘− x maps α ∪^{×} _{⌞}β_{⌟} to ρ_{α} ∨ λ_{β}. In particular, it maps

α ∪^{×} ⊥_{^{∗}x} = α ∪^{×} _{⌞}⊤_{x}_{⌟} ↦ ρ_{α} ∨ λ_{⊤_{x}} = ρ_{α}
⊥_{x} ∪^{×} _{⌞}β_{⌟} ↦ ρ_{⊥_{x}} ∨ λ_{β} = λ_{β}.

Proof The canonical isomorphism x ∪^{×} ^{∗}x ⟶^{∼} x ∘− x is just the transpose of

[figure: (x ∪^{×} ^{∗}x) ∩^{×} x; \overleftarrow{κ}; x ∪^{×} (^{∗}x ∩^{×} x); x ∪^{×} 2; ∼; x]

So we can apply Theorem 3.1:

[(⊤_{x} ∪^{×} ⊥_{^{∗}x}) ∧ (α ∪^{×} _{⌞}β_{⌟}) ∧ (⊥_{x} ∪^{×} ⊤_{^{∗}x})] ∩^{×} γ

↦ [⊤_{x} ∪^{×} (⊥_{^{∗}x} ∩^{×} γ)] ∧ [α ∪^{×} (_{⌞}β_{⌟} ∩^{×} γ)] ∧ [⊥_{x} ∪^{×} (⊤_{^{∗}x} ∩^{×} γ)]
↦ ⊤ ∧ [α ∪^{×} (_{⌞}β_{⌟}(γ))] ∧ [⊥_{x} ∪^{×} (⊤_{^{∗}x}(γ))]
↦ [α ∨ (_{⌞}β_{⌟}(γ))] ∧ (⊤_{^{∗}x}(γ))

Now if γ = ⊥, the latter expression evaluates to (α ∨ ⊥) ∧ ⊥ = ⊥; if ⊥ < γ ≤ β, it evaluates to (α ∨ ⊥) ∧ ⊤ = α; otherwise, it evaluates to (α ∨ ⊤) ∧ ⊤ = ⊤.

But since joins in x ∘− x are computed pointwise, it is easy to see that ρ_{α} ∨ λ_{β} also maps

γ ↦ \{ \begin{matrix}⊥ & if γ = ⊥_{x} \\ α & if ⊥_{x} < γ ≤ β \\ ⊤ & otherwise. \end{matrix}

q.e.d.

The fact that every element of x ∘− x can be written as a meet of elements of the form ρ_{α} ∨ λ_{β} is equivalent to the simplicity of x ∘− x as a quantale, [6].

Lemma 6.3 For any α, β ∈ x, ρ_{α} ∧ λ_{β} = ρ_{α} ∘ λ_{β}.

Proof

Meets in x ∘− x can be found by first computing the pointwise meet, and then finding the largest sup-homomorphism beneath that.

But the pointwise meet of ρ_{α} and λ_{β}

γ ↦ \{ \begin{matrix}⊥ & if γ ≤ β \\ α & otherwise. \end{matrix}

is already a sup-homomorphism—it equals ρ_{α} ∘ λ_{β}. Therefore this is ρ_{α} ∧ λ_{β}. q.e.d. Combining the previous two lemmata with Theorem 5.1, we immediately obtain:

Theorem 6.4 The composite

[figure: x ∩^{×} ^{∗}x; ϕ_{x,^{∗}x}; x ∪^{×} ^{∗}x; ∼; x ∘− x]

can be described by

α ∩^{×} _{⌞}β_{⌟} ↦ ρ_{α} ∘ λ_{β}.

Example 6.5

Let M_{3} denote the five-element modular but non-distributive lattice. Then the six automorphisms of M_{3} do not lie in the range of

[figure: M_{3} ∩^{×} ^{∗}M_{3}; ϕ_{M_{3},^{∗}M_{3}}; M_{3} ∪^{×} ^{∗}M_{3}; ∼; M_{3} ∘− M_{3}]

because …

This is in accordance with the well-known fact that ϕ_{x,^{∗}x} is invertible if and only if x is completely distributive.

7 Conclusion

Blah, blah, blah.

References

[1] Michael Barr. ∗-autonomous categories, volume 752 of Lecture Notes in Mathematics. Springer, Berlin, 1979. With an appendix by Po Hsiang Chu.

[2] J. R. B. Cockett and R. A. G. Seely. Weakly distributive categories. J. Pure Appl. Algebra, 114(2):133–173, 1997.

[3] J.M. Egger. The Frobenius relations meet linear distributivity. In Proceedings of CT’06 (White Point), volume ? of Theory and Applications of Categories, pages ?–? ??, ???, 2007.

[4] J.M. Egger and David Kruml. Girard couples in quantale theory. to appear, June 2007.

[5] André Joyal and Myles Tierney. An extension of the Galois theory of Grothendieck. Mem. Amer. Math. Soc., 51(309):vii+71, 1984.

[6] Jan Paseka et al. An appropriate selection of articles. Various Journals, n(m):j–k, wxyz.

[7] Robert Rosebrugh and R. J. Wood. Constructive complete distributivity. IV. Appl. Categ. Structures, 2(2):119–144, 1994.