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: effective epi iff surjective in CompHaus/Profinite/Stonean #7421

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat: effective epi iff surjective in CompHaus/Profinite/Stonean #7421

wants to merge 5 commits into from

Conversation

dagurtomas
Copy link
Collaborator

@dagurtomas dagurtomas commented Sep 28, 2023 •
edited

@dagurtomas dagurtomas added t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Sep 28, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Sep 28, 2023
@dagurtomas dagurtomas mentioned this pull request Sep 28, 2023
Closed
20 tasks
jcommelin
jcommelin reviewed Sep 29, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

The three proofs are somewhat repetitive (-;
Is there maybe some categorical feature lurking underneath that could be abstracted out?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Sep 29, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@dagurtomas
Copy link
Collaborator Author

Probably it is enough to have pullbacks and coproducts interact nicely (something like extensive/regular), but I just abstracted out a stronger property that we already have for CompHaus, Profinite and Stonean.

@riccardobrasca
Copy link
Member

I agree it's not worth to find the maximal generality here, at least for now.

jcommelin
jcommelin approved these changes Oct 9, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 9, 2023
bors bot pushed a commit that referenced this pull request Oct 9, 2023
@dagurtomas
feat: effective epi iff surjective in CompHaus/Profinite/Stonean (
159651e 
#7421)

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

bors bot commented Oct 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: effective epi iff surjective in CompHaus/Profinite/Stonean [Merged by Bors] - feat: effective epi iff surjective in CompHaus/Profinite/Stonean Oct 9, 2023
@bors bors bot closed this Oct 9, 2023
@bors bors bot deleted the dagur_EffectiveEpiIffSurjective branch October 9, 2023 13:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. 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 @riccardobrasca @jcommelin