restrictStalkIso_hom_eq_germ — Mathlib

English

For an open embedding h: U ↪ X and V an open in U, the germ map after restriction matches the germ map before restriction via the restriction isomorphism.

Русский

Для вложения открытых множеств h: U ↪ X и открытого V в U, герма-отображение после ограничения совпадает с герма-отображением до ограничения через изоморфизм ограничения.

LaTeX

$$$$ (X.restrict h).presheaf.germ V x hx \\circ (X.restrictStalkIso h x).hom = X.presheaf.germ ((Opens.map f.base).obj V) (f x) ... $$$$

Lean4

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

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