Lean4
/-- If `f : 𝓕.stalk p₀ ⟶ c`, then a natural transformation `𝓕 ⟶ skyscraperPresheaf p₀ c` can be
defined by: `𝓕.germ p₀ ≫ f : 𝓕(U) ⟶ c` if `p₀ ∈ U` and the unique morphism to a terminal object
if `p₀ ∉ U`.
-/
@[simps]
def toSkyscraperPresheaf {𝓕 : Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) : 𝓕 ⟶ skyscraperPresheaf p₀ c
where
app
U :=
if h : p₀ ∈ U.unop then 𝓕.germ _ p₀ h ≫ f ≫ eqToHom (if_pos h).symm
else ((if_neg h).symm.ndrec terminalIsTerminal).from _
naturality U V
inc := by
dsimp
by_cases hV : p₀ ∈ V.unop
· have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
split_ifs
rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
· split_ifs
exact ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext ..