stalkMap_hom_inv — Mathlib

English

For an isomorphism e: X ≅ Y and y ∈ Y, the application of the hom map after applying the inverse stalk map to y equals the specialization on y.

Русский

Для изоморфизма e: X ≅ Y и элемента y ∈ Y, применение germap после применения обратной stalkMap к y даёт специализацию на y.

LaTeX

$$$$e.hom.stalkMap (e.inv.base y) \\circ e.inv.stalkMap y = Y.presheaf.stalkSpecializes (specializes_of_eq \\text{...}).$$$$

Lean4

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

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