English
For specialization h, the specialized stalk maps commute with the fiber maps to the base ring after localization.
Русский
Для специализации г, композиции стэков совместимы с волокнами к базовой карте после локализации.
LaTeX
$$$(structureSheaf R).presheaf.stalkSpecializes h \\gg\\; StructureSheaf.stalkToFiberRingHom R x = StructureSheaf.stalkToFiberRingHom R y \\gg (CommRingCat.ofHom(PrimeSpectrum.localizationMapOfSpecializes h))$$$
Lean4
@[simp, reassoc, elementwise nosimp]
theorem stalkSpecializes_stalk_to_fiber {R : Type*} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) :
(structureSheaf R).presheaf.stalkSpecializes h ≫ StructureSheaf.stalkToFiberRingHom R x =
StructureSheaf.stalkToFiberRingHom R y ≫ (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)) :=
by
change _ ≫ (StructureSheaf.stalkIso R x).hom = (StructureSheaf.stalkIso R y).hom ≫ _
rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]
exact localizationToStalk_stalkSpecializes h
