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.
   • CommentAuthorDavidRoberts
   • CommentTimeJan 21st 2013
   • (edited Jan 21st 2013)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI 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).

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

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeJan 21st 2013
   • (edited Jan 21st 2013)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexOk, 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 21st 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks for cleaning that up!

   Thanks for cleaning that up!

4. • CommentRowNumber4.
   • CommentAuthorStephan A Spahn
   • CommentTimeJan 21st 2013
   • (edited Jan 21st 2013)
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexAt [[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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 21st 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex@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.

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

6. • CommentRowNumber6.
   • CommentAuthorzskoda
   • CommentTimeJan 21st 2013
   • (edited Jan 21st 2013)
   • PermaLink
   Author: zskoda
   Format: MarkdownItexI 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 21st 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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 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?

8. • CommentRowNumber8.
   • CommentAuthorStephan A Spahn
   • CommentTimeJan 21st 2013
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItex@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.

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

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 21st 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexActually, 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).

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

10. • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeJan 21st 2013
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexActually, shouldn't a logical functor preserve and reflect all _higher_ order logic as well? After all, it preserves power objects...

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

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 21st 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexZhen: 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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 22nd 2013
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexMike - 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.

    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.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@Todd: Yes, that's exactly what I had in mind.

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