nLab
definable set

Contents

Definition

Definability is most often considered only for a first-order language LL (not a theory); a definable set is an equivalence class of formulas which evaluate in the same way in every LL-structure. It makes sense to do the same for a theory: in that case in the definition of the equivalence relation one restricts to models of TT.

Let LL be a first-order language and TT a theory in LL. Any formula ϕ(x 1,,x n)\phi(x_1,\ldots,x_n), whose only free variables could be among x 1,,x nx_1,\ldots,x_n, together with a model MM for TT evaluates to a truth value on each a=(a 1,,a n)M na = (a_1,\ldots,a_n)\in M^n, hence it determines the subset ϕ(M)M n\phi(M)\subset M^n of all aa such that ϕ(a)\phi(a). Two formulas ϕ,ψ\phi,\psi with the same number of free variables are equivalent if ϕ(M)=ψ(M)\phi(M) = \psi(M) for every model MM of TT. A definable set XX in TT is an equivalence class of formulas in LL under this relation. Consider the category el(L)\mathcal{M}_{el}(L) of LL-structures and elementary monomorphism?s and its full subcategory el(T)\mathcal{M}_{el}(T) whose objects are the models of TT. We can also view a definable set for a theory TT as a functor el(T)Set\mathcal{M}_{el}(T)\to Set which is of the form Mϕ(M)M\mapsto\phi(M) for some LL-formula ϕ\phi.

By X(M)X(M) denote the set of all aMa\in M such that X(a)X(a) holds, i.e. ϕ(a)\phi(a) is true for any choice of representative ϕX\phi\in X.

Given two definable sets X,YX,Y in TT a definable function f:XYf: X\to Y is a definable subset of the product sort X×YX\times Y such that f MX(M)×Y(M)f_M\in X(M)\times Y(M) is a function (we also write f M:X(M)Y(M)f_M : X(M)\to Y(M)) for every model MM of TT. Analogously a definable equivalence relation is a definable subset RX×XR\subset X\times X such that R(M)R(M) is an equivalence relation for every model MM of TT.

Properties

Proposition. Given a small category \mathcal{M} and two functors F,G:SetF,G:\mathcal{M}\to Set the natural transformations α:FG\alpha : F\to G are in 1-1 correspondence with functors α˜:Set\tilde\alpha : \mathcal{M}\to Set such that α˜(A)F(A)×G(A)\tilde\alpha(A) \subset F(A)\times G(A) and such that α˜(A)\tilde\alpha(A) is a functional relation.

Proof. If α:FG\alpha:F\to G is an Ob()Ob(\mathcal{M})-indexed family with components α A:F(A)G(A)\alpha_A: F(A)\to G(A) viewed as functional relations α˜ AF(A)×G(A)\tilde\alpha_A\subset F(A)\times G(A), then the extension to a functor means
that there is a (automatically unique) dotted arrow α˜ f\tilde\alpha_f

α˜ A α˜ f α˜ B F(A)×G(A) F(f)×G(f) F(B)×G(B)\array{ \tilde\alpha_A & \stackrel{\tilde\alpha_f}\hookrightarrow & \tilde\alpha_B\\ \downarrow && \downarrow \\ F(A)\times G(A)&\stackrel{F(f)\times G(f)}\longrightarrow & F(B)\times G(B) }

making the diagram commutative (once the existence of α˜ f\tilde\alpha_f is known, the functoriality of α˜ fg=α˜ fα˜ g\tilde\alpha_{f\circ g} = \tilde\alpha_f\circ\tilde\alpha_g comes by uniqueness of α˜ f\tilde\alpha_f and the functoriality of F×GF\times G which it restricts from). That means that for every xF(A)x\in F(A) (x,α A(x))(x,\alpha_A(x)) should be sent to (F(f)(x),G(f)(α A(x)))(F(f)(x), G(f)(\alpha_A(x))) by α˜ f\tilde\alpha_f, what is a restriction of F(f)×G(f)F(f)\times G(f), but by α B\alpha_B being functional relation this must be the same as (F(f)(x),α B(F(f)(x)))(F(f)(x), \alpha_B(F(f)(x))), i.e. that G(f)(α A(x))=α B(F(f)(x))G(f)(\alpha_A(x))=\alpha_B(F(f)(x)). Q.E.D.

In other words, functoriality of α˜\tilde\alpha is the same as α\alpha being natural.

Corollary. Definable functions for LL (for TT) are in 1-1 correspondence with natural transformations of definable sets as functors el(L)Set\mathcal{M}_{el}(L)\to Set (resp. el(T)Set\mathcal{M}_{el}(T)\to Set).

For a fixed (multi-sorted, first-order) theory TT, definable sets and definable functions form a category Def(T)Def(T). This category (or any equivalent category) is the syntactic category of the theory. Models of TT can be recovered as left exact functors Def(T)SetDef(T)\to Set. Notice that definable sets are functors from models to sets, and models are functors definable sets to sets; just the latter are the “evaluation functionals” among all functors.

See also definable groupoid.

An \infty-definable set is an intersection of definable sets.

We can also consider a relative version of a definable set (definability with parameters).

Given definable sets X,YX,Y, a fixed model MM and a fixed set AX(M)A\subset X(M), we say that an element bY(M)b\in Y(M) is definable over AA if there is (a 1,,a n)A n(a_1,\ldots,a_n)\in A^n and a TT-definable function f:X nYf:X^n\to Y such that f(a 1,,a n)=bf(a_1,\ldots,a_n)=b. All elements bb definable over AA form the subset Y(A)Y(M)Y(A)\subset Y(M). A subset BMB\subset M is definably closed if it is closed under definable functions. Given AMA\subset M, there is the minimal definably closed subset BB such that ABMA\subset B\subset M, the definable closure B=dcl(A)B = dcl(A) of AA.

If we extend the language by the constants from AA we get a new language L AL_A. The definable sets in language LL over AA are the definable sets in language L AL_A over \emptyset.

One can also study ind-objects and pro-objects in the category of definable sets and definable functions.

References

  • Moshe Kamensky, Ind- and Pro- definable sets, math.LO/0608163

  • Jan Holly, Definable operations on sets and elimination of imaginaries, Proc. Amer. Math. Soc. 117 (1993), no. 4, 1149–1157, MR93e:03052, doi, pdf

  • David Kazhdan, Lecture notes in model theory, pdf

  • D. Haskell, E. Hrushovski, H.D.Macpherson, Definable sets in algebraically closed valued fields: elimination of imaginaries, J. reine und angewandte Mathematik 597 (2006), MR2007i:03040, doi/CRELLE.2006.066)

Revised on March 26, 2014 03:44:06 by Urs Schreiber (185.37.147.12)