Add properties: cartesian filtered colimits + cocartesian cofiltered limits#84
Merged
ScriptRaccoon merged 14 commits intomainfrom Apr 16, 2026
Merged
Add properties: cartesian filtered colimits + cocartesian cofiltered limits#84ScriptRaccoon merged 14 commits intomainfrom
ScriptRaccoon merged 14 commits intomainfrom
Conversation
88db21e to
811ccc5
Compare
d328b31 to
b0517d2
Compare
5d18203 to
0ee5b26
Compare
b741286 to
86e749a
Compare
this settles in particular the category of sets (and many more)
baa1e95 to
c183ce7
Compare
This was referenced Apr 18, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Several proofs that certain categories are not cartesian closed or do not have exact filtered colimits have used a different property (or its negation): for every object$X$ the functor $X \times -$ preserves filtered colimits. This property has several connections to existing properties in the database, so it makes sense to add this here. My question on mathoverflow indicates that there is no established name yet, but cartesian filtered colimits has been suggested. So let's take this here.
Adding the property of having cartesian filtered colimits along with several implications indeed has clarified a lot of proofs in the database, and some could even be removed since they are now automatically generated (see the change in
database/data/004_property-assignments/Meas.sqlfor example).Another motivation to add this property was to decide efficiently if the partial order$[0,1]$ (regarded as a thin category) has exact filtered colimits; this was missing before this PR. This is now done automatically by combining several implications:
cartesian closed + filtered colimits => cartesian filtered colimits,thin + cartesian filtered colimits => exact filtered colimits, and we already knew that it is cartesian closed because ofthin + semi-strongly connected => locally cartesian closed.Since the deduction system automatically dualizes implications, it makes sense to directly also add the dual property of having cocartesian cofiltered limits (which is even less common). This means that$X \sqcup -$ preserves cofiltered limits.
The property "cartesian filtered colimits" has been decided for almost all categories in the database. Exceptions:
LRS,Sch(let's not talk about these...), andMet_c(I don't even know right now if filtered colimits exist).The property "cocartesian cofiltered limits" has been deciced for all categories in the database. Some proofs are quite interesting, for example why Grp does not satisfy this property.