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.
    • CommentAuthorYimingXu
    • CommentTimeFeb 8th 2023
    • (edited Feb 8th 2023)

    Hi, all.

    I am trying to understand the proof of proposition 7.6 in Shulman’s paper . I am interested in understanding it for applying it within SEAR to obtain interesting constructions (or ETCS, I say SEAR here because it comes with a collection axiom). One point that confuses me is that I am not yet familiar to the notion of stacks. As the claim is that the proof of 7.6 can be carried our within SEAR for each particular case, I think it would be ideal if I can see how the proof of 7.6 expands on particular examples to obtain a proof within SEAR. (Note: I do not think I am confused by how to apply the principle of replacement, I am confused by how its proof works for these particular examples. Say, from the context we can obtain from collection, how can we derive the existence of the context we want by manipulation within these examples without directly appeal to the replacement schema.)

    For the simplest example I can think of, consider we want to build the well-ordered set N without explicitly defining the order “ltlt”. I think we may obtain an isomorphic copy of the well-ordered set N using replacement.

    Let U be N, u be a natural number n in N, we can prove for each n there exists a set A and a relation R on A, such that R is a well order on A. That is, the context Θ\Theta is [A,R:AA][A,R:A\looparrowright A], and it can be proved that consider the formula ϕ\phi such that ϕ(N,n,A,R:AA)\phi(N,n,A,R:A\looparrowright A) is true iff AA has cardinality nn and RR is a well-order on AA, then there would be a context over a cover p:VNp:V \to N which descents to a context over NN, and the resultant context should consist of a set A˜\tilde{A} and a relation on A˜\tilde{A}, where A˜\tilde{A} has a map to NN, call it qq. I think then q 1(n)q^{-1}(n) will be the well-ordered set contains nn elements, and the whole A˜\tilde{A} is the disjoint union of A 0,,A n,A_0,\cdots,A_n,\cdots. where A nA_n is the well-ordered set containing nn elements. Then we can collect the maximal elements in each such set and obtain a copy of NN with the order <\lt.

    This example above is due to myself and I am not sure if I have got it correct, but the following example from Mike Shulman must be correct. It is a bit complicated and let me expand the story in details below.

    For an ordinal α\alpha, there is a notion of the α\alpha-th Beth number, denoted as α\beth_\alpha. This number itself is a set, so you may think of associate each ordinal with a set.

    If α<ω\alpha \lt \omega, means that α\alpha is a finite ordinal, that is, a natural number, then the α\alpha-th Beth number is the power set That is, , 1=PNP^\alpha(\mathbb N\beth_0 =\mathbb N\beth_1= PN, 2=PPN\beth_2 = PPN and 3=PPPN\beth_3 =PPPN, etc.

    Now consider the notion of the ω\omega-th Beth number, ω\beth_\omega is defined to be the minimal set such that for every natural number nn, the set n\beth_n injects to it. We are going construct ω\beth_\omega, and its construction relies on schema of replacement.

    Regarding how to apply the replacement schema (credit to Mike Shulman):

    The way to use replacement of contexts here is something like the following. For simplicity consider the natural numbers N. For x in N, consider the context consisting of a set X, a function p : X -> N, a relation R from X to X, and a function z : N -> X. Depending on x and on this context, consider the statement that the image of p is {y | y <= x}, that z is an isomorphism onto the fiber p^{-1}(0), and that R is the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x. One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic. Therefore, by replacement of contexts, there is a universal such context over N, which in particular has a function p : X -> N x N. Pulling this back along the diagonal map of N, we obtain an N-indexed family of sets that is the sequence of iterated powersets starting with N, and thus its total space is beth_omega.

    Recall the statement of replacement of contexts (from Shulman’s paper):

    for any formula ϕ(U,u:U,Θ)\phi(U, u :\in U, \Theta), for any UU, if for every u:Uu :\in U there is an extension Θ\Theta of (U,u)(U, u) such that ϕ(U,u,Θ)\phi(U, u, \Theta), and moreover this extension Θ\Theta is unique up to a unique isomorphism of contexts Φ Θ\Phi_\Theta, then there is an extension Θ 0\Theta_0 of (U *U,ΔU)(U ^* U,\Delta U ) in Set/USet/U such that ϕ(U,u,u *Θ 0)\phi(U, u , u ^ * \Theta_0 ) for all u:Uu :\in U.

    Here the ϕ\phi is the “statement” in ” consider the statement that the image of p”. This statement is on the following parameters: 1. The fixed natural number xx, as in “For x in N, consider…”. 2. the function p:XNp:X\to N, 3. the relation R:XXR:X\looparrowright X, which is “the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x”. (Union of relations are given by consider a relation from XX to YY as a subset of the power set calP(X×Y){\cal P} (X\times Y)). 4. the funcion z:NXz:N\to X, which injects NN to XX.

    Intuitively, this relation says that XX is a set which is fibred over N N via the projection map p:XNp:X\to N, such that the fibre of 00 is N N, and for each number m<nm\lt n the fiber of its successor m+1m+1 is the power set of the fiber of mm. (*) Therefore, n\beth_n is the fiber of nn.

    Call the predicate by Upow(n,p:XN,R:X,z:NX)Upow(n,p:X\to N,R:X\looparrowright,z:{N}\to X), we apply replacement of contexts on UpowUpow. Here UU is N N, uUu\in U, is nNn\in N, Θ\Theta is the list [X,p:XN,R:XX,z:NX][X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]. As suggested by

    One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.

    By induction on nNn\in N, we prove there exists a context [X,p:XN,R:XX,z:NX][X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X] up to unique isomorphism such that Upow(n,p:XN,R:XX,z:NX)Upow(n,p:X\to N,R:X\looparrowright X,z:{ N}\to X). Therefore we can apply replacement. It gives a context Θ 0:=[X 0(N),p 0:X 0N×N,R 0:X 0X 0,z 0:BbbN×NX 0]\Theta_0:=[X_0(\to N),p_0:X_0\to { N}\times { N}, R_0:X_0\looparrowright X_0,z_0:{\Bbb N}\times {N}\to X_0] where the maps p 0,z 0p_0,z_0 and the relation z 0z_0 are in the slice category. In particular, the fibre of the map p 0:X 0N×Np_0:X_0\to { N}\times { N} on the point (n,n)(n,n) is the greatest fiber, i.e., the fiber of nn as in (*) above, of a context satisfying Upow(n,p:XN,R:X,z:NX)Upow(n,p:X\to N,R:X\looparrowright,z:{ N}\to X). Therefore, pulling back along the diagonal map just means take out all these sets 1,..., n, n+1,...\beth_1,...,\beth_n,\beth_{n+1},... (infinitely many). All these sets are contained as a subset of X 0X_0, so we can take union of them.

    Could someone please explain the proof of 7.6 in Shulman’s paper, in terms of some examples such as the two above, to illustrate how the proofs work? It does not have to be convoluted. I am most confused by the step which uses “Set is a stack of its regular topology”.