Skip to content

[Merged by Bors] - feat(Condensed): explicit sheaf condition for light condensed sets#13503

Closed
dagurtomas wants to merge 5 commits intomasterfrom
dagur/LightCondensedExpl
Closed

[Merged by Bors] - feat(Condensed): explicit sheaf condition for light condensed sets#13503
dagurtomas wants to merge 5 commits intomasterfrom
dagur/LightCondensedExpl

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jun 4, 2024 •
edited
Loading

@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory t-condensed Condensed mathematics labels Jun 4, 2024
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 4, 2024
This was referenced Jun 4, 2024
Closed
Closed
@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 4, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 5, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 5, 2024

This PR/issue depends on:

@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 5, 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 6, 2024
joelriou
joelriou reviewed Jun 6, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 6, 2024
View reviewed changes
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 6, 2024

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 6, 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 6, 2024
@dagurtomas @joelriou
Apply suggestions from code review
6b12255 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Jun 7, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 7, 2024
@dagurtomas
feat(Condensed): explicit sheaf condition for light condensed sets (#…
678f491 
…13503)

- [x] depends on: #13501
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 7, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Condensed): explicit sheaf condition for light condensed sets [Merged by Bors] - feat(Condensed): explicit sheaf condition for light condensed sets Jun 7, 2024
@mathlib-bors mathlib-bors bot closed this Jun 7, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/LightCondensedExpl branch June 7, 2024 09:39
grunweg pushed a commit that referenced this pull request Jun 7, 2024
@dagurtomas @grunweg
feat(Condensed): explicit sheaf condition for light condensed sets (#…
d7936b7 
…13503)

- [x] depends on: #13501
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@dagurtomas @AntoineChambert-Loir
feat(Condensed): explicit sheaf condition for light condensed sets (#…
914c601 
…13503)

- [x] depends on: #13501
mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
@dagurtomas
feat(Condensed): the functor from TopCat to LightCondSet (#13504)
e655d3b 
- [x] depends on: #13503
dagurtomas added a commit that referenced this pull request Jul 2, 2024
@dagurtomas
feat(Condensed): the functor from TopCat to LightCondSet (#13504)
d3774bd 
- [x] depends on: #13503
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-category-theory Category theory t-condensed Condensed mathematics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@dagurtomas @joelriou