Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 1 of 1
Hi, all.
I am trying to understand the proof of proposition 7.6 in Shulman’s paper https://arxiv.org/pdf/1808.05204.pdf . 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 “”. 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 is , and it can be proved that consider the formula such that is true iff has cardinality and is a well-order on , then there would be a context over a cover which descents to a context over , and the resultant context should consist of a set and a relation on , where has a map to , call it . I think then will be the well-ordered set contains elements, and the whole is the disjoint union of . where is the well-ordered set containing elements. Then we can collect the maximal elements in each such set and obtain a copy of with the order .
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 , there is a notion of the -th Beth number, denoted as . This number itself is a set, so you may think of associate each ordinal with a set.
If , means that is a finite ordinal, that is, a natural number, then the -th Beth number is the power set That is, , , and , etc.
Now consider the notion of the -th Beth number, is defined to be the minimal set such that for every natural number , the set injects to it. We are going construct , 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 , for any , if for every there is an extension of such that , and moreover this extension is unique up to a unique isomorphism of contexts , then there is an extension of in such that for all .
Here the is the “statement” in ” consider the statement that the image of p”. This statement is on the following parameters: 1. The fixed natural number , as in “For x in N, consider…”. 2. the function , 3. the relation , 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 to as a subset of the power set ). 4. the funcion , which injects to .
Intuitively, this relation says that is a set which is fibred over via the projection map , such that the fibre of is , and for each number the fiber of its successor is the power set of the fiber of . (*) Therefore, is the fiber of .
Call the predicate by , we apply replacement of contexts on . Here is , , is , is the list . As suggested by
One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.
By induction on , we prove there exists a context up to unique isomorphism such that . Therefore we can apply replacement. It gives a context where the maps and the relation are in the slice category. In particular, the fibre of the map on the point is the greatest fiber, i.e., the fiber of as in (*) above, of a context satisfying . Therefore, pulling back along the diagonal map just means take out all these sets (infinitely many). All these sets are contained as a subset of , 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”.
1 to 1 of 1