feat(category_theory/opposites): some opposite category properties (#2464)
feat(category_theory/opposites): some opposite category properties (#2464)

Add some more basic properties relating to the opposite category.

Make sure you have:

  * [x] reviewed and applied the coding style: [coding](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/naming.md)
  * [x] reviewed and applied [the documentation requirements](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/doc.md)
  * [x] make sure definitions and lemmas are put in the right files
  * [x] make sure definitions and lemmas are not redundant

For reviewers: [code review check list](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/code-review.md)

If you're confused by comments on your PR like `bors r+` or `bors d+`, please see our [notes on bors](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/bors.md) for information on our merging workflow.




leanprover-community/mathlib,leanprover-community/mathlib