stalkMap_inv_hom — Mathlib

English

If two morphisms are equal, their stalk maps agree up to the corresponding specialization equivalence.

Русский

Если два гомоморфизма равны, их stalk maps совпадают с учётом соответствующего эквивалентного отношения специализации.

LaTeX

$$$$f = g \\Rightarrow f.stalkMap x \\circ X.presheaf.stalkSpecializes (\\text{specializes_of_eq} \\cdot) = g.stalkMap x' \\circ Y.presheaf.stalkSpecializes (\\text{specializes_of_eq} \\cdot).$$$$

Lean4

@[reassoc (attr := simp)]
theorem stalkMap_inv_hom (e : X ≅ Y) (x : X) :
    e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x = X.presheaf.stalkSpecializes (specializes_of_eq <| by simp) :=
  by
  rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)]
  simp

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