English
Let R and S be commutative rings. Consider the coproduct of the spectra Spec(R) and Spec(S) as a scheme. Then for every point x of this coproduct, the stalk map along the structural morphism coprodSpec R S at x is an isomorphism of local rings.
Русский
Пусть R и S — коммутативные кольца. Рассмотрим копродукт спектр Spec(R) и Spec(S) как схему. Тогда для любой точки x этого копродукта натянутай стэковая карта вдоль морфизма coprodSpec R S в x является изоморфизмом локальных колец.
LaTeX
$$$\forall (R\ S : Type) [\mathrm{CommRing}~R] [\mathrm{CommRing}~S],\\forall x \in \mathrm{carrier}\left(\mathrm{coprodSpec}\,R\,S\right),\\ IsIso\left( (\mathrm{coprodSpec}\,R\,S).stalkMap\,x \right).$$$
Lean4
theorem isIso_stalkMap_coprodSpec (x) : IsIso ((coprodSpec R S).stalkMap x) :=
by
obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
· have := Scheme.stalkMap_comp coprod.inl (coprodSpec R S) x
rw [← IsIso.comp_inv_eq, Scheme.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inl R S)] at this
rw [coprodMk_inl, ← this]
letI := (RingHom.fst R S).toAlgebra
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) := IsOpenImmersion.of_isLocalization (1, 0)
infer_instance
· have := Scheme.stalkMap_comp coprod.inr (coprodSpec R S) x
rw [← IsIso.comp_inv_eq, Scheme.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at this
rw [coprodMk_inr, ← this]
letI := (RingHom.snd R S).toAlgebra
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) := IsOpenImmersion.of_isLocalization (0, 1)
infer_instance
