Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorzskoda
   • CommentTimeMay 29th 2012
   • PermaLink
   Author: zskoda
   Format: MarkdownItexI have recently created an entry [[definable set]]. It is usually defined as an equivalence class of formulas satisfied by the same elements in each [[structure in model theory|structure]] of the first order language (or model for a [[theory]]). But some works recently, like the lectures of [[David Kazhdan]] ([pdf](http://www.ma.huji.ac.il/~kazhdan/Notes/motivic/b.pdf)), take for granted the observation that in fact the relation of equivalence implies that the evaluation of definable sets in a model extends to a functor on the category of models and elementary monomorphismsm, say $\mathcal{M}_{el}$. There are now many other notions in model theory which have 'definable" as a prefix, and they do not fill uniformly in the same pattern. For example, the category of "definable spaces" and "definable continuous maps" is not the same as the functor from $\mathcal{M}_{el}$ to topological spaces and continuous maps, though possibly some examples would probably fit in the latter description. Also some "definable" notions are for a fixed model and not functors on $\mathcal{M}$. Now, Hrushovski in his 2006 work looked at [[definable groupoid]]s, about which I just plan to create an entry. Now I was cautious not to say that it is simply an [[internal groupoid]] in the category of definable sets, as it is at first defined differently. Besides dealing with internal objects in a large functor category, one should possibly make care about this as well, regarding that we are dealing with a setup where one should be maybe careful about tools like large cardinals (what would be the elegant way to do?). But in any case, the first problem (that the definition was not given as a functor) can easily be dealt. So the definition roughly says that one has definable set of objects and of morphisms (just as we wanted), but then the structure maps like target, composition etc. should be definable functions, hence, as relations they are definable subsets of cartesian products, so when presented from $\mathcal{M}_{el}$ as functors into the categories of sets and relations, which are functional in every model. So, now I just checked a very simple fact, specific to the category of sets and functions, that __Proposition.__ Given a small category $\mathcal{M}$ and two functors $F,G:\mathcal{M}\to Set$ the natural transformations $\alpha : F\to G$ are in 1-1 correspondence with functors $\beta : \mathcal{M}\to Set$ such that $\beta(A) \subset F(A)\times G(A)$ and $\beta(A)$ is a functional relation. In other words, functoriality of $\beta$ is the same as $\alpha$ being natural. That is new to me. This immediately implies that the [[definable groupoid]] as in Hrushovski [arxiv/math.LO/0603413](http://arxiv.org/abs/math/0603413) is (up to the delicacies dealing with functor categories) indeed an internal groupoid in the category of functors $\mathcal{M}_{el}\to Set$ and natural transformations.

   I have recently created an entry definable set. It is usually defined as an equivalence class of formulas satisfied by the same elements in each structure of the first order language (or model for a theory). But some works recently, like the lectures of David Kazhdan (pdf), take for granted the observation that in fact the relation of equivalence implies that the evaluation of definable sets in a model extends to a functor on the category of models and elementary monomorphismsm, say $\mathcal{M}_{el}$. There are now many other notions in model theory which have ’definable” as a prefix, and they do not fill uniformly in the same pattern. For example, the category of “definable spaces” and “definable continuous maps” is not the same as the functor from $\mathcal{M}_{el}$ to topological spaces and continuous maps, though possibly some examples would probably fit in the latter description. Also some “definable” notions are for a fixed model and not functors on $\mathcal{M}$.

   Now, Hrushovski in his 2006 work looked at definable groupoids, about which I just plan to create an entry. Now I was cautious not to say that it is simply an internal groupoid in the category of definable sets, as it is at first defined differently. Besides dealing with internal objects in a large functor category, one should possibly make care about this as well, regarding that we are dealing with a setup where one should be maybe careful about tools like large cardinals (what would be the elegant way to do?).

   But in any case, the first problem (that the definition was not given as a functor) can easily be dealt.

   So the definition roughly says that one has definable set of objects and of morphisms (just as we wanted), but then the structure maps like target, composition etc. should be definable functions, hence, as relations they are definable subsets of cartesian products, so when presented from $\mathcal{M}_{el}$ as functors into the categories of sets and relations, which are functional in every model. So, now I just checked a very simple fact, specific to the category of sets and functions, that

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

   In other words, functoriality of $\beta$ is the same as $\alpha$ being natural. That is new to me.

   This immediately implies that the definable groupoid as in Hrushovski arxiv/math.LO/0603413 is (up to the delicacies dealing with functor categories) indeed an internal groupoid in the category of functors $\mathcal{M}_{el}\to Set$ and natural transformations.

2. • CommentRowNumber2.
   • CommentAuthorzskoda
   • CommentTimeMay 29th 2012
   • PermaLink
   Author: zskoda
   Format: MarkdownItexOK, I created [[definable groupoid]], while the proposition and reinterpretation of [[definable function]]s is inserted into [[definable set]] with a proof. Please check.

   OK, I created definable groupoid, while the proposition and reinterpretation of definable functions is inserted into definable set with a proof. Please check.

3. • CommentRowNumber3.
   • CommentAuthorzskoda
   • CommentTimeMay 29th 2012
   • (edited May 29th 2012)
   • PermaLink
   Author: zskoda
   Format: MarkdownItexIt seems the $n$Lab is not accessible so let me record the last version of the proof here. __Proposition.__ Given a small category $\mathcal{M}$ and two functors $F,G:\mathcal{M}\to Set$ the natural transformations $\alpha : F\to G$ are in 1-1 correspondence with functors $\tilde\alpha : \mathcal{M}\to Set$ such that $\tilde\alpha(A) \subset F(A)\times G(A)$ and such that $\tilde\alpha(A)$ is a functional relation. Proof. If $\alpha:F\to G$ is an $Ob(\mathcal{M})$-indexed family with components $\alpha_A: F(A)\to G(A)$ viewed as functional relations $\tilde\alpha_A\subset F(A)\times G(A)$, then the extension to a functor means that there is a (automatically unique) dotted arrow $\tilde\alpha_f$ $$\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 $\tilde\alpha_f$ is known, the functoriality of $\tilde\alpha_{f\circ g} = \tilde\alpha_f\circ\tilde\alpha_g$ comes by uniqueness of $\tilde\alpha_f$ and the functoriality of $F\times G$ which it restricts from). That means that for every $x\in F(A)$ $(x,\alpha_A(x))$ should be sent to $(F(f)(x), G(f)(\alpha_A(x)))$ by $\tilde\alpha_f$, what is a restriction of $F(f)\times G(f)$, but by $\alpha_B$ being _functional_ relation this must be the same as $(F(f)(x), \alpha_B(F(f)(x)))$, i.e. that $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 $L$ (for $T$) are in 1-1 correspondence with natural transformations of __definable sets__ as functors $\mathcal{M}_{el}(L)\to Set$ (resp. $\mathcal{M}_{el}(T)\to Set$).

   It seems the $n$Lab is not accessible so let me record the last version of the proof here.

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

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

   $$\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 $\tilde\alpha_f$ is known, the functoriality of $\tilde\alpha_{f\circ g} = \tilde\alpha_f\circ\tilde\alpha_g$ comes by uniqueness of $\tilde\alpha_f$ and the functoriality of $F\times G$ which it restricts from). That means that for every $x\in F(A)$ $(x,\alpha_A(x))$ should be sent to $(F(f)(x), G(f)(\alpha_A(x)))$ by $\tilde\alpha_f$, what is a restriction of $F(f)\times G(f)$, but by $\alpha_B$ being functional relation this must be the same as $(F(f)(x), \alpha_B(F(f)(x)))$, i.e. that $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 $L$ (for $T$) are in 1-1 correspondence with natural transformations of definable sets as functors $\mathcal{M}_{el}(L)\to Set$ (resp. $\mathcal{M}_{el}(T)\to Set$).

4. • CommentRowNumber4.
   • CommentAuthorjesse
   • CommentTimeSep 18th 2016
   • (edited Sep 18th 2016)
   • PermaLink
   Author: jesse
   Format: MarkdownItexHello Zoran! Everywhere I look on the nLab for model-theoretic things it seems you've preceded me :p I've expanded the page at [[definable groupoid]]. I've included in the Remarks section some stuff I've worked out in some personal notes but which I'm pretty sure are folklore: having definable Skolem functions is the external axiom of choice for $\mathbf{Def}(T)$, and so this happens precisely when all definable fully faithful essentially surjective functors between definable categories can be upgraded to a full equivalence of categories; also, that Freyd's general adjoint functor theorem internalizes to $\mathbf{Def}(T)$ without a problem as long as you have something to pick out the initial objects of comma categories. I've also added a remark on this business of identifying definable sets as functors $\mathbf{Mod}(T) \to \mathbf{Set}$, which would seem to be given by [[Makkai duality]] (which I still have to write up; I also still need to sit down and carefully work through his rather involved definitions of ultra(categories, functors, morphisms)): the [[syntactic category]] of a first-order theory $T$ is equivalent to the pretopos of "ultraproduct-preserving" functors $\mathbf{Mod}(T) \to \mathbf{Set}$; taking points of definable sets in models is the prototypical example of such an ultrafunctor, so definable functions $X \overset{f}{\to} Y$ may be identified with the associated "functor of points" $M \mapsto X(M) \overset{f(M)}{\to} Y(M)$ on the category of models.

   Hello Zoran! Everywhere I look on the nLab for model-theoretic things it seems you’ve preceded me :p

   I’ve expanded the page at definable groupoid. I’ve included in the Remarks section some stuff I’ve worked out in some personal notes but which I’m pretty sure are folklore: having definable Skolem functions is the external axiom of choice for $\mathbf{Def}(T)$, and so this happens precisely when all definable fully faithful essentially surjective functors between definable categories can be upgraded to a full equivalence of categories; also, that Freyd’s general adjoint functor theorem internalizes to $\mathbf{Def}(T)$ without a problem as long as you have something to pick out the initial objects of comma categories.

   I’ve also added a remark on this business of identifying definable sets as functors $\mathbf{Mod}(T) \to \mathbf{Set}$, which would seem to be given by Makkai duality (which I still have to write up; I also still need to sit down and carefully work through his rather involved definitions of ultra(categories, functors, morphisms)): the syntactic category of a first-order theory $T$ is equivalent to the pretopos of “ultraproduct-preserving” functors $\mathbf{Mod}(T) \to \mathbf{Set}$; taking points of definable sets in models is the prototypical example of such an ultrafunctor, so definable functions $X \overset{f}{\to} Y$ may be identified with the associated “functor of points” $M \mapsto X(M) \overset{f(M)}{\to} Y(M)$ on the category of models.

5. • CommentRowNumber5.
   • CommentAuthorzskoda
   • CommentTimeSep 19th 2016
   • PermaLink
   Author: zskoda
   Format: MarkdownItexThanks for warming us back to the subject and adding precise details :)

   Thanks for warming us back to the subject and adding precise details :)