Skip to content

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

Closed
Multramate wants to merge 12 commits intomasterfrom
gleason
Closed

[Merged by Bors] - feat(Topology/ExtremallyDisconnected): prove Gleason's theorem#5634
Multramate wants to merge 12 commits intomasterfrom
gleason

Conversation

@Multramate
Copy link
Copy Markdown
Collaborator

@Multramate Multramate commented Jun 30, 2023 •
edited
Loading

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 awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Jul 8, 2023
@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Jul 8, 2023

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

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 8, 2023
@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
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 27, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) 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
Copy Markdown
Contributor

@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!

@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 1, 2023
@Multramate Multramate requested a review from j-loreaux August 3, 2023 15:11
@Multramate Multramate added awaiting-review 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
Copy Markdown
Contributor

@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.

@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 8, 2023
@Multramate Multramate added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 8, 2023
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 9, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 9, 2023
bors bot pushed a commit that referenced this pull request Aug 9, 2023
@Multramate
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
Copy Markdown

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
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@Multramate @kim-em
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.

2 participants

@Multramate @j-loreaux