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

]]>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.

]]>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 $Set$ (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 $Set$ (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.

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

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 $Set \to Set^\mathbb{N}/\mathcal{U}$, where the right side indicates a 2-colimit along the filtered system of logical functors $Set/U \to Set/U'$ obtained by pulling back along inclusions $U' \hookrightarrow U$ between subsets $U, U' \subseteq \mathbb{N}$ belonging to an ultrafilter $\mathcal{U}$ on $\mathbb{N}$.

The pullback functor $Set \to Set/U$ is both logical and conservative (isomorphism-reflecting), so the logical functor $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 $Set$. I think Stephan must be wondering about a proposition like $\forall r \in \mathbb{R} \exists n \in \mathbb{N} n \gt r$. My understanding is that this is true in both the models $Set$ and $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).

]]>@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.

]]>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?

]]>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.

]]>@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 $(\mathbb{R}, 0, 1, +, \cdot, \leq)$ are elementarily equivalent.

]]>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.

]]>Thanks for cleaning that up!

]]>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.

]]>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).

]]>