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 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 nforum nlab noncommutative noncommutative-geometry number-theory 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 sheaves 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.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 29th 2018
   • (edited Jan 29th 2018)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSteve Awodey gives a nice [account](http://schd.ws/hosted_files/clmps2015/d4/Lambek.pdf) of his passage from Lambek and Moerdijk's work on sheaf representations of toposes to the work with his student Breiner on [[logical schemes]]. From David R. on [g+](https://plus.google.com/+DavidRoberts/posts/6qvkvAihMPh) I hear that Jacob Lurie is running a course on categorical logic right up to Ultracategories and the "Strong Conceptual Completeness" theorem of Makkai. Now Awodey tells us about how in his work with Forssell >"We replace Makkai’s ultraproduct structure on the groupoids of models by a Stone-style logical topology." (Slide 26) This was a step on his way to the work with Breiner who [observes](https://www.andrew.cmu.edu/user/awodey/students/breiner.pdf) >"We reframe Makkai & Reyes’ conceptual completeness theorem as a theorem about schemes...The theorem follows immediately from our scheme construction." Isn't it reasonable to take Awodey's approach as more natural category theoretically? Given we know that this interest of Lurie in [[conceptual completeness]] relates to an $(\infty,1)$-version found in spectral algebraic geometry (see [here](https://mathoverflow.net/questions/226931/variant-of-conceptual-completeness#comment600118_231768)), wouldn't we expect that logical schemes would provide a good basis to construct a logical variant of derived schemes. Should we not be seeing some nice HoTT syntax-semantics dualities emerging? If we can take a pretopos as a first-order theory, what can we say similarly in the case of the $\infty$-pretopoi of A. 9 of [[Spectral Algebraic Geometry]]? Won't they have to be HoTT-like theories (but somehow first-order), which perhaps can be recaptured through some $\infty$-stacks on an $\infty$-groupoid of models? The focus in SAG seems to be on recovering $\infty$-toposes, rather than pretoposes, (Theorem A.9.0.6). Does Makkai-Reyes offer advantages over Awodey-Breiner there?

   Steve Awodey gives a nice account of his passage from Lambek and Moerdijk’s work on sheaf representations of toposes to the work with his student Breiner on logical schemes.

   From David R. on g+ I hear that Jacob Lurie is running a course on categorical logic right up to Ultracategories and the “Strong Conceptual Completeness” theorem of Makkai.

   Now Awodey tells us about how in his work with Forssell

   “We replace Makkai’s ultraproduct structure on the groupoids of models by a Stone-style logical topology.” (Slide 26)

   This was a step on his way to the work with Breiner who observes

   “We reframe Makkai & Reyes’ conceptual completeness theorem as a theorem about schemes…The theorem follows immediately from our scheme construction.”

   Isn’t it reasonable to take Awodey’s approach as more natural category theoretically?

   Given we know that this interest of Lurie in conceptual completeness relates to an $(\infty,1)$-version found in spectral algebraic geometry (see here), wouldn’t we expect that logical schemes would provide a good basis to construct a logical variant of derived schemes.

   Should we not be seeing some nice HoTT syntax-semantics dualities emerging? If we can take a pretopos as a first-order theory, what can we say similarly in the case of the $\infty$-pretopoi of A. 9 of Spectral Algebraic Geometry? Won’t they have to be HoTT-like theories (but somehow first-order), which perhaps can be recaptured through some $\infty$-stacks on an $\infty$-groupoid of models? The focus in SAG seems to be on recovering $\infty$-toposes, rather than pretoposes, (Theorem A.9.0.6). Does Makkai-Reyes offer advantages over Awodey-Breiner there?

2. • CommentRowNumber2.
   • CommentAuthorjesse
   • CommentTimeJan 29th 2018
   • PermaLink
   Author: jesse
   Format: MarkdownItexOne "unnatural" aspect of the Awodey-Forssell duality is that the equivalence between pretoposes and groupoids of models is only gotten by artificially restricting which continuous groupoid homomorphisms are allowed on the groupoid side (if I remember correctly, these are _defined_ to be ones which induce an inverse image functor between the toposes of equivariant sheaves sending coherent objects to coherent objects...) However, ultrafunctors between the ultracategories of models of T' and T correspond to interpretations T to T', full stop. According to Steve, one of the points of Spencer Breiner's thesis was to show that this was a feature instead of a bug: this definition is equivalent to requiring that the continuous groupoid homomorphism induce a map between their notion of structure sheaves. However, I haven't read Spencer's thesis as closely as I've read the Awodey-Forssell paper, so I can't yet give an opinion about that.

   One “unnatural” aspect of the Awodey-Forssell duality is that the equivalence between pretoposes and groupoids of models is only gotten by artificially restricting which continuous groupoid homomorphisms are allowed on the groupoid side (if I remember correctly, these are defined to be ones which induce an inverse image functor between the toposes of equivariant sheaves sending coherent objects to coherent objects…)

   However, ultrafunctors between the ultracategories of models of T’ and T correspond to interpretations T to T’, full stop.

   According to Steve, one of the points of Spencer Breiner’s thesis was to show that this was a feature instead of a bug: this definition is equivalent to requiring that the continuous groupoid homomorphism induce a map between their notion of structure sheaves. However, I haven’t read Spencer’s thesis as closely as I’ve read the Awodey-Forssell paper, so I can’t yet give an opinion about that.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 29th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRight. So that's being pointed out on slide 26 of Steve's [talk](http://schd.ws/hosted_files/clmps2015/d4/Lambek.pdf) and the resolution comes from the structure sheaves, as you say, part of what they call "affine logical schemes" (slide 31). Then Boolean pretoposes and affine logical schemes are contravariantly equivalent.

   Right. So that’s being pointed out on slide 26 of Steve’s talk and the resolution comes from the structure sheaves, as you say, part of what they call “affine logical schemes” (slide 31). Then Boolean pretoposes and affine logical schemes are contravariantly equivalent.