category of ω-sets

 logic
Notation ω−Set\omegaSet Objects pairs (X,RX)(X, R_X) where XX is a set and RX⊆N×XR_X \subseteq \IN \times X is a "realization" relation such that (p2)∗(RX)=X(p_2)_*(R_X) = X Morphisms a morphism (X,RX)→(Y,RY)(X, R_X) \to (Y, R_Y) is a function f:X→Yf : X \to Y such that there exists a realizer tracker compatible with ff: this is a partial recursive function ⌜f⌝:N⇢N\code{f} : \IN \dashrightarrow \IN such that for every (n,x)∈RX(n,x) \in R_X, the value ⌜f⌝(n)\code{f}(n) is defined and (⌜f⌝(n),f(x))∈RY(\code{f}(n),f(x)) \in R_Y Related Set\Set External nLab link
An ω\omega-set represents a mathematical set with computational encodings of its elements; and similarly, a morphism of ω\omega-sets is a mathematical function such that, roughly speaking, there is a computer program which translates encodings in the domain to encodings in the codomain (at least theoretically, if run on a computer with unlimited storage capacity and given an unlimited though finite time to work). In particular, if we consider (n,x)∈RX(n, x) \in R_X roughly to express a notion of nn being a serialization of a valid representation of xx, then:
  • We do not require RXR_X to be total on the first coordinate, i.e. we allow for some natural numbers which are not valid representations of any element of XX.
  • We do not require RXR_X to be the inverse of a partial functional relation, i.e. we allow for some elements of XX to have multiple valid representations.
  • We do not require RXR_X to be a partial functional relation. This allows the category to express notions of "uniform computability", where some pieces of information in the codomain can be derived given only partial information about the value in the domain.
In many of the proofs to follow, we will use the phrase "nn realizes xx" to mean (n,x)∈RX(n, x) \in R_X. Also, we will fix a choice of a total recursive pairing function ⟨−,−⟩:N2→N\langle {-}, {-} \rangle : \IN^2 \to \IN with total recursive inverses p1,p2:N⇉Np_1, p_2 : \IN \rightrightarrows \IN. (Standard examples of such a pairing function include ⟨m,n⟩≔(m+n+12)+m\langle m, n \rangle \coloneqq \binom{m+n+1}{2} + m, or the function interleaving the binary representations of mm and nn.)The forgetful functor U:ω−Set→SetU : \omegaSet \to \Set has a right adjoint ∇:Set→ω−Set\nabla : \Set \to \omegaSet mapping a set XX to the ω\omega-set (X,N×X)(X, \IN \times X). Also, U(∇X)=XU(\nabla X) = X, and it is easy to see that the counit εX:U(∇X)→X\varepsilon_X : U(\nabla X) \to X is the identity function. Therefore, the counit of the adjunction is an isomorphism, so ∇\nabla is fully faithful.

Satisfied properties

Assigned properties

Deduced properties

Unsatisfied properties

Assigned properties

Deduced properties*

*This also uses the deduced satisfied properties.

Unknown properties

There are 4 properties for which the database has no information on whether they are satisfied. Please help us fill in the gaps by contributing to this project.

Special objects

  • terminal object: (1,N×1)(1, \IN \times 1)
  • initial object: (∅,∅)(\varnothing, \varnothing)
  • products: [binary case] The binary product of (X,RX)(X, R_X) and (Y,RY)(Y, R_Y) is X×YX \times Y with realization relation RX×Y≔{(⟨n,m⟩,(x,y))∣(n,x)∈RX∧(m,y)∈RY}.R_{X\times Y} \coloneqq \{ (\langle n, m \rangle, (x, y)) \mid (n, x) \in R_X \land (m, y) \in R_Y \}.
  • coproducts: [binary case] The binary coproduct of (X,RX)(X, R_X) and (Y,RY)(Y, R_Y) is X⊔YX \sqcup Y with realization relation RX⊔Y≔{(2n,x)∣(n,x)∈RX}∪{(2n+1,y)∣(n,y)∈RY}.R_{X\sqcup Y} \coloneqq \{ (2n, x) \mid (n, x) \in R_X \} \cup \{ (2n+1, y) \mid (n, y) \in R_Y \}.

Special morphisms

  • isomorphisms: A morphism f:(X,RX)→(Y,RY)f : (X, R_X) \to (Y, R_Y) is an isomorphism if and only if the underlying function X→YX \to Y is a bijection, and there also exists a partial recursive function ψ:N⇢N\psi : \IN \dashrightarrow \IN such that whenever we have n∈N,x∈Xn\in\IN, x\in X such that nn realizes f(x)∈Yf(x)\in Y, then ψ(n)\psi(n) exists and ψ(n)\psi(n) realizes x∈Xx\in X
  • monomorphisms: Morphisms of ω\omega-sets whose underlying set function is injective
  • epimorphisms: Morphisms of ω\omega-sets whose underlying set function is surjective
  • regular monomorphisms: A morphism f:(X,RX)→(Y,RY)f : (X, R_X) \to (Y, R_Y) is a regular monomorphism if and only if the underlying function X→YX \to Y is injective, and there exists a partial recursive function ψ:N⇢N\psi : \IN \dashrightarrow \IN such that whenever we have n∈Nn\in \IN and x∈Xx\in X such that nn realizes f(x)∈Yf(x) \in Y, then ψ(n)\psi(n) exists and ψ(n)\psi(n) realizes x∈Xx\in X
  • regular epimorphisms: A morphism f:(X,RX)→(Y,RY)f : (X, R_X) \to (Y, R_Y) is a regular epimorphism if and only if there exists a partial recursive function ψ:N⇢N\psi : \IN \dashrightarrow \IN such that whenever we have n∈Nn\in \IN and y∈Yy\in Y such that nn realizes yy, then ψ(n)\psi(n) exists, and there exists x∈Xx\in X such that f(x)=yf(x) = y and ψ(n)\psi(n) realizes xx

Comments

  • Note that the realizer tracker ⌜f⌝\code{f} is not part of the data of a morphism f:(X,RX)→(Y,RY)f : (X, R_X) \to (Y, R_Y); only the existence of at least one realizer tracker is required.