Skip to content

[Merged by Bors] - feat: Stonean is precoherent#6725

Closed
dagurtomas wants to merge 5 commits intomasterfrom
dagur_StoneanPrecoherent
Closed

[Merged by Bors] - feat: Stonean is precoherent#6725
dagurtomas wants to merge 5 commits intomasterfrom
dagur_StoneanPrecoherent

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Aug 22, 2023

Co-authored-by: Jon Eugster @joneugster
Co-authored-by: Boris Bolvig Kjær bbk@math.ku.dk @bbolvig
Co-authored-by: Sina Hazratpour sinahazratpour@gmail.com @sinhp
Co-authored-by: Nima Rasekh rasekh@mpim-bonn.mpg.de @nimarasekh

We give a characterisation of effective epimorphic families in Stonean and deduce that Stonean is a precoherent category.
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.


Open in Gitpod

@dagurtomas
Copy link
Copy Markdown
Contributor Author

This is instead of #5861 which had too many merge conflicts.

@dagurtomas dagurtomas mentioned this pull request Aug 22, 2023
1 task
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 22, 2023
@dagurtomas dagurtomas added t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Aug 22, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 22, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 22, 2023

This PR/issue depends on:

@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 22, 2023
@dagurtomas dagurtomas requested a review from jcommelin August 22, 2023 22:15
@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 Aug 22, 2023
Copy link
Copy Markdown
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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 23, 2023
bors bot pushed a commit that referenced this pull request Aug 23, 2023
Co-authored-by: Jon Eugster @joneugster  
Co-authored-by: Boris Bolvig Kjær <bbk@math.ku.dk> @bbolvig
Co-authored-by: Sina Hazratpour <sinahazratpour@gmail.com> @sinhp
Co-authored-by: Nima Rasekh <rasekh@mpim-bonn.mpg.de> @nimarasekh 

 -  [x] depends on: #5808  

We give a characterisation of effective epimorphic families in `Stonean` and deduce that `Stonean` is a precoherent category.
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.
@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 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: Stonean is precoherent [Merged by Bors] - feat: Stonean is precoherent Aug 23, 2023
@bors bors bot closed this Aug 23, 2023
@bors bors bot deleted the dagur_StoneanPrecoherent branch August 23, 2023 08:58
dagurtomas added a commit that referenced this pull request Aug 23, 2023
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-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants