English
Under the detailed gluing data for finite covers in the localization setup, there is a unique global section matching all local sections via algebra maps.
Русский
При детализированном задании сцепления для конечного покрытия локализации существует единственный глобальный участок, совпадающий с локальными через алгебраические отображения.
LaTeX
$$$\exists! r: R, \forall a:\; a.\Elem, \text{algebraMap}(R,\mathrm{Away}(a.1))\, r = f a$$$
Lean4
/-- `selfZPow x (m : ℤ)` is `x ^ m` as an element of the localization away from `x`. -/
noncomputable def selfZPow (m : ℤ) : B :=
if _ : 0 ≤ m then algebraMap _ _ x ^ m.natAbs else mk' _ (1 : R) (Submonoid.pow x m.natAbs)
