Commit 2024-06-05 11:06 5795dea5
View on Github →feat: left adjoint functors preserve sheafification (#13499)
In this PR, we show that left adjoint functors preserve sheafification. The definition of Sheaf.composeAndSheafify was moved to the file PreservesSheafification.lean so that this definition may replace the previous sheafCompose'.