English
For any scheme X and point x, the map fromSpecStalk x is isomorphic to the map obtained by applying Spec.map to the germ map and then conjugating by the ΓSpecIso; this provides a canonical description of fromSpecStalk.
Русский
Для любой схемы X и точки x отображение fromSpecStalk совпадает с отображением, полученнымApplying Spec.map к germ-map и затем через ΓSpecIso.
LaTeX
$$Spec_fromSpecStalk (X) (x) = Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ Top Opens.instCompleteLattice.top x trivial)$$
Lean4
@[reassoc (attr := simp)]
theorem fromSpecStalkOfMem_toSpecΓ {X : Scheme.{u}} (U : X.Opens) (x : X) (hxU : x ∈ U) :
U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU) :=
by
rw [fromSpecStalkOfMem, Opens.toSpecΓ, Category.assoc, fromSpecStalk_toSpecΓ_assoc, ← Spec.map_comp, ← Spec.map_comp]
congr 1
rw [IsIso.comp_inv_eq, Iso.inv_comp_eq]
erw [stalkMap_germ U.ι U ⟨x, hxU⟩]
rw [Opens.ι_app, Opens.topIso_hom, ← Functor.map_comp_assoc]
exact (U.toScheme.presheaf.germ_res (homOfLE le_top) ⟨x, hxU⟩ (U := U.ι ⁻¹ᵁ U) hxU).symm
