Todd Trimble Note on power allegories

Redirected from "semi-simplicial types".

Contents

Preliminaries
First results for power objects
Power allegories with sums
Bicategories of relations with power objects

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.

Preliminaries

Lemma

If $r: A \to B$ has a right adjoint $s: B \to A$ in an allegory $\mathcal{A}$ , then $s = r^{op}$ .

Proof

Given $r \dashv s$ , we have $1_A \leq s r$ and $r s \leq 1_B$ . Then

1_A = s r \wedge 1_A \leq (s \wedge 1_A r^{op})r = (s \wedge r^{op})r

by the modular law. Clearly

r(s \wedge r^{op}) \leq r s \leq 1_B

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,

1_A = s r \wedge 1_A \leq s(r \wedge s^{op} 1_A) = s(r \wedge s^{op})

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).

Theorem

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.

Proof

First we show that if $\mathbf{B}$ carries an allegory structure, then it satisfies the Frobenius equations

\delta \delta^{op} = (\delta^{op} \otimes 1)(1 \otimes \delta) = (1 \otimes \delta^{op})(\delta \otimes 1)

(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

(s \wedge r f)f^{op} = s f^{op} \wedge r

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

(s \wedge r f)f^{op} = \sigma_A \delta_A \delta_A^{op}

s f^{op} \wedge r = \sigma_A (\delta_A^{op} \otimes 1_A)(1_A \otimes \delta_A)

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

r^{op} \coloneqq (\eta_B^{op} \otimes 1_A)(1_B \otimes r \otimes 1_A)(1_B \otimes \eta_A) = (1_A \otimes \eta_B^{op})(1_A \otimes r \otimes 1_B)(\eta_A \otimes 1_B).

The point is that any candidate $r^{op}$ for an allegorical structure must be equal to these expressions. We have for example

\array{ (\eta_B^{op} \otimes 1_A)(1_B \otimes r \otimes 1_A)(1_B \otimes \eta_A) & = & (\epsilon_B \otimes 1_A)(\delta_B^{op} \otimes 1_A)(1_B \otimes r \otimes 1_A)(1_B \otimes \eta_A) \\ & \leq & (\epsilon_B \otimes 1_A)(r \otimes 1_A)(\delta_B^{op} \otimes 1_A)(r^{op} \otimes 1_A \otimes 1_A)(1_B \otimes \eta_A) \\ & \leq & (\epsilon_B \otimes 1_A)(\delta_B^{op} \otimes 1_A)(r^{op} \otimes 1_A \otimes 1_A)(1_B \otimes \eta_A) \\ & = & r^{op}(\eta_A^{op} \otimes 1_A)(1_A \otimes \eta_A) \\ & = & r^{op} }

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

\array{ r & = & (1_B \otimes \eta_A^{op})(1_B \otimes \eta_B^{op} \otimes 1_{A \otimes A})(1_{B \otimes B} \otimes r \otimes 1_{A \otimes A})(1_{B \otimes B} \otimes \eta_A \otimes 1_A)(\eta_B \otimes 1_A) \\ & \leq & (1_B \otimes \eta_A^{op})(1_B \otimes r^{op} \otimes 1_A)(\eta_B \otimes 1_A) }

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

r^{op} \leq (1_A \otimes \eta_B^{op})(1_A \otimes r \otimes 1_B)(\eta_A \otimes 1_B).

The same line of argument shows

(1_A \otimes \eta_B^{op})(1_A \otimes r \otimes 1_B)(\eta_A \otimes 1_B) \leq r^{op}

followed by

r^{op} \leq (\eta_B^{op} \otimes 1_A)(1_B \otimes r \otimes 1_A)(1_B \otimes \eta_A),

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.

Theorem

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})$ ).

First results for power objects

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$ ,

$\chi_r \colon A \to P(B)$

denotes the unique map such that $\ni_B \chi_r = r$ . It is also called the classifying map of $r$ .

Definition

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

t \leq r/s \Longleftrightarrow t \leq (s^o\backslash r^o)^o \Longleftrightarrow t^o \leq s^o\backslash r^o \Longleftrightarrow s^o t^o = (t s)^o \leq r^o \Longleftrightarrow t s \leq r.

Proposition

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.

Proof

Since $r = \ni_C \chi_r$ and $s = \ni_C \chi_s$ , we have

\array{ s t \leq r & iff & \ni_C \chi_s t \leq \ni_C \chi_r \\ & iff & \ni_C \chi_s t \chi_r^o \leq \ni_C \\ & iff & \chi_s t \chi_r^o \leq \ni_C \backslash \ni_C \\ & iff & t \leq \chi_s^o (\ni_C \backslash \ni_C) \chi_r }

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

P P(C) \stackrel{\ni_{P(C)}}{\to} P(C) \stackrel{\ni_C}{\to} C.

Define the internal order $[\Rightarrow] \colon P(C) \to P(C)$ by the composite

P(C) \stackrel{\in_{P(C)}}{\to} P P(C) \stackrel{\bigcup_C}{\to} P(C).

Its opposite is $[\Leftarrow] \coloneqq \ni_{P(C)} \bigcup_C^o$ . We will show that under suitable conditions, $[\Leftarrow] = \ni_C \backslash \ni_C$ .

Proposition

$\ni_C [\Leftarrow] \leq \ni_C$ .

Proof

We have a diagram

\array{ P C & \stackrel{\bigcup_C^o}{\to} & P P C & \stackrel{\ni_{P C}}{\to} & P C \\ & \mathllap{1} \searrow \geq & \downarrow \mathrlap{\bigcup_C} & & \downarrow \mathrlap{\ni_C} \\ & & P C & \underset{\ni_C}{\to} & C }

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$ .

Proposition

The internal relation $[\Leftarrow]: P C \to P C$ is reflexive: $1_{P C} \leq [\Leftarrow]$ .

Proof

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.

Proposition

If $R: P C \to P C$ is reflexive, then $\ni_C R \leq \ni_C$ if and only if $R \leq {[\Leftarrow]}$ .

Proof

If $R \leq [\Leftarrow]$ , then $\ni_C R \leq \ni_C [\Leftarrow] \leq \ni_C$ by Proposition . 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.

Proposition

$[\Leftarrow]$ is transitive: $[\Leftarrow] \circ [\Leftarrow] \leq [\Leftarrow]$ .

Proof

By Proposition , $[\Leftarrow] [\Leftarrow]$ is reflexive. So, by Proposition , it suffices to observe that $\ni_C [\Leftarrow] [\Leftarrow] \leq \ni_C$ , but this is immediate from Proposition .

Power allegories with sums

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}$ .

Lemma

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.

Proof

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

!_C !_C^o \leq \sigma_C^o \sigma_C = \ni_C \sigma_C \sigma_C^o \sigma_C = \ni_C \sigma_C = 1

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.

Lemma

The coproduct functor $+: \mathbf{B} \times \mathbf{B} \to \mathbf{B}$ preserves local meets (and in particular is $Pos$ -enriched).

Proof

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

\left( \array{r & 0 \\ 0 & s} \right) + \left( \array{r' & 0 \\ 0 & s'}\right) = \left( \array{r + r' & 0 \\ 0 & s + s'}\right)

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.

Lemma

The coproduct inclusion arrows $i_1, i_2: C \to C + C$ are maps.

Proof

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.

Lemma

The codiagonal $\nabla_{P C}: P C + P C \to P C$ is a map.

Proof

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$ .

Lemma

The codiagonal $\nabla_C: C + C \to C$ satisfies $\nabla_C \nabla_C^o = 1_C$ .

Proof

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

\sigma_C \nabla_C \nabla_C^o \sigma_C^o \leq 1

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

1_C = \nabla_C i_1 i_1^o \nabla_C^o \leq \nabla_C \nabla_C^o

using the counit $i_1 i_1^o \leq 1$ . Thus $1_C = \nabla_C \nabla_C^o$ .

Lemma

The arrow $\bot \coloneqq !_D \circ !_C^o: C \to D$ is the bottom element of the poset $\mathbf{B}(C, D)$ .

Proof

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$ .

Theorem

The poset $\mathbf{B}(C, D)$ admits binary joins: given $R, S: C \to D$ , the composite

R \vee S \coloneqq (C \stackrel{\nabla^o}{\to} C + C \stackrel{R + S}{\to} D + D \stackrel{\nabla}{\to} D)

is the join of $R$ and $S$ .

Proof

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

\array{ C & \stackrel{\nabla^o}{\to} & C + C & \stackrel{T + T}{\to} & D + D \\ & \mathllap{1} \searrow = & \mathllap{\nabla} \downarrow & & \downarrow \mathrlap{\nabla} \\ & & C & \underset{T}{\to} & D }

where the commutativity of the triangle is Lemma . Thus if $R \leq T$ and $S \leq T$ , we have $R \vee S \leq T \vee T = T$ . This completes the proof.

Lemma

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$ .

Proof

We have a commutative diagram

\array{ P C & \stackrel{\nabla^o}{\to} & P C + P C & \stackrel{1 + R}{\to} & P C + P C & \stackrel{\nabla}{\to} & P C \\ & & \mathllap{\ni_C + \ni_C R} \downarrow & & \mathllap{(\ni_C, \ni_C)} \downarrow & \swarrow \mathrlap{\ni_C} \\ & & C + C & \underset{\nabla}{\to} & C }

which shows that $\ni_C (1 \vee R) = \ni_C \vee \ni_C R = \ni_C$ , as desired.

Theorem

A power allegory with coproducts is a division allegory.

Proof

First we establish the residuation, i.e. the division operations $/$ and $\backslash$ . According to Proposition , 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 . 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 , and since $1 \vee R$ is reflexive, we have $1 \vee R \leq [\Leftarrow]$ by Proposition , 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…)

Bicategories of relations with power objects

Proposition

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$ .

Proof

There are natural isomorphisms

\array{ Map(\mathbf{B})(A \times B, P(C)) & \cong & \mathbf{B}(A \times B, C) & \\ & \cong & \mathbf{B}(A, B \times C) & by\; compact\; closure\\ & \cong & Map(\mathbf{B})(A, P(B \times C)) }

whence $P(B \times C)$ satisfies the universal property that characterizes an exponential $P(C)^B$ in $Map(\mathbf{B})$ .

Revised on December 1, 2019 at 19:06:59 by Todd Trimble