English
Let f: X → Y be a morphism of schemes, U ⊆ Y open, x ∈ X with hx: f.base x ∈ U, and y an element in the germ that sits over U. Then f.stalkMap x (Y.presheaf.germ _ (f.base x) hx y) equals X.presheaf.germ (f⁻¹ᵁ U) x hx (f.app U y). This is the compatibility of the stalk map with germs under f.
Русский
Пусть f: X → Y — морфизм схем, U ⊆ Y открыто, x ∈ X с hx: f.base x ∈ U, и y — элемент в germs над U. Тогда f.stalkMap x (Y.presheaf.germ _ (f.base x) hx y) = X.presheaf.germ (f⁻¹ᵁ U) x hx (f.app U y). Совместимость stalkMap с germs через f.
LaTeX
$$$f.stalkMap x (Y.presheaf.germ _ (f.base x) hx y) = X.presheaf.germ (f^{-1}\\!\\!\\, U) x hx (f.app U y)$$$
Lean4
@[simp]
theorem stalkMap_germ_apply (U : Y.Opens) (x : X) (hx : f.base x ∈ U) (y) :
f.stalkMap x (Y.presheaf.germ _ (f.base x) hx y) = X.presheaf.germ (f ⁻¹ᵁ U) x hx (f.app U y) :=
PresheafedSpace.stalkMap_germ_apply f.toPshHom U x hx y
