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.
    • CommentAuthorUrs
    • CommentTimeMay 30th 2017
    • (edited May 30th 2017)

    I have cross-linked the entries forcing and classifying topos just a tad more by

    1. adding a half-sentence at the end of the paragraph in the Idea-section at “forcing” which mentions the word “classifying topos”

    2. adding to “classifying topos” the references (grabbed from “forcing”) on the relation between the two: here.

    I imagine any categorical logician who would write a pedagogical exposition at forcing on how this concept appears from the point of view of topos theory could have some effect on the community. The issue keeps coming up in discussions I see, and so if we had a point to send people to really learn about the relation (instead of just being bluntly old that there is one) that might have an effect.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 30th 2017

    To what extent can the ’forcing’ of classifying ((,1)(\infty, 1)-)toposes be expressed in HoTT? E.g., when we see here

    the classifying H\mathbf{H}-topos for pointed objects, the result of going to the internal logic of H\mathbf{H} and decreeing

    Let there be a pointed object!

    is this expressible as some kind of declaration of an element of some type?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMay 30th 2017
    • (edited May 30th 2017)

    My understanding is that this is precisely right. The passage of going from an \infty-topos H\mathbf{H} to the \infty-topos

    H[X *][Grpd fin */,H] \mathbf{H}[X_\ast] \coloneqq [\infty Grpd^{\ast/}_{fin}, \mathbf{H}]

    which has a pointed object freely adjoined (namely the 0-sphere S 0Grpd finS^0 \in \infty Grpd_{fin} under the Yoneda embedding) should correspond to adding to the internal language of H\mathbf{H} the axioms

    X:Type e:X. \begin{aligned} & \vdash X \colon Type \\ & \vdash e \colon X \end{aligned} \,.

    This should be just an \infty-version of the story of the univeral property of the syntactic category here, modulo the usual caveats that apparently type theorists forgot to write out the proofs that are needed here to make this fully precise.

    My understanding is that this is what drives for example the idea by Eric Finster et al. on axiomatizing the tangent \infty-topos

    THH[X *]/(ΣΩ(X * S *)X S *) S T \mathbf{H} \simeq \mathbf{H}[X_\ast]/(\Sigma \Omega (X^{S_\ast}_\ast) \to X^{S_\ast}_\bullet)_S

    (see at Characterization via a generic stable object)

    in homotopy type theory by adding the above two axioms plus conditions that make the generic pointed object a stable homotopy type.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMay 30th 2017

    That’s close to right, but there’s a subtlety to remember. The syntactic category of HoTT is (conjecturally) an elementary \infty-topos, whereas the classifying topos of a theory is supposed to be a Grothendieck \infty-topos. Moreover, the former has (conjecturally) a universal property with respect to logical functors, whereas the latter has a universal property with respect to geometric morphisms.

    The precise thing to say is that classifying toposes, in the sense usually understood, only exist for geometric theories: theories presented by axioms that use only the strurcture preserved by inverse image functors of geometric morphisms, i.e. finite limits and arbitrary colimits (including unions of subobjects). The “1-theories” of this sort are geometric logic; probably there is a somewhat more general kind of “geometric \infty-logic”. But an arbitrary set of axioms in HoTT, involving type constructors like Π\Pis, doesn’t have a classifying topos. Moreover, the classifying topos of a geometric theory is not the syntactic category of the dependent type theory containing those axioms; instead we take the syntactic category of the geometric theory containing those axioms, and use it as a site to build a topos of sheaves.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 30th 2017
    • (edited May 30th 2017)

    To come back to #1

    In one such discussion (here), John Baez writes:

    So, I could learn the topos-theoretic approach and read Fourman’s paper to see how it connects to the classical approach. Or, maybe the references you mention work that out. I just don’t want to be trapped in a world where I understand forcing but can only talk about it to topos theorists.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 30th 2017

    Thanks, Mike. Yeah, I am faintly aware of this subtlety. Shouldn’t have said “is precisely”.

    In any case, all the more do I wish somebody would write a useful presentation of these relations.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 31st 2017

    It seems that forcing relations aren’t the only ones between set universes, and that one could go so far as to view the set multiverse as a category

    where all the models of set theory appear as the objects, and all of the known ways that they can relate appear as morphisms, including elementary embeddings, the forcing extension relation, embeddings from one model to an inner model of another, the end-extension relation, and so on.

    Maybe taking on the challenge of making category theoretic sense of some larger picture like this would be profitable. Another job for Jesse :)

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeJun 2nd 2017

    There was a bit of discussion with Lurie here about geometric type theory inspired by the work of Vickers and Maietti. Let’s start simple. Consider Mike’s models of inverse categories. Do they classify what we expect them to classify? Has this even been worked out for Sierpinski space?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2017

    I think it’s pretty easy to see (using facts from HTT) that any (,1)(\infty,1)-topos of presheaves on a 1-category CC classifies flat (,1)(\infty,1)-functors out of CC, which necessarily land inside the 0-truncated objects of any (,1)(\infty,1)-topos.