Lean4
/-- Taking skyscraper sheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
`p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
-/
def skyscraperSheafFunctor : C ⥤ Sheaf C X
where
obj c := skyscraperSheaf p₀ c
map f := Sheaf.Hom.mk <| (skyscraperPresheafFunctor p₀).map f
map_id _ := Sheaf.Hom.ext <| (skyscraperPresheafFunctor p₀).map_id _
map_comp _ _ := Sheaf.Hom.ext <| (skyscraperPresheafFunctor p₀).map_comp _ _