Construction. Product of two pointed posets [dt-000E]

Liam O'Connor

Given two pointed posets $X$ and $Y$ , the product poset $X \times Y$ is ordered as follows: $(x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y'$ Intuitively, this says that "the information content of a pair of values is increased by increasing the information of either or both of its component values".

This product poset is also pointed, with bottom value $\bot _{X \times Y}$ being $(\bot _A, \bot _B)$ .

Construction. Product of two pointed posets [dt-000E]

Definition. Pointed poset [dt-000G]

Construction. Product of two pointed posets [dt-000E]

Example. The domain $\mathbb {B}_\bot \times \mathbb {B}_\bot$ [dt-000F]

Solution.

Solution.

Solution.

Definition. Projection operators for products [dt-0020]

Construction. Product of cpos [dt-0021]

Theorem. Continuity of projection operations [dt-0022]

Definition. The split function [dt-0023]

Theorem. Continuity of split [dt-0024]

Proof.

Definition. The $\mathit {swap}$ function [dt-0025]

Definition. Product of functions [dt-0026]

Exercise. [dt-002G]

Solution.

Pictorial Properties [dt-0027]

Exercise. [dt-0028]

Solution.

Definition. Universal property for cpo products [dt-0029]

Aside. Category theory [dt-002A]

Definition. Category [dm-000G]

Example. The category $\mathbf {Set}$ [dm-000H]

Example. The category $\mathbf {Rel}$ [dm-000I]

Example. The category $\mathbf {Cpo}$ [dt-002B]

Definition. Functor [dm-000J]

Example. The category $\mathbf {Cat}$ [dm-000K]

Commutative diagrams [dm-000L]

Corollary. Derived properties of cpo products [dt-002C]

Exercise. [dt-002I]

Solution.

Isomorphisms for cpo products [dt-002D]

Definition. Cpo isomorphism [dt-002E]

Theorem. Commutative monoid structure for cpos [dt-002H]

Proof.

Definition. The set of continuous functions [dt-002F]

Theorem. [dt-002J]

Proof.

Upshot.

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$