StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper

theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c), StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f) = f

This theorem states that for a given topological space `X`, a point `p₀` in `X`, a category `C` with terminal objects and colimits, a presheaf `𝓕` of `C` on `X`, and a morphism `f` from the stalk of the presheaf at the point `p₀` to an object `c` in `C`, the composition of the morphism `f` with the function `fromStalk` applied to the result of `toSkyscraperPresheaf` applied to `f` is equal to `f` itself. Essentially, it expresses a kind of round-trip property: if you map a stalked presheaf to a 'skyscraper presheaf' and then map it back again, you get the original presheaf.

More concisely: For any topological space X, presheaf 𝓕 on X, point p0 in X, object c in the category C with terminal objects and colimits, and morphism f from the stalk of 𝓕 at p0 to c, the diagram commutes: fromStalk (toSkyscraperPresheaf f) = f.