nLab effect algebra of predicates

Idea

In (Jacobs 12) the approach to categorical logic where the substrate carrying the logical notions are Heyting algebras of subobjects in a topos is replaced by a new one where the substrate is effect algebra of predicates in extensive categories.

Predicates

Let CC be a category with coproducts (written ++). A predicate is a map XpX+XX\stackrel{p}{\to} X+X such that [id X,id X]p=id X[id_X,id_X]\circ p=id_X.

A predicate is hence in particular a coalgebra for the CC-endofunctor XX+XX\mapsto X+X.

If we denote the coproduct inclusions by k 1:XX+Xk_1:X\to X+X and k 2:XX+Xk_2:X\to X+X, then their coproduct [k 2,k 1]:X+XX+X[k_2,k_1]:X+X\to X+X is the swap map (which is a self-inverse equivalence).

For a predicate pp the orthocomplement of pp is defined to be the composite p :=[k 2,k 1]pp^\perp:=[k_2,k_1]\circ p. We have (p ) p(p^\perp)^\perp\simeq p.

Effect algebra of predicates

Lemma

In a extensive category we have the following diagrams involving coproducts and pullbacks:

(…lots of diagrams…)

Corollary

Predicates with the operations defined by (…) assemble to an effect algebra called the effect algebra of predicates.

Examples

Examples

If XSetX\in Set is a set and p:XX+Xp:X\to X+X is a predicate on XX, then p(x)=k 1xp(x)=k_1 x or p(x)=k 2xp(x)=k_2 x.

In particular we can identify pp with a subset U={x|p(x)=k 1x}XU=\{x|p(x)=k_1 x\}\subseteq X. Then ¬U={x|p(x)=k 2x}={x|p (x)=k 1x}\neg U=\{x|p(x)=k_2 x\}=\{x|p^\perp(x)=k_1 x\}

Proof

In SetSet we have disjoint coproducts such that in our case we have

0 X k 2 X k 1 X+X\array{ 0&\to &X\\ \downarrow&&\downarrow^{k_2}\\ X&\stackrel{k_1}{\to}&X+X }

is a pushout square as well as a pullback square. And in SetSet we have universal coproducts such that in our case we have X+XXX+X\simeq X. Now if we assume [id X,id X]pid X[id_X,id_X]\circ p\simeq id_X the couniversal property of the coproduct implies that pp factors through k 1k_1 and k 2k_2 followed by an equivalence.

A category having disjoint- and universal coproducts is called an extensive category.

Further examples are listed at

References

Created on January 8, 2013 at 03:47:33. See the history of this page for a list of all contributions to it.