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 “lt”. 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 [A,R:A↬A], and it can be proved that consider the formula ϕ such that ϕ(N,n,A,R:A↬A) is true iff A has cardinality n and R is a well-order on A, then there would be a context over a cover p:V→N which descents to a context over N, and the resultant context should consist of a set ˜A and a relation on ˜A, where ˜A has a map to N, call it q. I think then q−1(n) will be the well-ordered set contains n elements, and the whole ˜A is the disjoint union of A0,⋯,An,⋯. where An is the well-ordered set containing n elements. Then we can collect the maximal elements in each such set and obtain a copy of N 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, , ℶ1=PN, ℶ2=PPN and ℶ3=PPPN, etc.
Now consider the notion of the ω-th Beth number, ℶω is defined to be the minimal set such that for every natural number n, the set ℶn 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 ϕ(U,u:∈U,Θ), for any U, if for every u:∈U there is an extension Θ of (U,u) such that ϕ(U,u,Θ), and moreover this extension Θ is unique up to a unique isomorphism of contexts ΦΘ, then there is an extension Θ0 of (U*U,ΔU) in Set/U such that ϕ(U,u,u*Θ0) for all u:∈U.
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 x, as in “For x in N, consider…”. 2. the function p:X→N, 3. the relation R:X↬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 X to Y as a subset of the power set calP(X×Y)). 4. the funcion z:N→X, which injects N to X.
Intuitively, this relation says that X is a set which is fibred over N via the projection map p:X→N, such that the fibre of 0 is N, and for each number m<n the fiber of its successor m+1 is the power set of the fiber of m. (*) Therefore, ℶn is the fiber of n.
Call the predicate by Upow(n,p:X→N,R:X↬,z:N→X), we apply replacement of contexts on Upow. Here U is N, u∈U, is n∈N, Θ is the list [X,p:X→N,R:X↬X,z:N→X]. As suggested by
One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.
By induction on n∈N, we prove there exists a context [X,p:X→N,R:X↬X,z:N→X] up to unique isomorphism such that Upow(n,p:X→N,R:X↬X,z:N→X). Therefore we can apply replacement. It gives a context Θ0:=[X0(→N),p0:X0→N×N,R0:X0↬X0,z0:BbbN×N→X0] where the maps p0,z0 and the relation z0 are in the slice category. In particular, the fibre of the map p0:X0→N×N on the point (n,n) is the greatest fiber, i.e., the fiber of n as in (*) above, of a context satisfying Upow(n,p:X→N,R:X↬,z:N→X). Therefore, pulling back along the diagonal map just means take out all these sets ℶ1,...,ℶn,ℶn+1,... (infinitely many). All these sets are contained as a subset of X0, 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