Commit 2026-02-27 15:40 3c2700df
View on Github →feat(CategoryTheory/Sites): skyscraper sheaves (#35719)
Let Φ be a point of a site (C, J). In this file, we construct the skyscraper sheaf functor skyscraperSheafFunctor : A ⥤ Sheaf J A and show that it is a right adjoint to Φ.sheafFiber : Sheaf J A ⥤ A.
Estimated changes
added theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_symm_apply
added theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm
added theorem CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val