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/ExtremallyDisconnected): prove Gleason's theorem #5634

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(Topology/ExtremallyDisconnected): prove Gleason's theorem #5634

wants to merge 12 commits into from

Conversation

Multramate
Copy link
Collaborator

@Multramate Multramate commented Jun 30, 2023 •
edited

This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Co-authored-by: Filippo A E Nuccio filippo.nuccio@univ-st-etienne.fr
Co-authored-by: Dagur Ásgeirsson dagurtomas@gmail.com
Co-authored-by: Nikolas Kuhn nikolaskuhn@gmx.de

Open in Gitpod

@Multramate Multramate added the WIP Work in progress label Jun 30, 2023
@Multramate Multramate marked this pull request as ready for review July 8, 2023 17:58
@Multramate Multramate added awaiting-review The author would like community review of the PR awaiting-CI new-feature Add features not present in Mathlib 3 and removed WIP Work in progress labels Jul 8, 2023
@Multramate
Copy link
Collaborator Author

Unsure where to put the lemmas mem_coe_of_mem, ..., image_coe_eq_restrict_image - any ideas appreciated.

@dagurtomas dagurtomas mentioned this pull request Jul 11, 2023
Closed
2 tasks
@Multramate Multramate changed the title feat: Gleason's theorem feat(Topology/ExtremallyDisconnected): Gleason's theorem Jul 15, 2023
@Multramate Multramate changed the title feat(Topology/ExtremallyDisconnected): Gleason's theorem feat(Topology/ExtremallyDisconnected): prove Gleason's theorem Jul 15, 2023
@Multramate Multramate added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 17, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 27, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 29, 2023
@j-loreaux j-loreaux self-assigned this Jul 29, 2023
j-loreaux
j-loreaux reviewed Aug 1, 2023
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is just a first review, as I'm sure there will be more to say later. One thing it would be really nice to have is comments within the proofs sketching the idea (these can be interspersed throughout the proof, or just one comment at the top, whichever makes more sense).

Thanks for filling in this TODO!

Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
@j-loreaux j-loreaux 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 Aug 1, 2023
@Multramate Multramate 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 Aug 3, 2023
j-loreaux
j-loreaux reviewed Aug 8, 2023
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I started a Zulip thread here about Lean.Internal.coeM that shows up for the monadic coercion lemmas. I think those are placed appropriately, but they may not be necessary if my alternative approach to Lemma 2.4 works.

Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Show resolved Hide resolved
Mathlib/Topology/ExtremallyDisconnected.lean Outdated Show resolved Hide resolved
@j-loreaux j-loreaux 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 new-feature Add features not present in Mathlib 3 labels Aug 8, 2023
@Multramate Multramate 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 Aug 8, 2023
@j-loreaux
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Aug 9, 2023
bors bot pushed a commit that referenced this pull request Aug 9, 2023
@Multramate @faenuccio
@dagurtomas @nick-kuhn
feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634)
a2c3434 
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Co-authored-by: Filippo A E Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Dagur Ásgeirsson <dagurtomas@gmail.com>
Co-authored-by: Nikolas Kuhn <nikolaskuhn@gmx.de>
@bors
Copy link

bors bot commented Aug 9, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(Topology/ExtremallyDisconnected): prove Gleason's theorem [Merged by Bors] - feat(Topology/ExtremallyDisconnected): prove Gleason's theorem Aug 9, 2023
@bors bors bot closed this Aug 9, 2023
@bors bors bot deleted the gleason branch August 9, 2023 20:23
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@Multramate @faenuccio
@dagurtomas @nick-kuhn @semorrison
feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634)
adbc69d 
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Co-authored-by: Filippo A E Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Dagur Ásgeirsson <dagurtomas@gmail.com>
Co-authored-by: Nikolas Kuhn <nikolaskuhn@gmx.de>
bors bot pushed a commit that referenced this pull request Aug 22, 2023
@dagurtomas @Multramate
feat: projectivity of Stonean in CompHaus (#5808)
093597d 
Co-authored-by: Filippo A E Nuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr)
Co-authored-by: Nikolas Kuhn [nikolaskuhn@gmx.de](mailto:nikolaskuhn@gmx.de)
Co-authored-by: Adam Topaz [topaz@ualberta.ca](mailto:topaz@ualberta.ca)

 -  [x] depends on: #5634 
 -  [x] depends on: #5761  

This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.



Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

@j-loreaux j-loreaux

Labels
ready-to-merge This PR has been sent to bors. 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
3 participants
@Multramate @j-loreaux @leanprover-community-mathlib4-bot