In Categories, Allegories, Freyd and Scedrov allude to a first attempt to define power allegory as an allegory $\mathcal{A}$ satisfying a power object axiom: the inclusion $i: Map(\mathcal{A}) \to \mathcal{A}$ has a right adjoint $P$. The word βattemptβ probably signals that this is probably not an optimal definition: we probably need to assume more than just an allegory plus power objects in order to build an interesting theory. Indeed Freyd and Scedrov wind up assuming $\mathcal{A}$ is a division allegory, embodying quite a lot of internal logic from the get-go, before they introduce power objects.
But the snappy immediacy of the power object axiom leads one to wonder what other assumptions on an allegory lead to a good theory of power allegories. In these notes we will see how far we get if we add one or both of the following assumptions:
The allegory admits finite coproducts (equivalently finite cartesian products, since allegories are self-dual).
The allegory is a bicategory of relations in the sense of Carboni-Walters (equivalently, a unitary pretabular allegory).
Our main focus is on the first assumption, where we show that an allegory with sums satisfying the power object axiom must be a division allegory, and indeed a positive power allegory in the terminology of Freyd-Scedrov, at which point we can piggy-back on their results. This is an interesting and perhaps surprising development, which in a loose sense is dual to the usual development of topos theory. In ordinary topos theory, having a subobject classifier, one may start with negative types (finite limits, exponentials, etc.), and derive positive types and formulas (finite colimits, internal unions, existential quantification, etc.). Whereas in allegory theory, the the initial emphasis is on positive formulas (relational composition is after all guarded existential quantification) and here we assume some positive types (namely finite coproducts); then when we add in the power object axiom, we can derive negative formulas in the form of division allegory structure involving guarded universal quantification. Under the finite coproduct axiom or bicategory of relations axiom, we can also construct some exponentials out of power objects.
If $r: A \to B$ has a right adjoint $s: B \to A$ in an allegory $\mathcal{A}$, then $s = r^{op}$.
Given $r \dashv s$, we have $1_A \leq s r$ and $r s \leq 1_B$. Then
by the modular law. Clearly
as well, so $r \dashv s \wedge r^{op}$. It follows that $s = s \wedge r^{op}$, or $s \leq r^{op}$. By similar reasoning,
and $r \wedge s^{op} \dashv s$, so $r \wedge s^{op} = r$ or $r \leq s^{op}$. Thus both $r^{op} \leq s$ and $s \leq r^{op}$, as desired.
It is not known to me whether allegorical structure is property-like with respect to underlying $Pos$-enriched categories, but we have the following partial result involving cartesian bicategories (which are property-like with respect to underlying 2-categories).
Let $\mathbf{B}$ be a (locally posetal) cartesian bicategory. Then $\mathbf{B}$ carries at most one allegory structure. Indeed, a (locally posetal) cartesian bicategory is an allegory iff it is a bicategory of relations.
First we show that if $\mathbf{B}$ carries an allegory structure, then it satisfies the Frobenius equations
(where $\delta \dashv \delta^{op}$, of course), making $\mathbf{B}$ a bicategory of relations. Then we show that a bicategory of relations carries exactly one allegory structure.
Given such an allegory $\mathbf{B}$, we have for any map $f: A \to B$ and morphisms $r: B \to C$, $s: A \to C$ the equation
where the inequality $\leq$ comes for free, and the inequality $\geq$ is an instance of the modular law. Now put $f = \delta_A$, $r = \epsilon_A^{op} \otimes 1_A$, and $s = \epsilon_A \otimes 1_A \otimes \epsilon_A^{op}$. Then string diagrammatic calculations show
where $\sigma_A: A \otimes A \to A \otimes A$ is the symmetry isomorphism. The first Frobenius equation follows (and this is enough: if one Frobenius equation holds, then so does the other).
That a bicategory of relations $\mathbf{B}$ is an allegory is shown in the nLab; here, letting $\eta_A = \delta_A \epsilon_A^{op}: 1 \to A \otimes A$, the opposite of a morphism $r: A \to B$ is given by
The point is that any candidate $r^{op}$ for an allegorical structure must be equal to these expressions. We have for example
where the second line amounts to an instance of the modular law $t \wedge r s \leq r(r^{op} t \wedge s)$ (taking $t = \pi_1: B \otimes A \to B$ and $s = \pi_2: B \otimes A \to A$), and the lines thereafter are valid in bicategories of relations. But now it follows that
where the first line follows from identities in bicategories of relations (that are most easily verified through string diagrams). Swapping the roles of $r$ and $r^{op}$, this gives
The same line of argument shows
followed by
so we are done.
The following result is well-known and is proven in the nLab in the article βbicategory of relationsβ; it will not be reproven here.
A bicategory of relations $\mathbf{B}$ is a compact closed bicategory for which each object $B$ is dual to itself, with unit $\eta_B: 1 \to B \otimes B$ and counit $\eta_B^{op}: B \otimes B \to 1$.
In the sequel we will follow customary practice and denote the tensor product in $\mathbf{B}$ by $\times$ (which is an actual cartesian product when restricted to $Map(\mathbf{B})$).
Now suppose our allegory $\mathbf{B}$ is a power allegory: admits a right adjoint $P$ to the inclusion $i: Map(\mathbf{B}) \to \mathbf{B}$ of 1-categories.
Notation:
We generally drop $i$, and denote a component of the counit of $i \dashv P$ by $\ni_A \colon P(A) \to A$. It can be regarded as opposite to a membership relation (and thus we write $\in_A = \ni_A^o$, where $(-)^o$ is the βopposite relationβ involution on an allegory).
The unit $\sigma \colon A \to P(A)$ is a map and can be regarded as a singleton relation. It is the unique map $f \colon A \to P(A)$ such that $\ni_C f = 1_A$.
In general, given $r \colon A \to B$,
denotes the unique map such that $\ni_B \chi_r = r$. It is also called the classifying map of $r$.
Let $r: A \to C$ and $s: B \to C$ be arrows of $\mathbf{B}$. The right Kan lift $s \backslash r$ of $r$ through $s$, if it exists, is the unique arrow $A \to B$ such that for all $t: A \to B$ we have $t \leq s \backslash r$ iff $s t \leq r$.
Existence of right Kan lifts implies that $\mathbf{B}$ is a division allegory. For if $r: A \to B$ and $s: A \to C$ are arrows, we can form the right Kan extension $r/s: B \to C$ by $r/s = (s^o\backslash r^o)^o$, since
Suppose that for an object $C$ of $\mathbf{B}$ the arrow $\ni_C\backslash \ni_C$ exists. Then for every pair $r: A \to C$, $s: B \to C$, the arrow $s \backslash r: A \to B$ exists.
Since $r = \ni_C \chi_r$ and $s = \ni_C \chi_s$, we have
where we have used $\chi_r \dashv \chi_r^o$ and $\chi_s \dashv \chi_s^o$. Thus $s \backslash r = \chi_s^o (\ni_C \backslash \ni_C) \chi_r$.
Define the internal union by $\bigcup_C = P(\ni_C): P P(C) \to P(C)$, or in other words as the classifying map of the composite
Define the internal order $[\Rightarrow] \colon P(C) \to P(C)$ by the composite
Its opposite is $[\Leftarrow] \coloneqq \ni_{P(C)} \bigcup_C^o$. We will show that under suitable conditions, $[\Leftarrow] = \ni_C \backslash \ni_C$.
$\ni_C [\Leftarrow] \leq \ni_C$.
We have a diagram
Note in fact that the counit 2-cell $\geq$ is an equality because $\bigcup_C$ retracts $\sigma_{P C}$ (see the following proposition): we have $1 = \bigcup_C \sigma_{P C} \sigma_{P C}^o \bigcup_C^o \leq \bigcup_C \bigcup_C^o$ where the inequality uses the counit $\sigma \sigma^o \leq 1$.
The internal relation $[\Leftarrow]: P C \to P C$ is reflexive: $1_{P C} \leq [\Leftarrow]$.
By a triangular equation for the adjunction $i \dashv P: \mathbf{B} \to Map(\mathbf{B})$, we have $1_{P C} = P(\ni_C) \sigma_{P C} = \bigcup_C \sigma_{P C}$. Thus $1_{P C} = \sigma_{P C}^o \bigcup_C^o$, and it suffices to show $\sigma_{P C}^o \leq \ni_{P C}: P P C \to P C$. But this is equivalent to $1_{P C} \leq \ni_{P C} \sigma_{P C}$, which holds as an instance of the other triangular equation.
If $R: P C \to P C$ is reflexive, then $\ni_C R \leq \ni_C$ if and only if $R \leq {[\Leftarrow]}$.
If $R \leq [\Leftarrow]$, then $\ni_C R \leq \ni_C [\Leftarrow] \leq \ni_C$ by Proposition 2. If $\ni_C R \leq \ni_C$ and $1 \leq R$, then also $\ni_C \leq \ni_C R$, so $\ni_C R = \ni_C$. In that case, $P(\ni_C) P(R) = P(\ni_C)$, which implies $P(R) \leq P(\ni_C)^o P(\ni_C) = \bigcup_C^o P(\ni_C)$. We then have $R = \ni_{P C} P(R) \sigma_{P C} \leq \ni_{P C} \bigcup _C^o P(\ni_C) \sigma_{P C} = \ni_{P C} \bigcup_C^o = [\Leftarrow]$. This completes the proof.
$[\Leftarrow]$ is transitive: $[\Leftarrow] \circ [\Leftarrow] \leq [\Leftarrow]$.
By Proposition 3, $[\Leftarrow] [\Leftarrow]$ is reflexive. So, by Proposition 4, it suffices to observe that $\ni_C [\Leftarrow] [\Leftarrow] \leq \ni_C$, but this is immediate from Proposition 2.
In addition to the power object axiom, we assume in this section that the allegory $\mathbf{B}$ has coproducts $A + B$. As we remarked earlier, $A + B$ also plays the role of cartesian product since allegories are dagger categories (or alternatively since allegories have local meets and are therefore $CMon$-enriched). It follows, since right adjoints preserve products, that $P(A + B)$ is a product $P(A) \times P(B)$ in $Map(\mathbf{B})$.
Let $0$ denote the initial object of $\mathbf{B}$.
For any object $C$, the unique arrow $!_{P C}: 0 \to P C$ is a map (a left adjoint), and $!_C: 0 \to C$ is also a map.
Of course there exists a map $\chi_{!_C}: 0 \to P C$ that classifies the arrow $!_C: 0 \to C$, and this map is the unique arrow $!_{P C}: 0 \to P C$. Then, we have $\sigma_C !_C = !_{P C}$, so we have a counit $\sigma_C !_{P C} !_{P C}^o \sigma_C^o \leq 1$, which implies
giving a counit for a putative adjunction $!_C \dashv !_C^o$. On the other hand, we also have a unit $1_0 \leq !_C^o !_C$, in fact an equality there is only one arrow $0 \to 0$ in the first place.
The coproduct functor $+: \mathbf{B} \times \mathbf{B} \to \mathbf{B}$ preserves local meets (and in particular is $Pos$-enriched).
This follows from a more general lemma that if the underlying category $B$ of a $CMon$-enriched category has coproducts/biproducts, then the coproduct/biproduct functor $\oplus: B \times B \to B$ is $CMon$-enriched. This amounts to a claim of type
where the matrix entries on the right may be extracted by pre-composing and post-composing with coproduct injections and product injections, e.g., $a_{11} = p_1 \circ A \circ i_1$ where $A$ is the matrix sum on the left, and we use the fact that such composition is $CMon$-enriched.
The coproduct inclusion arrows $i_1, i_2: C \to C + C$ are maps.
Since $C + -: \mathbf{B} \to \mathbf{B}$ is $Pos$-enriched, it takes left adjoints to left adjoints. Hence $C + !_C: C + 0 \to C + C$ is a map, and this may be identified with a map $i_1: C \to C + C$, the first coproduct inclusion. Similarly, $i_2$ is a map.
The codiagonal $\nabla_{P C}: P C + P C \to P C$ is a map.
In fact we claim that the map $\chi \coloneqq \chi_{(\ni_C, \ni_C)}: P C + P C \to P C$ must be $\nabla$. By the previous lemma, $\chi i_1$ and $\chi i_2$ are maps; they classify $(\ni_C, \ni_C) \circ i_1 = \ni_C$ and $(\ni_C, \ni_C) \circ i_2 = \ni_C$. But $1_{P C}: P C \to P C$ is the unique classifying map of $\ni_C$; therefore $\chi i_1 = 1_{P C}$ and $\chi i_2 = 1_{P C}$. At the same time, $\nabla: P C + P C \to P C$ is the unique arrow $f$ in $\mathbf{B}$ such that $f i_1 = 1_{P C} = f i_2$. We conclude $\nabla = \chi$.
The codiagonal $\nabla_C: C + C \to C$ satisfies $\nabla_C \nabla_C^o = 1_C$.
By the previous lemma, the composite $\sigma_C \nabla_C$ is a map, being a composite of maps $\nabla_{P C} \circ (\sigma_C + \sigma_C)$. Thus we have a counit
which leads to $\nabla_C \nabla_C^o \leq \sigma_C^o \sigma_C = 1$. On the other hand, $\nabla_C$ retracts the map $i_1: C \to C + C$, and so
using the counit $i_1 i_1^o \leq 1$. Thus $1_C = \nabla_C \nabla_C^o$.
The arrow $\bot \coloneqq !_D \circ !_C^o: C \to D$ is the bottom element of the poset $\mathbf{B}(C, D)$.
Since $!_D: 0 \to D$ is a map, we have a counit $!_D !_D^o \leq 1_D$. Hence $!_D !_D^o S \leq S$ for any $S \in \mathbf{B}(C, D)$. But $!_D^o S = !_C^o: C \to 0$ because $0$ is terminal. Hence $!_D !_C^o \leq S$.
The poset $\mathbf{B}(C, D)$ admits binary joins: given $R, S: C \to D$, the composite
is the join of $R$ and $S$.
For now we give a sketch. It is clear that $R \vee -: \mathbf{B}(C, D) \to \mathbf{B}(C, D)$ is a poset morphism, as is $- \vee S$. One checks that $R \vee \bot = R$ and $\bot \vee S = S$, so we have $R = R \vee \bot \leq R \vee S$ and $S = \bot \vee S \leq R \vee S$. Next, for any $T: C \to D$ we have $T \vee T = T$ as may be seen from the diagram
where the commutativity of the triangle is Lemma 6. Thus if $R \leq T$ and $S \leq T$, we have $R \vee S \leq T \vee T = T$. This completes the proof.
If $R: P C \to P C$ is an arrow such that $\ni_C R \leq \ni_C$, then $1_{P C} \vee R$ also satisfies $\ni_C (1 \vee R) \leq \ni_C$.
We have a commutative diagram
which shows that $\ni_C (1 \vee R) = \ni_C \vee \ni_C R = \ni_C$, as desired.
A power allegory with coproducts is a division allegory.
First we establish the residuation, i.e. the division operations $/$ and $\backslash$. According to Proposition 1, we need only exhibit $\ni_C \backslash \ni_C$, which we claim is $[\Leftarrow] = \ni_{P C} \bigcup_C^o$. That is, we need only show that for $R: P C \to P C$, we have $\ni_C R \leq \ni_C$ if and only if $R \leq [\Leftarrow]$. The βifβ follows from Proposition 3. For the only if, use the fact that $\ni_C R \leq \ni_C$ implies $\ni_C (1 \vee R) \leq \ni_C$ by Lemma 8, and since $1 \vee R$ is reflexive, we have $1 \vee R \leq [\Leftarrow]$ by Proposition 4, whence $R \leq 1 \vee R \leq [\Leftarrow]$ as desired.
We have seen that $\mathbf{B}(C, D)$ is a join semi-lattice; the residuation implies that composition on either side preserves joins as well.
The results 2.214-2.216 of Freyd-Scedrov assure us that $\mathbf{B}(C, D)$ is a distributive lattice, that $0 \to C$ and $\nabla: C + C \to C$ are maps, and finally that coproducts are biproducts.
At this point the connection between the Freyd-Scedrov notion of power allegory and the notion adopted here (allegory with coproducts and power objects) is practically an afterthought, but we may as well show that the Freyd-Scedrov axioms on $\ni: i P \to 1$ are satisfied. (Hmmβ¦)
If the power allegory $\mathbf{B}$ is a bicategory of relations, then $P(B \times C)$ is an exponential $P(C)^B$ in $Map(\mathbf{B})$ for all objects $B, C$. In particular, $P(B) \cong P(1)^B$ for all $B$.
There are natural isomorphisms
whence $P(B \times C)$ satisfies the universal property that characterizes an exponential $P(C)^B$ in $Map(\mathbf{B})$.