fromStalk_to_skyscraper — Mathlib

English

Conversely, applying fromStalk to a skyscraper presheaf recovers the original presheaf morphism after applying toSkyscraperPresheaf.

Русский

Напротив, применение fromStalk к skyscraperPresheaf восстанавливает исходный морфизм предперешафа после применения toSkyscraperPresheaf.

LaTeX

$$$fromStalk p_0 (toSkyscraperPresheaf _ f) = f$$$

Lean4

theorem fromStalk_to_skyscraper {𝓕 : Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) :
    fromStalk p₀ (toSkyscraperPresheaf _ f) = f :=
  by
  refine 𝓕.stalk_hom_ext fun U hxU ↦ ?_
  rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc, eqToHom_trans,
    eqToHom_refl, Category.comp_id, Presheaf.germ]

Похожие утверждения