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(algebraic_topology/simplicial_object): Some API for converting between simplicial and cosimplicial #7656
Conversation
have := f.w, | ||
apply_fun (λ η, η.app x.unop) at this, | ||
exact this.symm, |
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.
have := f.w, | |
apply_fun (λ η, η.app x.unop) at this, | |
exact this.symm, | |
exact (congr_app f.w x.unop).symm, |
Took me a while to remember that we added congr_app
for exactly this awkwardness!
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.
Done! That's a useful one :)
have := f.unop.w, | ||
apply_fun (λ η, η.app (op x)) at this, | ||
exact this.symm, |
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.
have := f.unop.w, | |
apply_fun (λ η, η.app (op x)) at this, | |
exact this.symm, | |
exact (congr_app f.unop w (op x)).symm, |
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.
done
Otherwise, looks great. bors d+ |
✌️ adamtopaz 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>
…r-community/mathlib into simplicial_cosimplicial_equivs
bors r+ |
…etween simplicial and cosimplicial (#7656) This adds some code which is helpful to convert back and forth between simplicial and cosimplicial object. For augmented objects, this doesn't follow directly from the existing API in `category_theory/opposite`. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…etween simplicial and cosimplicial (#7656) This adds some code which is helpful to convert back and forth between simplicial and cosimplicial object. For augmented objects, this doesn't follow directly from the existing API in `category_theory/opposite`. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
This adds some code which is helpful to convert back and forth between simplicial and cosimplicial object.
For augmented objects, this doesn't follow directly from the existing API in
category_theory/opposite
.