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(LightProfinite): being light is a property of a profinite space #10391

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat(LightProfinite): being light is a property of a profinite space #10391

wants to merge 20 commits into from

Conversation

dagurtomas
Copy link
Collaborator

@dagurtomas dagurtomas commented Feb 9, 2024 •
edited

This PR defines the class Profinite.IsLight which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a LightProfinite, and the underlying profinite space of a LightProfinite is light.

Open in Gitpod

@dagurtomas dagurtomas mentioned this pull request Feb 9, 2024
Closed
7 tasks
@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR awaiting-CI t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Feb 9, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 9, 2024
@dagurtomas dagurtomas mentioned this pull request Feb 10, 2024
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 14, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@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 Feb 14, 2024
@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 Feb 14, 2024
@joelriou joelriou self-assigned this Feb 16, 2024
riccardobrasca
riccardobrasca reviewed Feb 27, 2024
View reviewed changes
Mathlib/Topology/Category/LightProfinite/IsLight.lean Outdated Show resolved Hide resolved
Mathlib/Topology/Category/LightProfinite/IsLight.lean Outdated
instance (X Y : Profinite) [X.IsLight] [Y.IsLight] : (Profinite.of (X × Y)).IsLight where
countable_clopens := Clopens.countable_prod

instance (S : Profinite) [S.IsLight] : Countable (DiscreteQuotient S) := by
Copy link
Member

Choose a reason for hiding this comment

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

Can you add a mathematical explanation of this proof? (In principle it would be nice to split it...)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I added just a small explanation, but I agree it would be nice to split it. I'll see what I can do about that tomorrow.

Copy link
Collaborator

Choose a reason for hiding this comment

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

In order to split the proof, I would suggest constructing, for any S profinite, an equiv. between DiscreteQuotient S and suitable Finset of clopens.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I changed the proof to using an injective map DiscreteQuotient S → Finset (Clopens S) instead, I think it's a lot clearer. I added a TODO to prove that this gives a bijection with the finite partitions of S into clopens.

dagurtomas and others added 2 commits February 27, 2024 23:51
@dagurtomas @riccardobrasca
Update Mathlib/Topology/Category/LightProfinite/IsLight.lean
de04156 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@dagurtomas
add small explanation
3e10359
@joelriou joelriou removed the awaiting-review The author would like community review of the PR label Mar 7, 2024
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 7, 2024
@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 9, 2024
@joelriou
Copy link
Collaborator

Thanks!

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Mar 12, 2024

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 12, 2024
@dagurtomas @joelriou
Update Mathlib/Topology/Category/LightProfinite/IsLight.lean
3a63c2f 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@dagurtomas
Copy link
Collaborator Author

Thanks for the reviews!
bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 12, 2024
@dagurtomas
feat(LightProfinite): being light is a property of a profinite space (#…
d1d1772 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LightProfinite): being light is a property of a profinite space [Merged by Bors] - feat(LightProfinite): being light is a property of a profinite space Mar 12, 2024
@mathlib-bors mathlib-bors bot closed this Mar 12, 2024
@mathlib-bors mathlib-bors bot deleted the dagur_IsLight branch March 12, 2024 11:33
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@dagurtomas @kbuzzard
feat(LightProfinite): being light is a property of a profinite space (#…
8778165 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
dagurtomas added a commit that referenced this pull request Mar 22, 2024
@dagurtomas
feat(LightProfinite): being light is a property of a profinite space (#…
431fe8a 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light.

- [x] depends on: #10390
utensil pushed a commit that referenced this pull request Mar 26, 2024
@dagurtomas @utensil
feat(LightProfinite): being light is a property of a profinite space (#…
6d06a51 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@dagurtomas @Louddy
feat(LightProfinite): being light is a property of a profinite space (#…
31d5576 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@dagurtomas @uniwuni
feat(LightProfinite): being light is a property of a profinite space (#…
733ac0c 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@dagurtomas @callesonne
feat(LightProfinite): being light is a property of a profinite space (#…
a2c7314 
…10391)

This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. 

- [x] depends on: #10390
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

@joelriou joelriou joelriou left review comments

Assignees

@joelriou joelriou

Labels
delegated t-category-theory Category theory 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
@dagurtomas @leanprover-community-mathlib4-bot @joelriou @riccardobrasca