[Merged by Bors] - feat(category_theory/sites/compatible_*): Compatibility of plus and sheafification with composition.

[adamtopaz]

Compatibility of sheafification with composition. This will be used later to obtain adjunctions between categories of sheaves.

---

• depends on: [Merged by Bors] - feat(category_theory/sites/whiskering): Functors between sheaf categories induced by compositiion #10496

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(category_theory/sites/whiskering): Functors between sheaf categories induced by compositiion #10496

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[jcommelin]

bors d+

[jcommelin]

Should all these defs come with simps?

[adamtopaz]

I'm not sure how useful these would be in practice. I think it would be much more useful to relate these isomorphism to sheafify_lift, but that requires additional assumptions to know that sheafification is a sheaf. What do you propose? I could add such lemmas in a separate section with these additional hypotheses, but I think simply adding simps here would generate lemmas that unfold things "too much".

[adamtopaz]

I added lemmas relating hom and inv of this construction to sheafify_lift and to to_sheafify, as well as some simp lemmas reducing the other isomorphisms in this file to these cases... take a look toward the bottom of the file.

[bors]

✌️ adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adamtopaz]

bors d-

@jcommelin could you take another quick look when you have time? The last changes I made were not so trivial...

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests