Commit 2024-12-19 21:50 c91dd0e1
View on Github →refactor(CategoryTheory/Sites): define Functor.sheafPullback as a left adjoint (#19516) The pullback of sheaves was previously constructed as a composition of functors involving a left Kan extension. We redefine it as an abstract left adjoint of the pushforward functor when it exists, and in the most favourable case, we provide an isomorphism with the previous construction. (This change shall be needed when we want to take pullback of étale sheaves.)