stalkMap_inv_hom_apply — Mathlib

English

If x = x' then the corresponding stalk maps agree after specialization.

Русский

Если x = x', то соответствующие stalk maps совпадают после специализации.

LaTeX

$$$$f.stalkMap x = f.stalkMap x'$$ under specialization.$$

Lean4

@[simp]
theorem stalkMap_inv_hom_apply (e : X ≅ Y) (x : X) (y) :
    e.hom.stalkMap x (e.inv.stalkMap (e.hom.base x) y) = X.presheaf.stalkSpecializes (specializes_of_eq <| by simp) y :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y

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