English
The skyscraper presheaf at p0 is equal to the pushforward of the skyscraper presheaf on a point space PUnit along the map sending the unique point to p0.
Русский
Скейскрайперный препешаф в точке p0 равен отображению скейскрайперного препешафа из однозначного пространства на X через соответствующее отображение.
LaTeX
$$$skyscraperPresheaf(p_0,A) = (ofHom (ContinuousMap.const (TopCat.of PUnit) p_0))_* skyscraperPresheaf(X := TopCat.of PUnit) PUnit.unit A$$$
Lean4
theorem skyscraperPresheaf_eq_pushforward [hd : ∀ U : Opens (TopCat.of PUnit.{u + 1}), Decidable (PUnit.unit ∈ U)] :
skyscraperPresheaf p₀ A =
(ofHom (ContinuousMap.const (TopCat.of PUnit) p₀)) _* skyscraperPresheaf (X := TopCat.of PUnit) PUnit.unit A :=
by
convert_to
@skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <| ContinuousMap.const _ p₀).obj U) C _ _ A = _ <;>
congr
