-
Notifications
You must be signed in to change notification settings - Fork 259
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.
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
[Merged by Bors] - feat(Condensed): Explicit descriptions of condensed sets #6731
Conversation
|
||
end Stonean | ||
|
||
namespace Condensed |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this maybe be CondensedSet
? Because the results here are not about arbitrary Condensed FooBar
, but specifically about CondensedSet
. That would allow more use of dot-notation...
Has this been discussed before and/or is there some policy? I'm not aware of it...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The target category should actually be more general. Then I can add versions for Type (u+1)
in the CondensedSet
namespace (maybe as abbrev
s?)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
We prove the characterisation of condensed sets as finite-product preserving presheaves satisfying the equalizer condition on `CompHaus`/`Profinite`, and just finite-product preserving presheaves on `Stonean`. Co-authored-by: Riccardo Brasca @riccardobrasca [riccardo.brasca@gmail.com](mailto:riccardo.brasca@gmail.com) Co-authored-by: Filippo A E Nuccio @faenuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr)
Build failed (retrying...): |
bors r- I'm pretty sure this is the one breaking the bors batches; could you merge master and fix the issues? |
Canceled. |
Hopefully works now. There were some name changes since this was last updated. |
It seems it does, thanks! (And congratulation for this result!) bors merge |
We prove the characterisation of condensed sets as finite-product preserving presheaves satisfying the equalizer condition on `CompHaus`/`Profinite`, and just finite-product preserving presheaves on `Stonean`. Co-authored-by: Riccardo Brasca @riccardobrasca [riccardo.brasca@gmail.com](mailto:riccardo.brasca@gmail.com) Co-authored-by: Filippo A E Nuccio @faenuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr)
Pull request successfully merged into master. Build succeeded: |
We prove the characterisation of condensed sets as finite-product preserving presheaves satisfying the equalizer condition on `CompHaus`/`Profinite`, and just finite-product preserving presheaves on `Stonean`. Co-authored-by: Riccardo Brasca @riccardobrasca [riccardo.brasca@gmail.com](mailto:riccardo.brasca@gmail.com) Co-authored-by: Filippo A E Nuccio @faenuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr)
We prove the characterisation of condensed sets as finite-product preserving presheaves satisfying the equalizer condition on
CompHaus
/Profinite
, and just finite-product preserving presheaves onStonean
.Co-authored-by: Riccardo Brasca @riccardobrasca riccardo.brasca@gmail.com
Co-authored-by: Filippo A E Nuccio @faenuccio filippo.nuccio@univ-st-etienne.fr
Stonean
inCompHaus
#5808Stonean
is precoherent #6725Stonean
andProfinite
#6810EffectiveEpiFamily
consists of anEffectiveEpi
#7420CompHaus
/Profinite
/Stonean
#7421IsSheafFor
certain presieves #7804CompHaus
and friends are preregular #8126