Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorzskoda
    • CommentTimeMay 29th 2012

    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 el\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 el\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 el\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:SetF,G:\mathcal{M}\to Set the natural transformations α:FG\alpha : F\to G are in 1-1 correspondence with functors β:Set\beta : \mathcal{M}\to Set such that β(A)F(A)×G(A)\beta(A) \subset F(A)\times G(A) and β(A)\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 elSet\mathcal{M}_{el}\to Set and natural transformations.

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeMay 29th 2012

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

    • CommentRowNumber3.
    • CommentAuthorzskoda
    • CommentTimeMay 29th 2012
    • (edited May 29th 2012)

    It seems the nnLab 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: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).

    • CommentRowNumber4.
    • CommentAuthorjesse
    • CommentTimeSep 18th 2016
    • (edited Sep 18th 2016)

    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 Def(T)\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 Def(T)\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 Mod(T)Set\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 TT is equivalent to the pretopos of “ultraproduct-preserving” functors Mod(T)Set\mathbf{Mod}(T) \to \mathbf{Set}; taking points of definable sets in models is the prototypical example of such an ultrafunctor, so definable functions XfYX \overset{f}{\to} Y may be identified with the associated “functor of points” MX(M)f(M)Y(M)M \mapsto X(M) \overset{f(M)}{\to} Y(M) on the category of models.

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeSep 19th 2016

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