nLab effect algebra of predicates

Redirected from "Borel regulator".

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.