Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI made some edits at [[classifying topos]] to correct what I thought were some inaccuracies. One is that simplicial sets classify [[interval objects]], but offhand I didn't see the exact notion of linear interval over at [[interval object]] that would make this a correct sentence. In any event, I went ahead and defined the notion of linear interval as a model of a specified geometric theory. The other is for local rings. I think when algebraic geometers refer to a sheaf of local rings, they refer to a sheaf of rings over a (sober) space all of whose stalks are local. I wasn't sure that description would be kosher for a general (Grothendieck) topos $E$ since there may not be any "stalks" (i.e., points $Set \to E$) to refer to. In any case, it seems to me safer to give the geometric theory directly.

   I made some edits at classifying topos to correct what I thought were some inaccuracies. One is that simplicial sets classify interval objects, but offhand I didn’t see the exact notion of linear interval over at interval object that would make this a correct sentence. In any event, I went ahead and defined the notion of linear interval as a model of a specified geometric theory.

   The other is for local rings. I think when algebraic geometers refer to a sheaf of local rings, they refer to a sheaf of rings over a (sober) space all of whose stalks are local. I wasn’t sure that description would be kosher for a general (Grothendieck) topos $E$ since there may not be any “stalks” (i.e., points $Set \to E$) to refer to. In any case, it seems to me safer to give the geometric theory directly.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks! That laziness about intervals bothered me too, but I was too lazy to unlazify it. I think Joyal (?) sometimes calls these "strict intervals", to indicate that top and bottom are distinct. I also agree that it's certainly not kosher to define anything stalkwise over a topos without enough points. Perhaps the geometric theory should also be mentioned at [[locally ringed topos]]?

   Thanks! That laziness about intervals bothered me too, but I was too lazy to unlazify it. I think Joyal (?) sometimes calls these “strict intervals”, to indicate that top and bottom are distinct.

   I also agree that it’s certainly not kosher to define anything stalkwise over a topos without enough points. Perhaps the geometric theory should also be mentioned at locally ringed topos?

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks! I added the remark about strict intervals (a little rashly now that I look back, since you put a question mark by Joyal), and mentioned that the non-strict ones are classified by presheaves on the augmented simplex category. On your recommendation, I also added a geometric theory-style definition to [[locally ringed topos]].

   Thanks! I added the remark about strict intervals (a little rashly now that I look back, since you put a question mark by Joyal), and mentioned that the non-strict ones are classified by presheaves on the augmented simplex category. On your recommendation, I also added a geometric theory-style definition to locally ringed topos.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexNotice that we do have an entry _[[interval]]_, which does describe the poset-intervals needed here. It appears at _[[interval object]]_ only under "related concepts", though. It would be good to somehow clarify the relation between these entries further, or else otherwise harmonize them.

   Notice that we do have an entry interval, which does describe the poset-intervals needed here.

   It appears at interval object only under “related concepts”, though. It would be good to somehow clarify the relation between these entries further, or else otherwise harmonize them.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexUrs, your first sentence is true, but the strictness assumption is missing (and of course there is a linearity assumption as well). Because there are classically equivalent formulations which become inequivalent when interpreted in a general topos, I think it's best not to leave anything to chance, and spell everything out carefully at [[classifying topos]].

   Urs, your first sentence is true, but the strictness assumption is missing (and of course there is a linearity assumption as well). Because there are classically equivalent formulations which become inequivalent when interpreted in a general topos, I think it’s best not to leave anything to chance, and spell everything out carefully at classifying topos.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexSure, I didn't imply anything else.

   Sure, I didn’t imply anything else.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI didn't know that fact about non-strict intervals and the augmented simplex category. Where is a reference?

   I didn’t know that fact about non-strict intervals and the augmented simplex category. Where is a reference?

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 23rd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexIf it's not in Mac Lane and Moerdijk (and I don't know, because my copy went AWOL), then I don't know where. Actually, I said it a bit offhandedly -- let me see if it's actually true! The idea of course is that the schizophrenic or ambimorphic adjunction induced by the 2-element set in different guises, which is familiar in the form of an adjoint equivalence $$\Delta^{op} \simeq StrictFinInterval$$ extends to an equivalence $\Delta_{a}^{op} \simeq FinInterval$. Then, for a topos $E$, a general (non-strict) interval corresponds to a filtered colimit of representables of finite intervals, $$FinInterval^{op} \stackrel{\hom(-, [n])}{\to} Set \stackrel{\Delta}{\to} E$$ (again, just as in the strict interval case), which corresponds to a left exact left adjoint $$Set^{\Delta_{a}^{op}} \simeq Set^{FinInterval} \to E$$ as required.

   If it’s not in Mac Lane and Moerdijk (and I don’t know, because my copy went AWOL), then I don’t know where. Actually, I said it a bit offhandedly – let me see if it’s actually true! The idea of course is that the schizophrenic or ambimorphic adjunction induced by the 2-element set in different guises, which is familiar in the form of an adjoint equivalence

   $$\Delta^{op} \simeq StrictFinInterval$$

   extends to an equivalence $\Delta_{a}^{op} \simeq FinInterval$. Then, for a topos $E$, a general (non-strict) interval corresponds to a filtered colimit of representables of finite intervals,

   $$FinInterval^{op} \stackrel{\hom(-, [n])}{\to} Set \stackrel{\Delta}{\to} E$$

   (again, just as in the strict interval case), which corresponds to a left exact left adjoint

   $$Set^{\Delta_{a}^{op}} \simeq Set^{FinInterval} \to E$$

   as required.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe proof in ML&M is very concrete and not very conceptual. If you know a nice conceptual proof, it would be a service to have it on the nLab! My intuition is certainly something along the lines of the fact that diagrams on the category of finitely presented models of a theory classify models of that theory, but that precise theorem is only true for finite-limit theories, which doesn't include (even non-strict) intervals. Is the central fact that makes it still work the one you mentioned above, that a general interval is still a filtered colimit of finite(ly presented) ones? That seems offhand like it should be true for models of all finitary theories, since the category of such models ought to be finitely accessible. Maybe I'm just confused....

   The proof in ML&M is very concrete and not very conceptual. If you know a nice conceptual proof, it would be a service to have it on the nLab! My intuition is certainly something along the lines of the fact that diagrams on the category of finitely presented models of a theory classify models of that theory, but that precise theorem is only true for finite-limit theories, which doesn’t include (even non-strict) intervals. Is the central fact that makes it still work the one you mentioned above, that a general interval is still a filtered colimit of finite(ly presented) ones? That seems offhand like it should be true for models of all finitary theories, since the category of such models ought to be finitely accessible. Maybe I’m just confused….

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike, maybe I'm confused myself. In fact I found myself getting confused trying to understand the scope of 'finitary theory' here, and reading Makkai-Paré's book wasn't helping me out of this confusion... on page 58 they write, "Let us call a category **elementary** if it is equivalent to $Mod(\mathcal{S})$ for a coherent sketch $\mathcal{S}$ (see Section 3.1). The term "elementary" is suggested by the established term "elementary class" in model theory. _An elementary class is the class of all models of a small set of axioms in first order logic_ [my emphasis]. By what we said in the previous sections, the elementary classes are precisely the same as the object-classes of categories of the form $Mod(\mathcal{S})$ for coherent sketches $\mathcal{S}$." What confuses me is this unrestricted "small set of axioms in first order logic", whereas coherent logic puts restrictions on the formulas. I wasn't sure what sorts of logical restrictions you had in mind, if any. Anyway, let me step back and say what I was probably unconsciously thinking in #8, which was something of a sledgehammer approach. A _coherent_ theory (like the theory of linear intervals or of strict linear intervals) should be uniquely determined from its models in $Set$, by Deligne's theorem. Therefore (I want to conclude), to check that $Set^{C^{op}}$ is a classifying topos for a coherent theory $T$, it's enough to test this in $Set$, i.e., establish that $T$-models in $Set$ are equivalent to flat functors $C \to Set$ -- this special case would ensure the general case for any topos in place of $Set$. Assuming this meta-principle, here's roughly how I'd argue that augmented simplicial sets classify (non-strict) linear intervals. Given a filtered diagram of representables $$J \stackrel{F}{\to} FinInterval \stackrel{yoneda}{\to} Set^{\Delta_a}$$ let $I$ be the filtered colimit of $J \stackrel{F}{\to} FinInterval \stackrel{i}{\hookrightarrow} Interval$. Then I want to claim that $Interval(i-, I)$ is the colimit of the first filtered diagram. But that's obvious, because finite intervals $[n]$ are finitely presentable in $Interval$, so $$Interval(i [n], I) = Interval(i [n], colim i \circ F) \cong colim Interval(i [n], i \circ F) \cong colim FinInterval([n], F)$$ naturally in $[n]$, in other words $Interval(i-, I) \cong colim (yoneda \circ F)$. Then, because finite intervals are dense in all intervals, we conclude that the category of intervals is equivalent to the category of flat functors $\Delta_a \to Set$. This sounds just like what you were suggesting when you mentioned the category of models being finitely accessible.

    Mike, maybe I’m confused myself. In fact I found myself getting confused trying to understand the scope of ’finitary theory’ here, and reading Makkai-Paré’s book wasn’t helping me out of this confusion… on page 58 they write, “Let us call a category elementary if it is equivalent to $Mod(\mathcal{S})$ for a coherent sketch $\mathcal{S}$ (see Section 3.1). The term “elementary” is suggested by the established term “elementary class” in model theory. An elementary class is the class of all models of a small set of axioms in first order logic [my emphasis]. By what we said in the previous sections, the elementary classes are precisely the same as the object-classes of categories of the form $Mod(\mathcal{S})$ for coherent sketches $\mathcal{S}$.”

    What confuses me is this unrestricted “small set of axioms in first order logic”, whereas coherent logic puts restrictions on the formulas. I wasn’t sure what sorts of logical restrictions you had in mind, if any.

    Anyway, let me step back and say what I was probably unconsciously thinking in #8, which was something of a sledgehammer approach. A coherent theory (like the theory of linear intervals or of strict linear intervals) should be uniquely determined from its models in $Set$, by Deligne’s theorem. Therefore (I want to conclude), to check that $Set^{C^{op}}$ is a classifying topos for a coherent theory $T$, it’s enough to test this in $Set$, i.e., establish that $T$-models in $Set$ are equivalent to flat functors $C \to Set$ – this special case would ensure the general case for any topos in place of $Set$.

    Assuming this meta-principle, here’s roughly how I’d argue that augmented simplicial sets classify (non-strict) linear intervals. Given a filtered diagram of representables

    $$J \stackrel{F}{\to} FinInterval \stackrel{yoneda}{\to} Set^{\Delta_a}$$

    let $I$ be the filtered colimit of $J \stackrel{F}{\to} FinInterval \stackrel{i}{\hookrightarrow} Interval$. Then I want to claim that $Interval(i-, I)$ is the colimit of the first filtered diagram. But that’s obvious, because finite intervals $[n]$ are finitely presentable in $Interval$, so

    $$Interval(i [n], I) = Interval(i [n], colim i \circ F) \cong colim Interval(i [n], i \circ F) \cong colim FinInterval([n], F)$$

    naturally in $[n]$, in other words $Interval(i-, I) \cong colim (yoneda \circ F)$. Then, because finite intervals are dense in all intervals, we conclude that the category of intervals is equivalent to the category of flat functors $\Delta_a \to Set$.

    This sounds just like what you were suggesting when you mentioned the category of models being finitely accessible.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJan 26th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhen I wrote "finitary" I giess I was really thinking of "coherent". But I think what Makkai and Pare have in mind is their Prop. 3.2.8 which shows that any first-order theory is equivalent *over classical logic* to a coherent one. In the Elephant (D1.5.13) this is called *Morleyization*. Let me think a bit about the rest of your comment.

    When I wrote “finitary” I giess I was really thinking of “coherent”. But I think what Makkai and Pare have in mind is their Prop. 3.2.8 which shows that any first-order theory is equivalent over classical logic to a coherent one. In the Elephant (D1.5.13) this is called Morleyization.

    Let me think a bit about the rest of your comment.

12. • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2012
    • (edited Jan 26th 2012)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike #11: ohhh!!! I think I remember seeing it in the Elephant before, and thinking to myself, "so this is the precise technical sense in which people say Deligne's theorem is equivalent to the Gödel completeness theorem for first-order logic." And then forgot about it, or at least the result didn't hit me with force until now.

    Mike #11: ohhh!!! I think I remember seeing it in the Elephant before, and thinking to myself, “so this is the precise technical sense in which people say Deligne’s theorem is equivalent to the Gödel completeness theorem for first-order logic.” And then forgot about it, or at least the result didn’t hit me with force until now.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 26th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWe should record that somewhere on the nLab.

    We should record that somewhere on the nLab.

14. • CommentRowNumber14.
    • CommentAuthorZhen Lin
    • CommentTimeJan 27th 2012
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexTodd #12, Mike #13: I've heard that analogy from my lecturer several times... I wish I knew what it meant! (If I had to guess, "enough points" means that truth can be checked at the level of stalks...?)

    Todd #12, Mike #13: I’ve heard that analogy from my lecturer several times… I wish I knew what it meant! (If I had to guess, “enough points” means that truth can be checked at the level of stalks…?)

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJan 27th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> (If I had to guess, "enough points" means that truth can be checked at the level of stalks...? I haven't been following closely, so if your question is about something more arcane than then notion of a topos with enough points, then please ignore the next sentence. But if you are asking for what it means for a topos to have enough points, see def. 2 at [[point of a topos]].

    (If I had to guess, “enough points” means that truth can be checked at the level of stalks…?

    I haven’t been following closely, so if your question is about something more arcane than then notion of a topos with enough points, then please ignore the next sentence.

    But if you are asking for what it means for a topos to have enough points, see def. 2 at point of a topos.

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 27th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexZhen, the result I was actually hoping for in #10, and which may be only loosely associated with "enough points", goes like this: suppose $T$ is a coherent theory, and that $E$ is a Grothendieck topos equipped with a $T$-model, such that the canonical map $$Topos(Set, E) \to Model_T(Set)$$ is an equivalence. Then $E$ is the classifying topos for $T$. In other words, I was hoping for a meta-principle that says, at least for some class of theories or toposes, that as long as you get the right answer in $Set$, you have the correct classifying topos. But something smells pretty fishy about the blunt generality in which I've stated it here, and now I only hope that at least something along these lines is true, but I don't want to guess what the something might be until I think it over more.

    Zhen, the result I was actually hoping for in #10, and which may be only loosely associated with “enough points”, goes like this: suppose $T$ is a coherent theory, and that $E$ is a Grothendieck topos equipped with a $T$-model, such that the canonical map

    $$Topos(Set, E) \to Model_T(Set)$$

    is an equivalence. Then $E$ is the classifying topos for $T$. In other words, I was hoping for a meta-principle that says, at least for some class of theories or toposes, that as long as you get the right answer in $Set$, you have the correct classifying topos. But something smells pretty fishy about the blunt generality in which I’ve stated it here, and now I only hope that at least something along these lines is true, but I don’t want to guess what the something might be until I think it over more.

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 27th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexLet's see. Suppose $E$ is as you suggest, and let $Set[T]$ denote the actual classifying topos of $T$. Then the given $T$-model in $E$ gives us a geometric morphism $E\to Set[T]$, and the hypothesis tells us that $Set$ sees this morphism as an equivalence. On the other hand, the hypothesis that $E$ has enough points tells us that the collection of geometric morphisms $Set\to E$ is jointly co-faithful and co-conservative. We'd like to conclude from these facts that $E\to Set[T]$ is an equivalence, but offhand I don't see how. And actually, aren't there examples of constructively inequivalent coherent theories that are classically equivalent?

    Let’s see. Suppose $E$ is as you suggest, and let $Set[T]$ denote the actual classifying topos of $T$. Then the given $T$-model in $E$ gives us a geometric morphism $E\to Set[T]$, and the hypothesis tells us that $Set$ sees this morphism as an equivalence. On the other hand, the hypothesis that $E$ has enough points tells us that the collection of geometric morphisms $Set\to E$ is jointly co-faithful and co-conservative. We’d like to conclude from these facts that $E\to Set[T]$ is an equivalence, but offhand I don’t see how.

    And actually, aren’t there examples of constructively inequivalent coherent theories that are classically equivalent?

18. • CommentRowNumber18.
    • CommentAuthorZhen Lin
    • CommentTimeJan 28th 2012
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexTodd #16: Ah. That definitely looks like a completeness theorem to me, thanks! Now that I have an idea of what's being discussed, I think this is the relevant claim in Mac Lane and Moerdijk [Ch. X, §7, Cor. 2]: > Let $T$ be a [coherent] theory. A formula $\forall x (\phi (x) \to \psi (x))$ as above holds in all models of $T$ in any topos, iff it holds in all models of $T$ in the topos $\mathbf{Sets}$. (I have replaced their use of "geometric" with "coherent", in line with current practice.) The proof explicitly makes use of Deligne's theorem that the classifying topos of $T$ has enough points because it is a topos over a site of finite type. It appears to me that your principle should follow if one can show that Set is a separator (in the appropriate 2-categorical sense) in the category of toposes with enough points: that is, if we have two non-isomorphic geometric morphisms $f, g : E \to F$ with $f \ncong g$, then there should be a geometric morphism $p : \mathbf{Set} \to E$ such that $f \circ p \ncong g \circ p$. Regrettably I am insufficiently practised in 2-category theory to see how this might be proven...

    Todd #16: Ah. That definitely looks like a completeness theorem to me, thanks! Now that I have an idea of what’s being discussed, I think this is the relevant claim in Mac Lane and Moerdijk [Ch. X, §7, Cor. 2]:

    Let $T$ be a [coherent] theory. A formula $\forall x (\phi (x) \to \psi (x))$ as above holds in all models of $T$ in any topos, iff it holds in all models of $T$ in the topos $\mathbf{Sets}$.

    (I have replaced their use of “geometric” with “coherent”, in line with current practice.) The proof explicitly makes use of Deligne’s theorem that the classifying topos of $T$ has enough points because it is a topos over a site of finite type.

    It appears to me that your principle should follow if one can show that Set is a separator (in the appropriate 2-categorical sense) in the category of toposes with enough points: that is, if we have two non-isomorphic geometric morphisms $f, g : E \to F$ with $f \ncong g$, then there should be a geometric morphism $p : \mathbf{Set} \to E$ such that $f \circ p \ncong g \circ p$. Regrettably I am insufficiently practised in 2-category theory to see how this might be proven…

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 28th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexZhen: how would that imply Todd's principle? If Set were a strong generator, then I would see it.

    Zhen: how would that imply Todd’s principle? If Set were a strong generator, then I would see it.

20. • CommentRowNumber20.
    • CommentAuthorZhen Lin
    • CommentTimeJan 29th 2012
    • (edited Jan 29th 2012)
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexAgh, I must have confused the fact that $1$ separates in $\mathbf{Set}$ with the fact that $1$ represents the forgetful/identity functor, of which the 2-analogue is what we actually want to prove. Sorry!

    Agh, I must have confused the fact that $1$ separates in $\mathbf{Set}$ with the fact that $1$ represents the forgetful/identity functor, of which the 2-analogue is what we actually want to prove. Sorry!

21. • CommentRowNumber21.
    • CommentAuthorZhen Lin
    • CommentTimeJan 31st 2012
    • (edited Jan 31st 2012)
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexI asked Olivia Caramello about this after seminar today and she said that if a geometric morphism $E \to F$ induces an equivalence $\mathrm{Geom}(\mathbf{Set}, E) \simeq \mathrm{Geom}(\mathbf{Set}, F)$, and $E$ and $F$ are _coherent_ toposes, then $E$ and $F$ are indeed equivalent; apparently it's a corollary of the conceptual completeness theorem of Makkai and Reyes.

    I asked Olivia Caramello about this after seminar today and she said that if a geometric morphism $E \to F$ induces an equivalence $\mathrm{Geom}(\mathbf{Set}, E) \simeq \mathrm{Geom}(\mathbf{Set}, F)$, and $E$ and $F$ are coherent toposes, then $E$ and $F$ are indeed equivalent; apparently it’s a corollary of the conceptual completeness theorem of Makkai and Reyes.

22. • CommentRowNumber22.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 31st 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThank you, Zhen! I'd like to think that over a bit before getting back to you.

    Thank you, Zhen! I’d like to think that over a bit before getting back to you.

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 1st 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOh! It's even stated explicitly as D3.5.9 in the Elephant. "Let S and T be coherent theories, and suppose we are given an interpretation of S in T for which the induced functor T-Mod(Set) $\to$ S-Mod(Set) is an equivalence. Then S and T are Morita-equivalent [i.e. their classifying toposes are equivalent]". Now I actually believe that we can prove the theorem about simplicial sets in this way. But I still don't quite follow the argument in #10 — I think I understand up until the sentence "Then, because finite intervals are dense in all intervals, we conclude that the category of intervals is equivalent to the category of flat functors $\Delta_a \to Set$." Can you explain how that sentence follows from the preceeding?

    Oh! It’s even stated explicitly as D3.5.9 in the Elephant. “Let S and T be coherent theories, and suppose we are given an interpretation of S in T for which the induced functor T-Mod(Set) $\to$ S-Mod(Set) is an equivalence. Then S and T are Morita-equivalent [i.e. their classifying toposes are equivalent]”.

    Now I actually believe that we can prove the theorem about simplicial sets in this way. But I still don’t quite follow the argument in #10 — I think I understand up until the sentence “Then, because finite intervals are dense in all intervals, we conclude that the category of intervals is equivalent to the category of flat functors $\Delta_a \to Set$.” Can you explain how that sentence follows from the preceeding?

24. • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 1st 2012
    • (edited Feb 1st 2012)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike, let me back up a bit. I first argued that a flat functor $\Delta_a \to Set$, in other words a functor which arises as a colimit of a filtered diagram $$J \stackrel{F}{\to} FinInterval \stackrel{yoneda}{\to} Set^{\Delta_a},$$ is isomorphic to a functor of the form $Interval(i-, I)$ for some interval $I$. So $Flat(\Delta_a, Set)$ is equivalent to the full subcategory $\mathcal{F}$ of $Set^{\Delta_a}$ consisting of functors of the form $Interval(i-, I)$. Now the functor $$Interval \to \mathcal{F}: I \mapsto \hom(i-, I)$$ is essentially surjective, and full and faithful precisely because $i: FinInterval \hookrightarrow Interval$ is a dense inclusion. Therefore the composite $$Interval \to \mathcal{F} \simeq Flat(\Delta_a, Set)$$ is an equivalence.

    Mike, let me back up a bit. I first argued that a flat functor $\Delta_a \to Set$, in other words a functor which arises as a colimit of a filtered diagram

    $$J \stackrel{F}{\to} FinInterval \stackrel{yoneda}{\to} Set^{\Delta_a},$$

    is isomorphic to a functor of the form $Interval(i-, I)$ for some interval $I$. So $Flat(\Delta_a, Set)$ is equivalent to the full subcategory $\mathcal{F}$ of $Set^{\Delta_a}$ consisting of functors of the form $Interval(i-, I)$. Now the functor

    $$Interval \to \mathcal{F}: I \mapsto \hom(i-, I)$$

    is essentially surjective, and full and faithful precisely because $i: FinInterval \hookrightarrow Interval$ is a dense inclusion. Therefore the composite

    $$Interval \to \mathcal{F} \simeq Flat(\Delta_a, Set)$$

    is an equivalence.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 1st 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, okay, I think I follow. I was forgetting that a functor into Set is flat iff it is a filtered colimit of representables. This seems to work, but I'm still worried because it doesn't seem like you've used anything other than that (1) the theory of intervals is coherent and (2) the category of intervals in Set is finitely accessible. Is is true that the classifying topos of any coherent theory whose category of Set-models is finitely accessible is a presheaf category on its category of finitely presented Set-models? I recalled that not every coherent theory has a finitely accessible category of models, and put a counterexample at [[coherent logic]], but this would still be a (to me) surprisingly widely applicable result.

    Ah, okay, I think I follow. I was forgetting that a functor into Set is flat iff it is a filtered colimit of representables. This seems to work, but I’m still worried because it doesn’t seem like you’ve used anything other than that (1) the theory of intervals is coherent and (2) the category of intervals in Set is finitely accessible. Is is true that the classifying topos of any coherent theory whose category of Set-models is finitely accessible is a presheaf category on its category of finitely presented Set-models?

    I recalled that not every coherent theory has a finitely accessible category of models, and put a counterexample at coherent logic, but this would still be a (to me) surprisingly widely applicable result.