feat(category_theory/basic/category): Combine and improve API on preorder categories. (#8982)
Material on preorders as categories was previously scattered throughout the library. This PR unites this material into a single file `category_theory/category/preorder` and also expands upon it, by relating adjoints to galois connections.
Co-authored-by: justus-springer <50165510+justus-springer@users.noreply.github.com>