Commit 2025-04-10 17:59 f7fae502

feat(CategoryTheory/Sites): global sections functor on sheaves (#22816) This PR defines Sheaf.Γ : Sheaf J A ⥤ A as the functor taking each sheaf to the limit of its underlying presheaf whenever possible, i.e. whenever A has sufficiently large limits, and shows that this agrees with several other common definitions when they are defined, like evaluation of sheaves on a terminal object. See Zulip for the discussion that lead to this approach.