Merged
Conversation
ScriptRaccoon
force-pushed
the
strongly-connected-categories
branch
from
103558d to
340a5d1
Compare
…undant assignments
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
1 participant
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.
We already had a property named "strongly connected" before (#3), but the definition was a bit non-standard. I have renamed* this property to "semi-strongly connected". It says that the category is inhabited and for every pair of objects$A,B$ there is a morphism $A \to B$ or $B \to A$ .
I also added a stronger property called "strongly connected" (directly borrowed from graph theory), meaning that the category is inhabited and for every pair of objects$A,B$ there is a morphism $A \to B$ . As usual, several implications have been added as well, and the property has been decided for all the categories in the database. It turns out that strongly connected categories are "not far" from pointed categories.
I also updated the nLab article accordingly.
Finally, the implication
"strongly connected + finite products => disjoint finite products"
has been added; which is also dualized automatically. This made it possible to remove 10 manual property assignments, now they are done automatically. (For example, CMon has disjoint coproducts since it is strongly connected (it is pointed!) and has coproducts.) Also, the implication "biproducts => disjoint finite coproducts" could be removed, this is now a consequence.
*This is not standard and subject to change.