English
There is an inverse pair of constructions between the homogeneous localization at x and the stalk at x, giving an isomorphism of rings when passing through the appropriate universal maps.
Русский
Существует пара конструкторов между однородной локализацией в точке x и стоком в точке x, образующая изоморфизм колец через соответствующие универсальные отображения.
LaTeX
$$$\text{homogeneousLocalizationToStalk}_{\mathcal{A}}(x) \circ \text{stalkToFiberRingHom}_{\mathcal{A}}(x) = \mathrm{id}$$$
Lean4
theorem homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
homogeneousLocalizationToStalk 𝒜 x (stalkToFiberRingHom 𝒜 x z) = z :=
by
obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z
change
homogeneousLocalizationToStalk 𝒜 x
((stalkToFiberRingHom 𝒜 x).hom (((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s)) =
((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s
obtain ⟨V, hxV, i, n, a, b, h, e⟩ := s.2 ⟨x, hxU⟩
simp only [Subtype.forall, apply_mk] at e
rw [stalkToFiberRingHom_germ, homogeneousLocalizationToStalk, e x hxV, Quotient.liftOn'_mk'']
refine Presheaf.germ_ext (C := CommRingCat) _ V hxV (homOfLE <| fun _ h' ↦ h ⟨_, h'⟩) i ?_
change
((Proj.structureSheaf 𝒜).presheaf.map (homOfLE <| fun _ h' ↦ h ⟨_, h'⟩).op) _ =
((Proj.structureSheaf 𝒜).presheaf.map i.op) s
apply Subtype.ext
ext ⟨t, ht⟩
rw [Proj.res_apply, Proj.res_apply]
simp [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk', e t ht]
