restrictStalkIso_hom_eq_germ_apply

English

The germ equality from restrictStalkIso_hom_eq_germ holds after applying the germ map argument.

Русский

Существование равенства гермов сохранится при применении соответствующего аргумента герма‑карт.

LaTeX

$$$$ (X.restrictStalkIso h x).hom ((X.restrict h).presheaf.germ _ x hx y) = X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ y $$$$

Lean4

theorem restrictStalkIso_hom_eq_germ_apply (y) :
    (X.restrictStalkIso h x).hom ((X.restrict h).presheaf.germ _ x hx y) =
      X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ y :=
  PresheafedSpace.restrictStalkIso_hom_eq_germ_apply X.toPresheafedSpace h V x hx y

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