stalkIso'_symm_mk — Mathlib

English

The symmetric of the stalk isomorphism is given by Germ on open basic sets, with the same explicit formula as the forward map.

Русский

Симметрическая часть изоморфизма стока задаётся germ на базовых открытых множествах тем же выражением, что и прямой путь.

LaTeX

$$$(\mathrm{stalkIso}'_{\mathcal{A}}(x))^{-1} = \mathrm{germ}$$$

Lean4

@[simp]
theorem stalkIso'_symm_mk (x) (f) :
    (Proj.stalkIso' 𝒜 x).symm (.mk f) =
      (Proj.structureSheaf 𝒜).presheaf.germ _ x (mem_basicOpen_den _ x f) (sectionInBasicOpen _ x f) :=
  rfl

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