[Merged by Bors] - chore(category_theory/limits): facts about opposites of limit cones #4250
Conversation
semorrison
added
the
awaiting-review
|
|
||
| namespace Monad_Mon_equiv |
There was a problem hiding this comment.
The changes in this file are unrelated to the PR. It seems the definitions here were teetering at the end of our -T100000 limit, and adding a few more simp lemmas tipped them over. I split the affected declaration into three pieces, and took the opportunity to make the naming more boring.
| @@ -512,8 +512,7 @@ begin | |||
| dsimp, | |||
| rw [comp_id, H.map_comp, is_equivalence.fun_inv_map H, assoc, nat_iso.cancel_nat_iso_hom_left, | |||
| assoc, is_equivalence.inv_fun_id_inv_comp], | |||
| apply comp_id, | |||
| -- annoyingly `dsimp, simp` leaves it as `c.π.app j ≫ 𝟙 _ = c.π.app j` instead of closing... | |||
There was a problem hiding this comment.
What's wrong with using comp_id to close the goal here? I guess it could be faster?
There was a problem hiding this comment.
Nothing was wrong with apply comp_id as a proof. More it was that I was previously disappointed that dsimp, simp was mysteriously failing, and now happy to see that it was working properly.
src/category_theory/opposites.lean
Outdated
| def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D := | ||
| { functor := e.functor.unop, | ||
| inverse := e.inverse.unop, | ||
| unit_iso := nat_iso.of_components (λ X, |
There was a problem hiding this comment.
Shouldn't this be just as short as the def above it? Is nat_iso.unop missing?
There was a problem hiding this comment.
Err... there's some good reason why it can't exist (Lean, quite reasonably, can't unify something) but I forget the details. I'll try to reconstruct them and write a comment.
There was a problem hiding this comment.
Oh, I see. No, nat_iso.unop already exists, and works fine. The problem is that here we would be trying to unop something like e.functor.op ⋙ e.inverse.op. That is equal to (e.inverse ⋙ e.functor).op, but not equal enough for Lean to allow using nat_iso.unop.
There was a problem hiding this comment.
No, I just wasn't trying hard enough. It's fixed now.
github-actions
bot
added
ready-to-merge
…4250) Simple facts about limit cones and opposite categories. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…4250) Simple facts about limit cones and opposite categories. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Simple facts about limit cones and opposite categories.