Skip to content

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules#13478

Closed
dagurtomas wants to merge 56 commits intomasterfrom
dagur/CondensedEpi
Closed

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules#13478
dagurtomas wants to merge 56 commits intomasterfrom
dagur/CondensedEpi

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jun 3, 2024

This PR characterises epimorphisms in condensed sets and condensed R-modules for any ring R, as morphisms of sheaves which are objectwise surjective on Stonean.


Open in Gitpod

joelriou and others added 30 commits March 27, 2024 10:10
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 3, 2024
@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 Jun 3, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 17, 2024

PR summary c6b1833b88

Import changes

No significant changes to the import graph


Declarations diff

+++ epi_iff_locallySurjective_on_compHaus
+++ epi_iff_surjective_on_stonean

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 17, 2024
@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 Jun 17, 2024
@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 Jun 17, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 1, 2024
@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 1, 2024
@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 1, 2024
@joelriou
Copy link
Copy Markdown
Contributor

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 10, 2024
…les (#13478)

This PR characterises epimorphisms in condensed sets and condensed `R`-modules for any ring `R`, as morphisms of sheaves which are objectwise surjective on `Stonean`. 



Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 10, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Condensed): characterise epimorphisms in condensed sets and modules [Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules Jul 10, 2024
@mathlib-bors mathlib-bors bot closed this Jul 10, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/CondensedEpi branch July 10, 2024 18:10
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory t-condensed Condensed mathematics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants