Lean4
/-- If `f : 𝓕 ⟶ skyscraperPresheaf p₀ c` is a natural transformation, then there is a morphism
`𝓕.stalk p₀ ⟶ c` defined as the morphism from colimit to cocone at `c`.
-/
def fromStalk {𝓕 : Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c) : 𝓕.stalk p₀ ⟶ c :=
let χ : Cocone ((OpenNhds.inclusion p₀).op ⋙ 𝓕) :=
Cocone.mk c <|
{ app := fun U => f.app ((OpenNhds.inclusion p₀).op.obj U) ≫ eqToHom (if_pos U.unop.2)
naturality := fun U V inc =>
by
dsimp only [Functor.const_obj_map, Functor.const_obj_obj, Functor.comp_map, Functor.comp_obj, Functor.op_obj,
skyscraperPresheaf_obj]
rw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc, eqToHom_trans, f.naturality,
skyscraperPresheaf_map]
have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2
simp only [dif_pos hV] }
colimit.desc _ χ
