Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(topology/sets/closeds): atoms in a t1_space are singletons #16721

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(topology/sets/closeds): atoms in a t1_space are singletons #16721

wants to merge 7 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Sep 30, 2022 •
edited

This is helpful to show that maximal ideals of C(X, π•œ) with X compact Hausdorff and π•œ either ℝ or β„‚ correspond to complements of singletons with respect to the Galois connection between continuous_map.ideal_to_set and continuous_map.set_to_ideal.

Open in Gitpod

@j-loreaux j-loreaux added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters labels Sep 30, 2022
@j-loreaux j-loreaux mentioned this pull request Sep 30, 2022
Closed
8 tasks
@j-loreaux j-loreaux added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 30, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 30, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 8, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@j-loreaux j-loreaux added the easy < 20s of review time. See the lifecycle page for guidelines. label Oct 8, 2022
@kbuzzard kbuzzard mentioned this pull request Oct 8, 2022
Closed
@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 10, 2022
@ADedecker ADedecker self-assigned this Oct 10, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 10, 2022
@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 10, 2022
@j-loreaux
Copy link
Collaborator Author

Let me know what you think now. I believe it's better overall, and it can all just go in the closeds file. I think that's acceptable.

@j-loreaux j-loreaux changed the title feat(topology/sets/opens): coatoms in a t1_space are complements of singletons feat(topology/sets/closeds): atoms in a t1_space are singletons Oct 11, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 11, 2022
@ADedecker ADedecker removed the awaiting-review The author would like community review of the PR label Oct 11, 2022
@ADedecker ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 11, 2022
@j-loreaux @ADedecker
Anatole's improvement
0091c0e 
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
@ADedecker
Copy link
Member

Thanks!

maintainer merge

@j-loreaux
Copy link
Collaborator Author

maintainer merge

@github-actions
Copy link

πŸš€ Pull request has been placed on the maintainer queue by j-loreaux.

@hrmacbeth
Copy link
Member

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 12, 2022
bors bot pushed a commit that referenced this pull request Oct 12, 2022
@j-loreaux
feat(topology/sets/closeds): atoms in a t1_space are singletons (#16721)
2e348d4 
This is helpful to show that maximal ideals of `C(X, π•œ)` with `X` compact Hausdorff and `π•œ` either `ℝ` or `β„‚` correspond to complements of singletons with respect to the Galois connection between `continuous_map.ideal_to_set` and `continuous_map.set_to_ideal`.
@bors
Copy link

bors bot commented Oct 12, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/sets/closeds): atoms in a t1_space are singletons [Merged by Bors] - feat(topology/sets/closeds): atoms in a t1_space are singletons Oct 12, 2022
@bors bors bot closed this Oct 12, 2022
@bors bors bot deleted the j-loreaux/opens-coatoms branch October 12, 2022 07:20
bors bot pushed a commit that referenced this pull request Oct 24, 2022
@j-loreaux
feat(topology/continuous_function/ideals): maximal ideals correspond …
63ff453 
…to (complements of) singletons (#16719)

This establishes the correspondence between maximal ideals of `C(X, π•œ)`  (where `X` is compact Hausdorff and `is_R_or_C π•œ`) and the complements of singletons in `X`. This allows for the proof that the natural map from `X` to `character_space π•œ C(X, π•œ)` is a homeomorphism.

- [x] depends on: #16709 
- [x] depends on: #16713 
- [x] depends on: #16714 
- [x] depends on: #16677 
- [x] depends on: #16663
- [x] depends on: #16721
- [x] depends on: #16722 
- [x] depends on: #16801
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ADedecker ADedecker ADedecker left review comments

Assignees

@ADedecker ADedecker

Labels
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@j-loreaux @mathlib-dependent-issues-bot @ADedecker @hrmacbeth