-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory/opposites): Add is_iso_op #9319
Conversation
justus-springer
commented
Sep 21, 2021
src/category_theory/opposites.lean
Outdated
@@ -86,6 +91,9 @@ lemma is_iso_of_op {X Y : C} (f : X ⟶ Y) [is_iso f.op] : is_iso f := | |||
⟨⟨(inv (f.op)).unop, | |||
⟨quiver.hom.op_inj (by simp), quiver.hom.op_inj (by simp)⟩⟩⟩ | |||
|
|||
lemma op_inv {X Y : C} (f : X ⟶ Y) [f_iso : is_iso f] : (inv f).op = inv f.op := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be a @[simp]
lemma? I'm not sure.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It probably should, since functor.map_inv
also simps towards the same direction.
bors d+ |
✌️ justus-springer can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors r+ |
Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|