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.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 21st 2013
    • (edited Jan 21st 2013)

    I changed the definition at logical functor, as it said that such a thing was a cartesian functor that preserved power objects. The page cartesian functor says

    A strong monoidal functor between cartesian monoidal categories is called a cartesian functor.

    which really is only about finite products, not finite limits as Johnstone uses, which I guess is where the definition of logical functor was lifted from. So logical functor now uses the condition ’preserves finite limits’.

    So I added a clarifying remark to cartesian functor that the definition there means finite-product-preserving, and that the Elephant uses a different definition.

    However, people may wish to have cartesian functor changed, and logical functor put back how it was. I’m ok with this, but I don’t like the terminology cartesian (and I’m vaguely aware this was debated to some extent on the categories mailing list, so I am happy to go with whatever people feel strongest about).

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 21st 2013
    • (edited Jan 21st 2013)

    Ok, now I decided that I wanted to do what I said in my last paragraph, but now I can’t seem to edit the page cartesian functor: it asks for cookies and javascript to be turned on, but they already are (Chrome 24.0.1312.52 on OSX). I want to say

    A finite limit-preserving functor between finitely complete categories is called a cartesian functor.

    and remove the other additions I made.

    I’ll try later in another browser.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2013

    Thanks for cleaning that up!

    • CommentRowNumber4.
    • CommentAuthorStephan A Spahn
    • CommentTimeJan 21st 2013
    • (edited Jan 21st 2013)

    At logical functor there is the sentence: “For example, the transfer principle of nonstandard analysis can be stated as the fact that a certain functor is logical and conservative.” I don’t know what functor is meant but I would have expected that a theorem in nonstandard analysis need not be valid in standard analysis. But this seems to be what the sentence indicates.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 21st 2013

    @Stephan: one way of formulating a transfer principle for nonstandard analysis is that there is an elementary embedding from the model of standard reals to any nonstandard model. For example, all models of the complete first-order theory of the structure (,0,1,+,,)(\mathbb{R}, 0, 1, +, \cdot, \leq) are elementarily equivalent.

    • CommentRowNumber6.
    • CommentAuthorzskoda
    • CommentTimeJan 21st 2013
    • (edited Jan 21st 2013)

    I think that the basic and the default notion is the cartesian functor between fibered categories. I do not know why a particular case of this construction has come to the forefront place in cartesian functor entry; it is of interest in what I see as a more limited community (almost exclusively in the community of pure category theorists and topos specialists) than the general notion, which is used also in applied areas like algebraic geometry and theoretical computer science, so I would just leave a remark that this is an often used special case, rather than to put it in the first sentence of the idea section. Especially having in mind the subtleties of the two variants of this special case.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2013

    I think we should avoid the terminology ’cartesian functor’ altogether, and say either ’finitely continuous functor’, ’finite-product–preserving functor’, or ’morphism of fibrations’ depending on what we actually mean. Then the page ’cartesian functor’ can just warn the reader that some people use it to mean all of these things.

    @Stephan: I don’t understand, why do you say that?

  1. @Todd: Thanks. This explains why the theorems I had in mind are not reflected - since they are not first-order statements. I think a link from this example to elementary embedding would be good.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 21st 2013

    Actually, let me run this past Mike, since he was the one who wrote the words at logical functor which are worrying Stephan. The logical functor in question might be a filter quotient construction SetSet /𝒰Set \to Set^\mathbb{N}/\mathcal{U}, where the right side indicates a 2-colimit along the filtered system of logical functors Set/USet/USet/U \to Set/U' obtained by pulling back along inclusions UUU' \hookrightarrow U between subsets U,UU, U' \subseteq \mathbb{N} belonging to an ultrafilter 𝒰\mathcal{U} on \mathbb{N}.

    The pullback functor SetSet/USet \to Set/U is both logical and conservative (isomorphism-reflecting), so the logical functor SetSet /𝒰Set \to Set^\mathbb{N}/\mathcal{U} is also logical and conservative. This should mean it preserves truth values of propositions that we can formulate in the internal logic of SetSet. I think Stephan must be wondering about a proposition like rnn>r\forall r \in \mathbb{R} \exists n \in \mathbb{N} n \gt r. My understanding is that this is true in both the models SetSet and Set /𝒰Set^\mathbb{N}/\mathcal{U} – of course, externally speaking, there are more nonstandard integers than standard integers, and this resolves the apparent difficulty (that infinite and infinitesimal reals exist in the latter model, again from the external point of view).

    • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeJan 21st 2013

    Actually, shouldn’t a logical functor preserve and reflect all higher order logic as well? After all, it preserves power objects…

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 21st 2013

    Zhen: yes, absolutely. I think what this means is that there is more than one type of transfer principle – or, that the filter quotient construction produces an ultraproduct of SetSet (regarded as a model of the first-order theory of ETCS, or of ZFC…). If my intuition is correct, then the hyperreals come about by applying the global sections functor to the real number object in this ultraproduct of SetSet (as a model of ETCS) – “global sections” being a way to view the real number object externally.

    There are aspects of this which might cause one to worry, such as the alleged “absoluteness” of the reals from the POV higher order logic, but if my intuition is correct, the resolution pays attention to the background set theory, and the internal/external distinction alluded to above.

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 22nd 2013

    Mike - I agree, but the change I (intended to have) made was the minimal such. I do agree that a beginner shouldn’t have to read three pages filled with terminology that is needless to say not universally adopted and actually conflicting in some sense. I just wanted to make it accurate, to start with.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2013

    @Todd: Yes, that’s exactly what I had in mind.