restrictStalkIso_inv_eq_germ — Mathlib

English

The inverse of the restriction stalk iso, composed with the germ map, equals the germ on the restricted presheaf.

Русский

Обратное ограничение stalk iso, сопоставленное с гермой, даёт герму ограниченного предsheaf.

LaTeX

$$$$ X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) \\langle x, hx, rfl \\rangle \\circ (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ V x hx $$$$

Lean4

@[reassoc (attr := simp)]
theorem restrictStalkIso_inv_eq_germ :
    X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ ≫ (X.restrictStalkIso h x).inv =
      (X.restrict h).presheaf.germ _ x hx :=
  PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace h V x hx

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