-
Notifications
You must be signed in to change notification settings - Fork 56
Dieudonne complete #1426
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Dieudonne complete #1426
Changes from all commits
Commits
Show all changes
39 commits
Select commit
Hold shift + click to select a range
6d9d85e
added completely uniformizable
Moniker1998 13b6476
added
Moniker1998 6e49252
Kelley
Moniker1998 923600b
added Engelking and equivalent definitions
Moniker1998 dcf557b
added another justification to a theorem
Moniker1998 a351154
T386 change
Moniker1998 b868adb
changes to description, theorem to be finished
Moniker1998 fb3f303
proof of T777 updated
Moniker1998 1fe2b16
Update properties/P000221.md
Moniker1998 95c5c37
Apply suggestion from @prabau
Moniker1998 e9168d0
Update P000221.md
Moniker1998 0f93f37
Update P000221.md
Moniker1998 266fc1e
Update T000386.md
Moniker1998 9fd4fe0
add Kolmogorov meta to P22
Moniker1998 fe75d38
add explore link to T777
Moniker1998 cec9bf6
add note to P207
Moniker1998 23ebe1c
added a remark that uniformity induces topology
Moniker1998 f9d4d2c
add explore to T776
Moniker1998 ecb2f1a
Update theorems/T000777.md
Moniker1998 5fd2db6
Cauchy net converges to its adherence points
Moniker1998 b496e50
Update T000777.md
Moniker1998 50036a8
fix a broken file
Moniker1998 3c2a191
T777: remove duplicate text, plus cosmetic changes
prabau 11dd212
fix missing double quotes
prabau 60f4995
Update theorems/T000777.md
Moniker1998 710c326
elaboration on nomenclature
Moniker1998 99ed32e
rephrased equivalent statements to include non-T0 case
Moniker1998 d3b077d
renamed theorems
Moniker1998 d75a5b1
Merge branch 'main' into completely-uniformizable
Moniker1998 7d964f8
doi => zb
felixpernegger f26685d
P63 cosmetic
prabau 9517dd6
P221 updates
prabau ed83bb5
Update properties/P000055.md
Moniker1998 5f9e3d1
T915 cosmetic
prabau d94dcda
Update theorems/T000917.md
Moniker1998 eaffea7
Update theorems/T000917.md
Moniker1998 a95d2c5
Update properties/P000221.md
Moniker1998 09b8ea2
Update theorems/T000916.md
Moniker1998 070ab95
Update theorems/T000386.md
Moniker1998 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,44 @@ | ||
| --- | ||
| uid: P000221 | ||
| name: Dieudonné complete | ||
| aliases: | ||
| - Completely uniformizable | ||
| - Topologically complete | ||
| refs: | ||
| - wikipedia: Completely_uniformizable_space | ||
| name: Completely uniformizable space | ||
| - zb: "1380.46022" | ||
| name: Rings of Continuous Functions (Gillman & Jerison) | ||
| - mr: 370454 | ||
| name: General Topology (Kelley) | ||
| - zb: "0684.54001" | ||
| name: General Topology (Engelking, 1989) | ||
| - zb: "1052.54001" | ||
| name: General Topology (Willard, 1970) | ||
| - zb: "0024.36301" | ||
| name: Sur les espaces uniformes complets (Dieudonné) | ||
| --- | ||
|
|
||
| There exists at least one [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness) | ||
| that induces the topology of $X$. | ||
|
|
||
| This is equivalent to each of the following: | ||
| - $X$ is homeomorphic to a closed subspace of a product of completely pseudometrizable spaces. | ||
| - $X$ is homeomorphic to a closed subspace of a product of {P121} spaces. | ||
|
|
||
| For the equivalence, see Problem 8.5.13(z) in {{zb:0684.54001}} and page 285 of {{zb:0024.36301}}. | ||
|
|
||
| Terminology: | ||
| We call a uniformity $\mathcal{U}$ *complete* if every Cauchy filter $\mathcal{F}$ on $(X, \mathcal{U})$ converges. Equivalently, every Cauchy net $(x_i)_{i\in I}$ on $(X, \mathcal{U})$ converges. Here a *Cauchy filter* is a filter $\mathcal{F}$ such that for every $U\in\mathcal{U}$ there exists $A\in\mathcal{F}$ such that $A\times A\subseteq U$. A *Cauchy net* is a net $(x_i)_{i\in I}$ such that for every $U\in\mathcal{U}$ there exists $i_0$ such that $(x_j, x_k)\in U$ for $j, k\geq i_0$. | ||
| (Compare with the definition of complete uniformity in 15.7 of {{zb:1380.46022}} where uniform structure is defined using pseudometrics.) | ||
|
|
||
| Such spaces are called *Dieudonné complete* (Problem 8.5.13 in {{zb:0684.54001}}) or *completely uniformizable* (Problem 39B in {{zb:1052.54001}}). | ||
| They are called *topologically complete* on page 208 of {{mr:370454}}; | ||
| this last term has also been used for {P55} and {P63}. | ||
|
|
||
| ---- | ||
| #### Meta-properties | ||
|
|
||
| - $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does. | ||
| - This property is preserved by arbitrary products. | ||
| - This property is hereditary with respect to closed sets. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,9 @@ | ||
| --- | ||
| uid: T000914 | ||
| if: | ||
| P000221: true | ||
| then: | ||
| P000012: true | ||
| --- | ||
|
|
||
| {P12} spaces are precisely the spaces admitting a uniformity. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| --- | ||
| uid: T000915 | ||
| if: | ||
| P000162: true | ||
| then: | ||
| P000221: true | ||
| refs: | ||
| - zb: "1380.46022" | ||
| name: Rings of Continuous Functions (Gillman & Jerison) | ||
| --- | ||
|
|
||
| See Corollary 15.14 of {{zb:1380.46022}} for complete uniformity on a {P162} space. | ||
| Alternatively, a {P162} space is a closed subspace of product of {S25} and {S25|P53}. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,16 @@ | ||
| --- | ||
| uid: T000916 | ||
| if: | ||
| and: | ||
| - P000001: true | ||
| - P000164: true | ||
| - P000221: true | ||
| then: | ||
| P000162: true | ||
| refs: | ||
| - zb: "1380.46022" | ||
| name: Rings of Continuous Functions (Gillman & Jerison) | ||
| --- | ||
|
|
||
| A {P221} {P1} space is {P6} [(Explore)](https://topology.pi-base.org/spaces?q=dieudonne+complete+%2B+T_0+%2B+not+completely+regular). | ||
| Now apply Theorem 15.20 of {{zb:1380.46022}}. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| --- | ||
| uid: T000917 | ||
| if: | ||
| and: | ||
| - P000134: true | ||
| - P000030: true | ||
| then: | ||
| P000221: true | ||
| refs: | ||
| - zb: "1358.54001" | ||
| name: General Topology (Kelley) | ||
| --- | ||
|
|
||
| By taking the Kolmogorov quotient we can assume $X$ is {P3}. | ||
| Assume $X$ is not {P221}. Since $X$ is {P207} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+strongly+collectionwise+normal), the neighbourhoods of the diagonal $\Delta_X\subseteq X\times X$ form a uniformity $\mathcal{U}$ on $X$, and since $X$ is {P12} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+completely+regular), the uniformity is compatible with $X$. | ||
|
|
||
| Equip $X$ with this uniformity and let $(x_i)_{i\in I}$ be a Cauchy net on $X$ that isn't convergent. Since a Cauchy net converges to each of its cluster points (see Theorem 6.21 on page 191 of {{zb:1358.54001}}), for each $x\in X$ there exists a neighbourhood $U_x$ of $x$ such that $x_i\notin U_x$ for large enough $i$. | ||
|
|
||
| From Theorem 5.28 on page 156 of {{zb:1358.54001}}, the open cover $\{U_x : x\in X\}$ is even, so there exists $V\in\mathcal{U}$ such that each $V[x] = \{y\in X :(x, y)\in V\}$ is contained in $U_z$ for some $z\in X$. If $i_0$ is such that $(x_j, x_k)\in V$ for $j, k\geq i_0$, then $(x_{i_0}, x_i)\in V$ for all $i\geq i_0$, so $x_i\in V[x_{i_0}]\subseteq U_z$ for all $i\geq i_0$. This is a contradiction since $x_i\notin U_z$ for big enough $i$. |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.