English
Let f: X → Y be a morphism of schemes, U ⊆ Y open, x ∈ X with f.base x ∈ U, and hx witnesses the inclusion. Then the equality Y.presheaf.germ U (f.base x) hx ≫ f.stalkMap x = f.app U ≫ X.presheaf.germ (f⁻¹U) x hx holds, expressing compatibility of germ maps with base change along f.
Русский
Пусть f: X → Y — морфизм схем, U ⊆ Y открыто, x ∈ X с f.base x ∈ U, и hx — доказательство включения. Тогда верно равенство germ-образов: germ_U(Y)(f.base x) hx ∘ f.stalkMap x = f.app U ∘ germ_(f⁻¹U)(x) hx, выражающее совместимость germ-перемещений с базисным изменением вдоль f.
LaTeX
$$$Y.presheaf.germ U (f.base x) hx \\;\\gg\\; f.stalkMap x = f.app U \\;\\gg\\; X.presheaf.germ (f^{-1}⟨U⟩) x hx$$$
Lean4
@[reassoc (attr := simp)]
theorem stalkMap_germ (U : Y.Opens) (x : X) (hx : f.base x ∈ U) :
Y.presheaf.germ U (f.base x) hx ≫ f.stalkMap x = f.app U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hx :=
PresheafedSpace.stalkMap_germ f.toPshHom U x hx
