English
A compatibility statement: Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f, i.e., passing through Spec preserves the morphism f via the closed-point construction.
Русский
Совместимость: Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f, то есть отображение через Spec сохраняет морфизм f через конструирование замкнутой точки.
LaTeX
$$$\\mathrm{Spec}.\\mathrm{map}(\\mathrm{stalkClosedPointTo}\; f) \\;\\gg\\; X.fromSpecStalk\\, _ = f$$$
Lean4
@[reassoc]
theorem Spec_stalkClosedPointTo_fromSpecStalk : Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f :=
by
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
(isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ (f.base (closedPoint R))) isOpen_univ
have := IsAffineOpen.Spec_map_appLE_fromSpec f hU (isAffineOpen_top _) (preimage_eq_top_of_closedPoint_mem f hxU).ge
rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
germ_stalkClosedPointTo]
simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc, Hom.app_eq_appLE, Hom.appLE_map_assoc,
Spec.map_comp_assoc]
