Priorities and Comonads

Jason Reed

November 18, 2000

Definition A priority on a category C with finite limits is a pair (P, σ) where P is a lex endofunctor on C and σ is a natural transformation P → P^{2} such that the diagram

P^{3} ^{σ_{P}} P^{2}

(i)

[figure: P^{2}; P σ; σ; P; σ]

commutes, and the diagram

P^{2}(X × Y) ^{σ_{X×Y}} P (X × Y)

P (P X × P Y)^{P q_{XY} }  (ii)

[figure: P^{2}X × P^{2}Y; q_{P X,P Y}; σ_{X} × σ_{Y}; P X × P Y; q_{XY}]

commutes for any objects X, Y of C, where q_{XY} is the canonical natural isomorphism P X × P Y → P (X × Y) induced by P being lex.

Lemma 0.1 Let (P, σ) be a priority on a category C. Then the diagram

[figure: P A; σ_{A}; P^{2}A; P (σ_{A}, 1_{P A}); P T P A; T P A; (σ_{A}, 1_{P A}); q_{P A,A}; P T A; σ_{T A}; P^{2}T A; P q_{P A,A}]

commutes.

Proof We first observe that

(P fst_{T P A})P (σ_{A}, 1_{P A})σ_{A} = P (fst_{T P A}(σ_{A}, 1_{P A}))σ_{A}
= P σ_{A}σ_{A}
= P σ_{A}fst_{T P A}(σ_{A}, 1_{P A})
= fst_{T P^{2}A}(P σ_{A} × σ_{A})(σ_{A}, 1_{P A})
= (P fst_{T P A})q_{P^{2}A,P A}(P σ_{A} × σ_{A})(σ_{A}, 1_{P A})

and

(P snd_{T P A})P (σ_{A}, 1_{P A})σ_{A} = P (snd_{T P A}(σ_{A}, 1_{P A}))σ_{A}
= σ_{A}
= σ_{A}snd_{T P A}(σ_{A}, 1_{P A})
= snd_{T P^{2}A}(P σ_{A} × σ_{A})(σ_{A}, 1_{P A})
= (P snd_{T P A})q_{P^{2}A,P A}(P σ_{A} × σ_{A})(σ_{A}, 1_{P A})

hence (by pairing the two equations) if we set h := (P fst_{T P A}, P snd_{T P A}) we have hP (σ_{A}, 1_{P A})σ_{A} = hq_{P^{2}A,P A}(P σ_{A} ×σ_{A})(σ_{A}, 1_{P A}). But it is easily seen that h = q^{−1}, so h is mono and therefore P (σ_{A}, 1_{P A})σ_{A} = q_{P^{2}A,P A}(P σ_{A} ×σ_{A})(σ_{A}, 1_{P A}). Now if we take the diagram (i) and multiply it with the (trivially commutative) diagram

[figure: P A; 1_{P A}; P A; P A; 1_{P A}; σ_{A}; P^{2}A; σ_{A}]

we obtain

[figure: P A × P A; σ_{A} × P A; T P A; T P A; σ_{A} × P A; P σ_{A} × σ_{A}; T P^{2}A; σ_{P A} × σ_{A}]

and since (σ_{A} × P A)Δ_{P A} = (σ_{A}, 1_{P A}), we have that the diagram

[figure: P A; (σ_{A}, P A); T P A; T P A; (σ_{A}, P A); P σ_{A} × σ_{A}; T P^{2}A; σ_{P A} × σ_{A}]

commutes. Putting all of the above together with diagram (ii) with X := P A and Y := A, we obtain the commutativity of

P A  \overline{σ_{A}} P^{2}A

T P A^{(σ_{A}, 1_{P A})}

[figure: T P A; (σ_{A}, 1_{P A}); σ_{P A} × σ_{A}; T P^{2}A; P σ_{A} × σ_{A}; q_{P^{2}A,P A}; P T P A; P (σ_{A}, 1_{P A})]

[figure: P T A; q_{P A,A}; σ_{T A}; P^{2}T A; P q_{P A,A}]

as required.

Theorem 0.2 Let (P, σ) be a priority on a category C. If we make the definitions

T A := P A × A
ϵ_{A} := snd_{P A×A}
δ_{A} := (q_{P A,A}(σ_{A}, 1_{P A}) × (P A × A))a_{P A,P A,A}(Δ_{P A} × A)

(where Δ_{A} := (1_{A}, 1_{A}) and a_{ABC} is the canonical natural isomorphism (A × B) × C → A × (B × C)) then (T, ϵ, δ) is a comonad.

Proof We easily have that ϵ and δ are natural because ‘everything in sight’ is natural in their definition. To simplify future computations, we define

α_{A} := (q_{P A,A}(σ_{A}, 1_{P A}) × (P A × A))

β_{A} := a_{P A,P A,A}
γ_{A} := Δ_{P A} × A

so that δ = αβγ. It remains to show that the comonad equalities are satisfied. We see first that the diagram

[figure: T A; snd_{T^{2}A}; T^{2}A; T snd_{T A}; T A]

[figure: 1_{T A}; 1_{T A}; (∗)]

T A^{δ_{A} }

commutes, because

snd_{T^{2}A}δ_{A} = snd_{T^{2}A}α_{A}β_{A}γ_{A}
= snd_{P A×(P A×A)}β_{A}γ_{A}
= (fst_{P A×A}snd_{P A×(P A×A)}, snd_{P A×A}snd_{P A×(P A×A)})β_{A}γ_{A}
= (fst_{P A×A}snd_{P A×(P A×A)}β_{A}, snd_{P A×A}snd_{P A×(P A×A)}β_{A})γ_{A}
= (snd_{P A×P A}fst_{(P A×P A)×A}, snd_{(P A×P A)×A})γ_{A}
= (snd_{P A×P A}fst_{(P A×P A)×A}γ_{A}, snd_{(P A×P A)×A}γ_{A})
= (snd_{P A×P A}Δ_{P A}fst_{P A×A}, snd_{P A×A})
= (fst_{P A×A}, snd_{P A×A})
= 1_{P A×A}

and

(T ϵ_{A})δ_{A} = T snd_{T A}α_{A}β_{A}γ_{A}
= (P snd_{T A} × snd_{T A})α_{A}β_{A}γ_{A}
= (P snd_{T A}q_{P A,A}(σ_{A}, 1_{P A}) × snd_{T A})β_{A}γ_{A}
= (snd_{P^{2}A×P A}(σ_{A}, 1_{P A}) × snd_{T A})β_{A}γ_{A}
= (1_{P A} × snd_{T A})β_{A}γ_{A}
= (fst_{P A×(P A×A)}, snd_{P A×A}snd_{P A×(P A×A)})β_{A}γ_{A}
= (fst_{P A×(P A×A)}β_{A}, snd_{P A×A}snd_{P A×(P A×A)}β_{A})γ_{A}
= (fst_{P A×P A}fst_{(P A×P A)×A}, snd_{(P A×P A)×A})γ_{A}
= (fst_{P A×P A}fst_{(P A×P A)×A}γ_{A}, snd_{(P A×P A)×A}γ_{A})
= (fst_{P A×P A}Δ_{P A}fst_{P A×A}, snd_{P A×A})
= (fst_{P A×A}, snd_{P A×A})
= 1_{P A×A}

This immediately provides that ϵ behaves correctly as a counit. Now we want to show that δ_{T} δ = (T δ)δ. If we hit the left triangle of (∗) ‘on the inside’ with T, we see that the following diagram commutes:

T^{2}A ^{snd_{T^{3}A}} T^{3}A

[figure: 1_{T^{2}A}]  (∗∗)

T^{2}A^{δ_{T A} }

We can then verify that snd_{T^{3}}δ_{T A}δ_{A} = snd_{T^{3}}(T δ_{A})δ_{A} by chasing the diagram resulting from pasting together (∗∗) with the left triangle of (∗) and the naturality of snd and 1_{C}:

T A

[figure: δ_{A}; δ_{A}]

[figure: T^{2}A; T A; 1_{T A}; snd_{T^{2}A}; T^{2}A]

[figure: 1_{T^{2}A}]

[figure: T^{3}A; δ_{T A}; snd_{T^{3}A}; T^{2}A; δ_{A}; snd_{T^{3}A}; T^{3}A; T (δ_{A})]

Next we observe that fst_{T^{2}A}δ_{A} = q_{P A,A}(σ_{A}, 1_{P A})fst_{T A}, for the following diagram commutes:

T A  \overline{δ_{A}} T^{2}A

[figure: (P A)^{2} × A; β_{A}; γ_{A}; P A × T A; α_{A}]

[figure: (P A)^{2}; fst_{(P A)^{2}×A}; P T A; fst_{T^{2}A}]

[figure: P A; fst_{T A}; 1_{P A}; Δ_{P A}; P A; fst_{P A×T A}; (σ_{A}, 1_{P A}); _{fst_{(P A)^{2}}}; T P A; q_{P A,A}]

from this we can conclude that the diagram

T^{3}  \overline{^{fst_{T^{3}A}}} P T^{2}A

[figure: T^{2}A; T δ_{A}; _{fst_{T^{2}A}}; P T A; P δ_{A}]

[figure: T P T A; (σ_{T A}, 1_{P T A}); snd_{T P T A}; P T A; P snd_{T^{2}A}; 1_{P T A}]

[figure: T^{3}A; δ_{T A}; fst_{T^{3}A}; P T^{2}A; P snd_{T^{2}A}; q_{P^{2}A,P A}]

commutes. So we know

sndδ_{T} δ = snd(T δ)δ

and

(P snd)fstδ_{T} δ = (P snd)fst(T δ)δ

If we can show (P fst)fstδ_{T} δ = (P fst)fst(T δ)δ, then it follows that δ_{T} δ = (T δ)δ and we are done. To see this, observe that the following two diagrams are commutative, and apply Lemma 0.1.

[figure: T A; δ_{A}; T^{2}A; T δ_{A}; T^{3}A]

[figure: T P A; q_{P A,A}; P T A; fst_{T^{2}A}; P δ_{A}; P T^{2}A; fst_{T^{3}A}]

[figure: P A; fst_{T A}; σ_{A}; (σ_{A}, 1_{P A}); P^{2}A; fst_{T P A}; P (σ_{A}, 1_{P A}); P fst_{T A}; P T P A; P q_{P A,A}; P^{2}T A; P fst_{T^{2}A}]

[figure: T P A; q_{P A,A}; P T A; σ_{T A}; P^{2}T A]

[figure: P A; (σ_{A}, 1_{P A}); T P T A; fst_{T P T A}; q_{P T A,T A}; (σ_{T A}, 1_{P T A}); P T^{2}A; P fst_{T^{2}A}]

[figure: T A; fst_{T A}; δ_{A}; T^{2}A; fst_{T^{2}A}; δ_{T A}; T^{3}A; fst_{T^{3}A}]