[Merged by Bors] - feat(algebraic_topology/dold_kan): tools for compatibilities, lemmas#17923
[Merged by Bors] - feat(algebraic_topology/dold_kan): tools for compatibilities, lemmas#17923
Conversation
|
This PR/issue depends on: |
| /-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced | ||
| from the counit isomorphism of `e'`. -/ | ||
| @[simps hom_app] | ||
| def τ₀ : eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor := |
There was a problem hiding this comment.
The name τ₀ is not great, unless it is standard for what you are doing. It is however tucked away in a namespace so perhaps wouldn't cause too much trouble. Will you be using this declaration outside this file? If not, it could be private; if so it could be called some horrible long mathlib name, or you could just leave it because in my mind it's very much a "lemma 3" kind of definition (needs to be there, is really called "this square obviously commutes" or whatever). Same comments for tau_1 and υ later on.
There was a problem hiding this comment.
Actually, these τ₀ etc appear in the assumptions to the constructions and statements in this file. They are used for the Dold-Kan equivalence for pseudoabelian categories (which is the very reason for the stuff in this file compatibility.lean). Then, keeping these in their separate namespace looks like the best solution.
| equivalence.fun_inv_map, iso.inv_hom_id_app_assoc, hG.inv_hom_id_app], | ||
| dsimp, | ||
| rw [comp_id, eA.functor_unit_iso_comp, e'.functor.map_id, id_comp, hF.inv_hom_id_app_assoc], | ||
| end |
There was a problem hiding this comment.
Wow! Well done, it doesn't even take forever to compile. Could you imagine a tactic doing this kind of argument in Lean 4?
There was a problem hiding this comment.
It was more painful when I initially attempted to prove these compatibilities directly on the Dold-Kan functors, but it become more smooth when I isolated the "general" statement involving abstract functors and isomorphisms. I do not know how to even think of a category_coherence which would prove all diagrams involving adjunctions commute.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Thanks for the review @kbuzzard ! Indeed, I could have obtained a Dold-Kan equivalence |
|
bors merge |
…17923) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Uh oh!
There was an error while loading. Please reload this page.