Isomorphisms for cpo products [dt-002D]
DefinitionCpo isomorphism [dt-002E]
An isomorphism between two cpos A and B is a bijection f between A and B such that f preserves the cpo structure, i.e., that f and f^{-1} are continuous.
We say two cpos A and B are isomorphic, written A \simeq B, iff an isomorphism exists between them.
TheoremCommutative monoid structure for cpos [dt-002H]
Cpos form a commutative monoid "up to isomorphism" under \times and \mathbf {1} (the cpo consisting of only one element \bot ). That is, for all cpos A, B and C:
- A \times \mathbf {1} \simeq A
- A \times (B \times C) \simeq (A \times B) \times C
- A \times B \simeq B \times A
Proof.
The isomorphisms required are the projection \pi _0, the \mathit {juggle} function from Exercise [dt-002G], and the swap function.
DefinitionThe set of continuous functions [dt-002F]
Let A \twoheadrightarrow B denote just the continuous functions from cpo A to cpo B: A \twoheadrightarrow B\; \triangleq \; \{ f : A \rightarrow B \mid f\ \text {is continuous} \}
Theorem [dt-002J]
There is an isomorphism between pairs of continuous functions and continuous functions that output pairs: (A \twoheadrightarrow B) \times (A \twoheadrightarrow C)\; \simeq \; (A \twoheadrightarrow (B \times C))
Proof.