Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
grothendieck_universe [2014/12/07 22:33]
nikolaj
grothendieck_universe [2015/08/24 19:32]
nikolaj
Line 5: Line 5:
 | @#FFFDDD: forall ​     | @#FFFDDD: $X\in{\mathfrak G}$ | | @#FFFDDD: forall ​     | @#FFFDDD: $X\in{\mathfrak G}$ |
 | @#55EE55: postulate ​  | @#55EE55: $\mathcal{P}(X) \subseteq{\mathfrak G}$ | | @#55EE55: postulate ​  | @#55EE55: $\mathcal{P}(X) \subseteq{\mathfrak G}$ |
 +| @#FFFDDD: forall ​     | @#FFFDDD: $x\in X$ |
 +| @#55EE55: postulate ​  | @#55EE55: $x\in{\mathfrak G}$ |
 | @#FFFDDD: exists ​     | @#FFFDDD: $P\in{\mathfrak G}$ | | @#FFFDDD: exists ​     | @#FFFDDD: $P\in{\mathfrak G}$ |
 | @#55EE55: postulate ​  | @#55EE55: $\mathcal{P}(X) \subseteq P$ | | @#55EE55: postulate ​  | @#55EE55: $\mathcal{P}(X) \subseteq P$ |
Line 10: Line 12:
 | @#55EE55: postulate ​  | @#55EE55: $Y \subseteq {\mathfrak G} \implies Y\ {\approx}\ {\mathfrak G}\lor Y \in {\mathfrak G} $ | | @#55EE55: postulate ​  | @#55EE55: $Y \subseteq {\mathfrak G} \implies Y\ {\approx}\ {\mathfrak G}\lor Y \in {\mathfrak G} $ |
  
-==== Discussion ​==== +----- 
-=== Formalities ​===+=== Discussion === 
 +== Formalities ==
 The symbol ${\approx}$ in the last postulate is an abbreviation. For subsets $Y$ of ${\mathfrak G}$, equinumerosity can be defined as the existence of a set of pairs, $f=\{\{y,​u\},​\{y',​u'​\},​\dots\}$,​ which puts elements $y\in Y$ uniquely in correspondence with $u\in{\mathfrak G}$: The symbol ${\approx}$ in the last postulate is an abbreviation. For subsets $Y$ of ${\mathfrak G}$, equinumerosity can be defined as the existence of a set of pairs, $f=\{\{y,​u\},​\{y',​u'​\},​\dots\}$,​ which puts elements $y\in Y$ uniquely in correspondence with $u\in{\mathfrak G}$:
  
->I reverse-engineered this from the metamath page, so it needs to be checked.+>I reverse-engineered this from the metamath page, so it needs to be checked
  
 $Y\ {\approx}\ {\mathfrak G}\equiv\exists f. \forall x.\left((x \in Y) \implies \exists!u.\ \{x, u\} \in f\right) \land \left((x \in {\mathfrak G}\setminus Y) \implies \exists(y \in Y).\ \{y,x\} \in f\right)$ $Y\ {\approx}\ {\mathfrak G}\equiv\exists f. \forall x.\left((x \in Y) \implies \exists!u.\ \{x, u\} \in f\right) \land \left((x \in {\mathfrak G}\setminus Y) \implies \exists(y \in Y).\ \{y,x\} \in f\right)$
  
 The first clause says $f$ corresponds to a function $F$ and moreover implies $F(b) \in Y \implies F(F(b))=b$. The second says $F$ is surjective into ${\mathfrak G}\setminus Y$. The first clause says $f$ corresponds to a function $F$ and moreover implies $F(b) \in Y \implies F(F(b))=b$. The second says $F$ is surjective into ${\mathfrak G}\setminus Y$.
 +
 +>​strangely,​ to me, the metamath defintion doesn'​t include transitivity in an obvious way, and I can't see it... I added it here anyway, since it's part of any other definition I've seen.
  
 === Reference === === Reference ===
Line 29: Line 34:
 [[http://​us.metamath.org/​mpeuni/​grothprim.html|grothprim]] (long), [[http://​us.metamath.org/​mpeuni/​grothprim.html|grothprim]] (long),
 [[http://​us.metamath.org/​mpeuni/​axgroth5.html|axgroth5]] (the one above) [[http://​us.metamath.org/​mpeuni/​axgroth5.html|axgroth5]] (the one above)
-==== Parents ====+ 
 +nLab:  
 +[[http://​ncatlab.org/​nlab/​show/​Grothendieck+universe|Grothendieck universe]] 
 + 
 +-----
 === Requirements === === Requirements ===
 [[Bijective function]], [[Power set]] [[Bijective function]], [[Power set]]
Link to graph
Log In
Improvements of the human condition