Commit 2020-04-16 01:05 5ac2b48c
View on Github →feat(category_theory): connected categories (#2413)
- Define connected categories (using the convention that they must be nonempty) by asserting every functor to a discrete category is isomorphic to a constant functor. We also give some equivalent conditions which are more useful in practice: for instance that any function which is constant for objects which have a single morphism between them is constant everywhere.
- Give the definition of connected category as specified on wikipedia, and show it's equivalent. (This is more intuitive but it seems harder to both prove and use in lean, it also seems nicer stated with
head'. If reviewers believe this should be removed, I have no objection, but I include it for now since it is the more familiar definition). - Give three examples of connected categories.
- Prove that
X × -preserves connected limits. This PR is the first of three PRs aiming to resolve my TODO here - that the forgetful functor from the over category creates connected limits. Make sure you have:- reviewed and applied the coding style: coding, naming
- reviewed and applied the documentation requirements
- make sure definitions and lemmas are put in the right files
- make sure definitions and lemmas are not redundant If this PR is related to a discussion on Zulip, please include a link in the discussion. For reviewers: code review check list