English
A compatibility identity holds between stalk maps and Spec.map, equating a composite of stalk isomorphisms and a localization with the stalk map along f.
Русский
Существуют совместные равенства для stalk-map и Spec.map, где композиция локализованной гомоморфной структуры совпадает со stalk-map по f.
LaTeX
$$$ (StructureSheaf.stalkIso R .) .hom \circ (Localization.localRingHom) .circ (StructureSheaf.stalkIso S p).inv = (Spec.map f).stalkMap p $$$
Lean4
/-- Variant of `AlgebraicGeometry.localRingHom_comp_stalkIso` for `Spec.map`. -/
@[elementwise]
theorem localRingHom_comp_stalkIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
(StructureSheaf.stalkIso R (PrimeSpectrum.comap f.hom p)).hom ≫
(CommRingCat.ofHom <| Localization.localRingHom (PrimeSpectrum.comap f.hom p).asIdeal p.asIdeal f.hom rfl) ≫
(StructureSheaf.stalkIso S p).inv =
(Spec.map f).stalkMap p :=
AlgebraicGeometry.localRingHom_comp_stalkIso f p
